LeanCIL

@3moredays1 @ben_a_adams @leanprover In the Add example, the spec is a separate Lean theorem: addition mod 2^64. The tool extracts the CIL model; choosing that contract is a separate step. github.com/NethermindEth/LeanCIL/blob/main/Exampl…

LeanCIL: formal proofs for your compiled C#, checked by Lean Microsoft's October Patch Tuesday fixed over 1,400 CVEs, more than in all of 2025, and much of that came from AI-driven bug finding. Attackers have the same tools, and more of our code is now written by models that produce convincing code with subtle bugs. “The tests pass” isn’t a strong enough guarantee any more for code that matters. A couple of months ago I proposed an official Lean semantics for C# on csharplang (#10314). One reply asked why not do it at IL level, so it covers F# and everything else that compiles to IL. That’s what I built. You point it at a Release build and a method: leancil extract bin/Release/net10.0/MyLib.dll "Arithmetic::Add(ulong,ulong)" artifacts/Add leancil verify artifacts/Add --proof proofs/Add.lean and it proves your theorem against the IL Roslyn actually emitted. Change the implementation and the same proof fails. Supported (.NET 10, x64 and ARM64, 64-bit little-endian): - Integer arithmetic, including checked, with overflow and divide-by-zero as exact faults - Structs with explicit and sequential layout, enums, ValueTuple - Span<T>, ReadOnlySpan<T>, slicing, MemoryMarshal.Cast/AsBytes, BinaryPrimitives - Arrays, stackalloc, unsafe pointers with checked provenance - Generic methods and structs (proved per concrete type argument), constrained interface calls on structs - Function pointers and tail calls - Collection-expression lookup tables (static ReadOnlySpan<T> Table => [...]) - Selected Vector128/256/512, SSE, AVX2, AVX-512 and AdvSimd intrinsics; IsSupported branches are resolved for the chosen hardware profile - throw new ArgumentException(...) and similar, proved as the exact exception Not supported: float/double, class instances, try/catch/finally, ordinary recursion, virtual dispatch on classes. Unsupported code is rejected with a diagnostic, never silently accepted. The best fit right now is allocation-free integer code where a bug is a security bug: parsers, hashing, big-integer arithmetic, SIMD kernels. NethermindEth/LeanCIL

LeanCIL: formal proofs for your compiled C# and F#, checked by Lean Microsoft's October Patch Tuesday fixed over 1,400 CVEs, more than in all of 2025, and much of that came from AI-driven bug finding. Attackers have the same tools, and more of our code is now written by models that produce convincing code with subtle bugs. “The tests pass” isn’t a strong enough guarantee any more for code that matters. A couple of months ago I proposed an official Lean semantics for C# on csharplang (#10314). One reply asked why not do it at IL level, so it covers F# and everything else that compiles to IL. That’s what I built. You point it at a Release build and a method: leancil extract bin/Release/net10.0/MyLib.dll "Arithmetic::Add(ulong,ulong)" artifacts/Add leancil verify artifacts/Add --proof proofs/Add.lean and it proves your theorem against the IL Roslyn actually emitted. Change the implementation and the same proof fails. Supported (.NET 10, x64 and ARM64, 64-bit little-endian): - Integer arithmetic, including checked, with overflow and divide-by-zero as exact faults - Structs with explicit and sequential layout, enums, ValueTuple - Span<T>, ReadOnlySpan<T>, slicing, MemoryMarshal.Cast/AsBytes, BinaryPrimitives - Arrays, stackalloc, unsafe pointers with checked provenance - Generic methods and structs (proved per concrete type argument), constrained interface calls on structs - Function pointers and tail calls - Collection-expression lookup tables (static ReadOnlySpan<T> Table => [...]) - Selected Vector128/256/512, SSE, AVX2, AVX-512 and AdvSimd intrinsics; IsSupported branches are resolved for the chosen hardware profile - throw new ArgumentException(...) and similar, proved as the exact exception Not supported: float/double, class instances, try/catch/finally, ordinary recursion, virtual dispatch on classes. Unsupported code is rejected with a diagnostic, never silently accepted. The best fit right now is allocation-free integer code where a bug is a security bug: parsers, hashing, big-integer arithmetic, SIMD kernels. NethermindEth/LeanCIL

AI now finds bugs that survived decades of human review, and writes code that looks right but isn’t. Tests can’t keep up. LeanCIL: formal verification for .NET Proofs about compiled C# and F# (any dotnet lang), for every input, checked by @leanprover NethermindEth/LeanCIL

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

@dodyg Working on the Formal Verification side of C#, right now NethermindEth/LeanCIL

@sebify @Kurdiumov First cut. LeanCIL NethermindEth/LeanCIL

I built it instead 😁 Introducing LeanCIL - formal semantics for .NET CIL in Lean 4, with machine-checked proofs against actual compiled assemblies Not just C# - a foundation for verifying F# and other .NET languages too Let's formally verify dotnet NethermindEth/LeanCIL