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

Category: devtools

Tags: formal-verification, dotnet, lean4, cil, static-analysis

Score: 7.8/10 (Innovation: 8, Technical: 9, Documentation: 8, Utility: 6)

LeanCIL extracts CIL from compiled .NET assemblies and verifies Lean 4 proofs against an explicit formal model of the instruction set. It enables machine-checked correctness and memory-safety claims for C#, F#, and other .NET languages, with a working memory model, contract composition, and explicit trust boundaries.

Target audience: formal methods researchers, security-critical .NET developers, compiler engineers

Repository: https://github.com/NethermindEth/LeanCIL · Lean · NOASSERTION · 64 stars

View on Hacker News