Spec# is an experimental programming system that seeks to push the envelope in specification and verification technology. The system includes the .NET object-oriented programming language Spec#, which is a superset of the C# language, adding type features like non-null types and contract features like pre- and postconditions and object invariants. The types are checked by the compiler. The contracts are checked dynamically through compiler-inserted run-time checks, and they can also be checked statically using the Spec# automatic program verifier. The system is integrated into Microsoft Visual Studio.
Related resources