.Net CodeContracts were this for me, but that was never fast. C# is a statically-typed language, so what kind of types could you further add to it? As a trivial

.Net CodeContracts were this for me, but that was never fast. C# is a statically-typed language, so what kind of types could you further add to it? As a trivial example, maybe you want to ensure that `invoice_id` consists of at least 20 characters. CodeContracts would then statically attempt to prove that assertion for you. They had meticulously annotated the entirety of the .Net stdlib, and those annotations were spot-on. This obviously helps with things like `null`. It completely changed the way I code. You have to think a little bit more about how you structure your code if you plan to hand it off to a theorem prover. I unlearned several bad habits (I unlearned even more with Rust).