NethermindEth / LeanCIL

# LeanCIL: Formal Verification for .NET
LeanCIL is a Lean 4 formal verification framework for .NET programs. It enables machine-checked proofs of correctness and safety against compiled Common Intermediate Language (CIL), supporting applications written in C#, F#, and other .NET languages.
Verification operates on the assembly's actual compiled instructions using CIL semantics defined in Lean. The current supported subset covers selected instructions and runtime features; unsupported behaviour is rejected explicitly.
## Build and test
Install the toolchain selected by `lean-toolchain` (Lean **4.35.0**, through elan) and .NET SDK **10.0.402**. The extractor uses Mono.Cecil; the F# examples also use FSharp.Core. Both packages are pinned in `Directory.Packages.props`. Lean uses Std and Lean, without Mathlib.
 [code] 
The scripts are .NET file-based apps, with shared C# logic included directly. No scripting runtime is needed beyond .NET.
The test command builds independent example assemblies, runs Lean semantic tests, extracts actual CIL, proves positive examples, checks semantic counterexamples, rejects malformed/unsupported inputs, and tests artifact identity. Results go to `artifacts/test-results.json`; generated CIL, proof caches and verification reports are ignored by Git.
To run one part of the suite, use `dotnet run --file scripts/Test.cs -- --suite core` (or `cli`, `integer`, `narrow`, `primitive`). Each selection builds its prerequisites and writes `artifacts/test-results- .json`. Use separate checkouts when running suites concurrently because tests build and mutate artifacts.
## Command-line tool
Build and install the .NET tool from this checkout:
 [code] 
Discover methods in a compiled assembly:
 [code] 
This lists canonical method signatures you can copy into `extract`, including overloads and non-public methods. Discovery reads metadata without executing the assembly. Listed methods are not necessarily supported: `extract` validates their signatures, CIL and reachable dependencies.
Extract a method from a compiled assembly:
 [code] 
Expected output from the repository root:
 [code] 
Check that the generated files still match the assembly and extraction settings:
 [code] 
Expected output on standard output:
 [code] 
Paths under the current directory are displayed relative to it; paths outside it remain absolute.
All commands exit with code `0` on success. Failures print a diagnostic to standard error and exit with code `1`. Failed checks and verification attempts start with `Invalid:` and produce no standard output. For example, if the generated Lean file has been edited:
 [code] 
The check reads the assembly path, method and hardware profile from the manifest, regenerates the extraction in memory, and compares it with the saved files without overwriting them. Assembly paths are stored relative to the artifact directory. If the DLL moves, use `leancil check artifacts/Add --assembly-path path/to/Examples.dll`; its identity and content must