Show HN: LeanCIL – Prove properties of compiled .NET code in Lean 4

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

Loading

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 Release

The 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.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, 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 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.

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

License

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