Formal verification
Formal verification uses automated tools to prove that given certain assumptions and conditions and without executing the program code, a program or procedure conforms to a certain specification. Silver uses the Spec# compiler and program verifier to formally verify C# smart contracts.
Spec# is a programming system created by Microsoft Research for developing correct .NET programs. Spec# was originally conceived as an extension to the C# language with constructs like non-null types and method contracts for creating specifications for object-oriented .NET software, and came with a complete toolset featuring a compiler, an IDE extension to Visual Studio 2005/2008, and a static program verifier codenamed Boogie.
From Verification of C# programs using Spec# and Boogie 2 by Rosemary Monahan
Boogie was later spun off to its own independent project and is now widely used as a general-purpose intermediate verification language. The Boogie program verifier generates logical formulas known as verification conditions from a Spec# program where showing the verification conditions are valid using the Z3 SMT solver implies that the program satisfies its specification.
Spec# originally targeted the C# 2.0 language specification and .NET 2.0. Silver uses an updated fork of Spec# which targets the .NET Framework 4.x so it can run without issue on modern systems and removes the outdated Visual Studio extension in favor of an updated command-line compiler and project system that can handle modern .csproj project files. Silver also uses a Roslyn based rewriter to rewrite newer C# syntax like interpolated strings to be interoperable with the Spec# compiler which only supports C# 2.0 features.
When you use the --verify switch with the compile command, Silver uses the Spec# compiler to create a separate assembly that can be verified using the Spec# program verifier. Specifications for the smart contract can be embedded in the C# source code of the smart contract as comments. This preserves C# source compatibility with other compilers and validators like the Stratis SCT tool.
One of the ways to declare a program specification is via a method contract. A contract specifies an agreement between a method (the callee) and the code that calls it (the caller) about what both sides can expect the state of a program to be in before and after the method is called. Statically typed languages like C# already contain the notion of a method contract in a method's signature which defines the layout of the data the program will pass to the method (by putting this data on the machine stack before the method call for instance) and the data the method will return to caller when it completes.
Spec# provides syntax for specifying non-null types, method pre-conditions, post-conditions, and object invariants.