LeanCIL: Formal Verification for .NET

LeanCIL uses Lean 4 to prove properties of compiled .NET code. It extracts Common Intermediate Language (CIL) from assemblies written in C#, F# and other .NET languages, then checks proofs against an explicit model of those instructions.

You can prove results for every input satisfying a contract, show that a loop terminates, check memory access conditions, or establish a counterexample to an incorrect implementation. Proofs can compose previously proved method contracts without unfolding helper bodies.

The buffer-fill example proves an arbitrary-length fill, including termination, the resulting contents and preservation outside the writable region. The span-content loop proves whether every element is zero over arbitrary-length symbolic caller storage, including termination and exact memory preservation.

flowchart TD
    source["C#, F# or other .NET source"] -- ".NET compiler" --> assembly["Compiled assembly<br/>(the actual CIL)"]
    assembly --> extract["leancil extract<br/>validate and translate"]
    extract --> generated["Extracted.lean<br/>and identity.json"]
    semantics["CIL semantics<br/>in Lean"] --> verify
    generated --> verify["leancil verify<br/>kernel check, replay, axiom audit"]
    assembly -. "SHA-256, regenerate and compare" .-> verify
    proof["Your theorem<br/>and proof"] --> verify
    verify --> report["verified.json<br/>the theorem holds for this CIL"]

    classDef trusted stroke-dasharray: 6 4
    class extract,semantics,verify trusted

The guarantee is exactly the proved theorem, including its preconditions and quantifiers. Lean checks the proof, not whether its statement captures your intended specification. The extractor, CIL model and verification machinery have an explicit trust boundary; LeanCIL does not claim complete CLR or JIT verification.

Install Lean 4.35.0 through elan and .NET SDK 10.0.403, as pinned in lean-toolchain and global.json. From this checkout:

dotnet pack Extractor -c Release -o artifacts/packages
dotnet tool update --global Nethermind.LeanCIL --add-source artifacts/packages --prerelease

The example assembly contains:

public static ulong Add(ulong x, ulong y) => unchecked(x + y);

Build it, extract its compiled instructions and check the supplied universal addition proof:

dotnet build Examples/Assembly -c Release
leancil extract Examples/Assembly/bin/Examples.dll "Arithmetic::Add(ulong,ulong)" artifacts/Add
leancil verify artifacts/Add --proof Examples/Proofs/Add.lean

Success prints Verified: ExampleProof.correctness and writes artifacts/Add/verified.json. The theorem states that the result equals (x + y) mod 2^64 for every pair of 64-bit inputs. Changing the implementation to subtraction makes the unchanged proof fail.

The getting-started walkthrough shows the expected output, edit/rebuild/failure/recovery sequence, and a proof that an invalid memory access cannot succeed. The examples cover arithmetic, calls, structs, classes and virtual calls, strings, generic methods, loops, memory access and compiled F#.

check validates extraction consistency; verify establishes the selected theorem, and verify --goals prints the goal at each sorry and failing tactic of an unfinished proof. Failures return a nonzero exit code. See the CLI reference for all commands, profiles, saved settings and diagnostics.

Keep application specifications and proofs in your own Lean package, with LeanCIL pinned as a dependency. Methods can publish contracts for separately compiled callers; consumer proofs can span multiple modules and share checked support across batch requests. Alternatively, extract --reference Lib.dll pins a referenced assembly by SHA-256 and extracts its bodies into one program; see referenced assemblies.

See consumer packages and workspaces and contract interfaces. Lake configuration and Lean elaborators execute code, so use packages you trust.

LeanCIL supports integer arithmetic, selected control flow and managed calls, reference-free structs, checked memory access, and arrays and spans of integers, enums, reference-free structs and supported integer vectors over supplied storage, reference-free array allocation, typed managed dispatch, and selected runtime helpers and SIMD intrinsics.

It also supports classes deriving from System.Object through admitted classes, created on a budgeted heap, with scalar fields, reference fields holding class instances, and fields holding arrays of class references or single-dimensional arrays of integers, Booleans, chars, enums, reference-free structs or integer vectors. A callvirt of a virtual method dispatches over the extracted classes on the receiver's runtime type, and castclass and isinst decide an admitted class from the instance's lineage. One-dimensional arrays of class references are allocated, loaded and stored with the runtime's covariance check. Strings, including interned literals, and classes outside the model are opaque references that are passed, stored, compared and tested against null but never read. Framework argument guards such as ArgumentNullException.ThrowIfNull are checked as runtime contracts.

Each has restrictions documented in the opcode support table and intrinsic support tables. Unsupported instructions and signatures are rejected explicitly.

The checked memory model tracks allocation identity, lifetime, bounds, permissions, initialization and alignment. CIL.Safety.invoke is the execution model for both functional correctness and memory-safety claims.

Other classes and field types, arrays of references other than one-dimensional arrays of admitted classes or of non-generic classes such as string, reading a string's characters, virtual dispatch outside the extracted classes, interface calls, type tests against interfaces, System.Object or value types, boxing, ordinary recursive calls, exception handlers, floating-point arithmetic and arbitrary external calls are outside the supported subset. Concurrency, GC implementation correctness and equivalence to arbitrary .NET runtimes are outside the model's guarantees. See soundness and limitations.

lake build
dotnet run --file scripts/Test.cs -- --suite core

Run dotnet run --file scripts/Test.cs for the full suite. Tests compile example assemblies, check Lean proofs, exercise rejection cases and validate artifact identity. Results are written to artifacts/. Use separate checkouts for concurrent suites because they mutate those files. See validation coverage and suite commands and CI operation.

Licensed under either Apache-2.0 or MIT, at your option.