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:
lake build
dotnet pack Extractor -c Release -o artifacts/packages
dotnet tool install --global Nethermind.LeanCIL --add-source artifacts/packages --version 0.1.0
dotnet build Examples/Assembly -c ReleaseThe example assembly contains:
public static ulong Add(ulong x, ulong y) => unchecked(x + y);Extract its compiled instructions and check the supplied universal addition proof:
leancil extract Examples/Assembly/bin/Examples.dll "Arithmetic::Add(ulong,ulong)" artifacts/Add
leancil verify artifacts/Add --proof Examples/Proofs/Add.leanSuccess 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, generic methods, loops, memory access and compiled F#.
| Command | Purpose |
|---|---|
leancil list |
Discover canonical method signatures in an assembly |
leancil extract |
Validate and translate a method and its reachable calls |
leancil check |
Check extraction artifacts against their assembly and settings |
leancil verify |
Check, kernel-replay and audit a named theorem |
leancil workspace |
Create an editable Lean proof workspace |
leancil verify-batch |
Verify multiple requests against one consumer snapshot |
check validates extraction consistency; verify establishes the selected theorem.
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.
See consumer packages and workspaces, contract interfaces and integration guidance. 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. 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.
General class allocation and virtual dispatch, 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 coreRun 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.
| Topic | Guide |
|---|---|
| First proof and failure diagnostics | Getting started |
| Proofs, contracts, loops and automation | Writing proofs |
| Modules and proof APIs | Architecture |
| Cross-assembly contracts | Contract interfaces |
| Independently checking imported implementations | Full verification |
| Runtime and architecture assumptions | Runtime profiles |
| Trusted components and guarantees | Soundness |
| Benchmarks and implementation investigations | Performance |
Licensed under either Apache-2.0 or MIT, at your option.