proglib

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

proglib is to programs what Mathlib is to mathematics: the definitions and scaffolding you need to state and prove theorems about programs written in real languages. Each language’s semantics follows that language’s reference and is tested differentially against a reference implementation.

Renamed 2026-11-10: this repository was lean-surfaces, and old links redirect. The Lean library is still imported as LeanModels; a later, announced commit renames it to Proglib.

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.

| Language | Completion | Current measurement | | --- |…