lean

Formal verification doesn’t eliminate risk. It relocates it into the spec, the model, and the trusted base. Five runnable Lean 4 proofs that compile cleanly and still sit on real bugs.

The same three theorems from the Python prover, now in Lean 4.

Guillermo Angeris builds a working theorem prover in 61 lines of Julia. A tiny trusted kernel, six axioms, and the compiler does the rest. Here is the construction.

I want to prove Concrete programs in Lean. The compiler already produces native Lean data as its IR, and the language is small enough that formalization might actually be tractable.

Wuyts is right about effects and ownership. The Hacker News skeptics are right about complexity. Concrete accepts both and says no to refinement types.

Concrete is a systems language designed so the compiler can reason about what code does: authority, allocation, resource lifetimes, and proof surface.