Microsoft developed the excellent Code Contracts[1] project. From the user's perpective, tt was a simple class called Contracts with a few methods such as Requi

Microsoft developed the excellent Code Contracts[1] project. From the user's perpective, tt was a simple class called Contracts with a few methods such as Require(), Ensure() and Invariant() Underneath the hood it used the Z3 Solver[2], which is both intuitive, flexible and fast. It validated the contracts while coding and highlighted in the Visual Studio IDE when a contract was broken. You could write something like: Contracts.Requires(x > 5 && y > x); Which would get translated to a compile time check as well. Unfortunately, Code Contracts has been dead for years now, and it was even removed entirely from .NET[3] due to being hard to maintain, and the verifier stopped working in newer versions of VS. Luckily, C# developers now have a small taste of contracts due to nullability analysis[4], but even more exciting is that contracts is making its way into C# as a first-level standard[5]. [1] https://www.microsoft.com/en-us/research/project/code-contracts/ https://www.microsoft.com/en-us/research/project/code-contra... [2] https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [3] https://github.com/dotnet/runtime/issues/20006 https://github.com/dotnet/runtime/issues/20006 [4] https://docs.microsoft.com/en-us/dotnet/csharp/nullable-references https://docs.microsoft.com/en-us/dotnet/csharp/nullable-refe... [5] https://github.com/dotnet/csharplang/issues/105 https://github.com/dotnet/csharplang/issues/105