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-contra...

[2] https://github.com/Z3Prover/z3

[3] https://github.com/dotnet/runtime/issues/20006

[4] https://docs.microsoft.com/en-us/dotnet/csharp/nullable-refe...

[5] https://github.com/dotnet/csharplang/issues/105