lean_models

Prove real Python / C++ / Rust / SystemVerilog programs correct in Lean 4.

Each language gets a deep embedding: the program’s real AST becomes a Lean value, and a definitional interpreter gives it meaning. Programs stay source-shaped — the Lean term mirrors the file you wrote — so specs and proofs read against code you recognize, which is what makes AI-assisted proving tractable.

Language progress

These bars use each tier’s checked-in differential corpus: MATCH rows divided by all rows, rounded to one decimal place. The linked coverage pages are the source of truth; this table is regenerated by harness/language_progress.py.