formal verification

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.

A tiny theorem prover is just a term language, a checker, and a small trusted kernel. We build one in plain Python to make the architecture explicit.

The Curry-Howard correspondence says that types and logical propositions are the same thing. Understanding why changes how you think about both programming and mathematics.

The original roadmap for proving Concrete programs in Lean, updated now that part of that bridge exists: source contracts, proof obligations, Lean-checked evidence, stale detection, and an explicit trusted base.

Vitalik Buterin wants trust nutrition labels for software. Concrete shows what the machine-and-math half looks like when the compiler produces it instead of a vendor writing prose.

Concrete already knows a lot about what a program relies on: authority, allocation, recursion, trust, safety obligations, and proof evidence. The next step is making those facts easy for agents, CI, and reviewers to use.

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.