Can I prove Concrete programs in Lean?

Series note: this is the proof-roadmap entry in the Concrete series. For the language overview, start with Why Concrete Exists and Concrete Spec. For the most practical compiler-report demo, read When the Compiler Is the Oracle.

I wrote the first version of this essay when proving Concrete programs in Lean was still mostly a plan. The question was simple and a little risky: can we take a function written in Concrete, connect it to something inside the compiler, and prove a real property about it in Lean?

Part of that answer now exists. Not for the whole language, and not for the final binary, but for a real subset. Concrete can take a source contract, turn it into an obligation, attach a Lean-checked proof or a decision-procedure result, and tell you when that evidence no longer matches the code. The important part is not that every claim turns green. It is that the tool refuses to mix up “proved,” “assumed,” “trusted,” and “not done yet.”

#Why I think there is an opening

Verified systems code is expensive. The seL4 microkernel took roughly 20 person-years to verify: about 200,000 lines of Isabelle proof for roughly 10,000 lines of C. Fiat Cryptography generates verified primitives that ship in real browsers. Mathlib has formalized an enormous amount of mathematics in Lean. The proof side is fine. The languages are the problem. They were never designed as proof targets, so most of the effort goes into bridging two unrelated worlds.

That bridging cost is what I want to attack. With VST you write C, a separate tool parses it into Coq, and you hope the tool’s model of C matches what your compiler actually does. Verus stays in Rust but has to model unsafe code, implicit Drop, Deref coercions, and everything else Rust was not designed to make verifiable. F* and Dafny start from verification and try to extract systems code, but you end up in a proof assistant. ATS tried to be both, but never caught on.

It always ends the same way: bolt verification onto a language that fights you, or extract systems code from a language that was not built for it. I think Concrete might be in a different position because of a decision I made early on: writing the compiler in Lean 4.

#What the compiler already gives me

Concrete’s compiler is written in Lean 4. I did not do this because I wanted to prove things about programs. I did it because Lean is a good language. But it created a structural opportunity I did not fully appreciate at first.

After parsing and elaboration, every Concrete program becomes Core IR, a small, explicit, fully typed intermediate representation defined as Lean inductive types:

inductive CExpr where
  | intLit (val : Int) (ty : Ty)
  | boolLit (val : Bool)
  | binOp (op : BinOp) (lhs rhs : CExpr) (ty : Ty)
  | call (fn : String) (typeArgs : List Ty) (args : List CExpr) (ty : Ty)
  | match_ (scrutinee : CExpr) (arms : List CMatchArm) (ty : Ty)
  | borrow (inner : CExpr) (ty : Ty)
  | borrowMut (inner : CExpr) (ty : Ty)
  | deref (inner : CExpr) (ty : Ty)
  -- ... ~40 constructors total across CExpr, CStmt, CMatchArm

This is native Lean data. Not a foreign object imported through FFI. Not a serialized AST that some other tool has to parse. The same types the compiler manipulates during elaboration, type checking, and lowering are the types I could write proofs about. There is no translation between two separate tools, though there are still internal boundaries (elaboration, the Core-to-math connection, lowering) where meaning could drift. Those boundaries live inside one codebase rather than across two ecosystems, and that matters.

All surface sugar is gone by the time code reaches Core. Method calls become plain function calls. ? becomes explicit match-and-return. -> becomes dereference-then-field-access. Borrows, moves, and destroys are explicit operations.

The compiler pipeline has hard boundaries:

Parse → Resolve → Check → Elaborate → CoreCheck → Mono → Lower → SSA → Emit

Core is the semantic authority. Everything before it is surface convenience; everything after it is lowering toward machine code. When I started thinking about where a proof boundary would go, Core was the obvious answer. It was already there.

#The original idea

Here is what I want to do. Take a Concrete function, say one that reverses a list:

fn reverse<T>(xs: List<T>) -> List<T> {
    let mut acc: List<T> = List::Nil
    for x in xs {
        acc = List::Cons(x, acc)
    }
    return acc
}

The compiler already elaborates this into a CExpr value in Lean. I want to connect that CExpr to Lean’s existing list library and prove something about it, like that it preserves length.

When I wrote this, I thought I needed three pieces that did not exist yet.

Piece 1: formal evaluation semantics for the proof representation. A Lean definition that says what extracted expressions mean:

-- Sketch, not real code yet
inductive Eval : Env → CExpr → Value → Prop where
  | intLit : Eval env (.intLit n ty) (.int n)
  | binOp : Eval env lhs (Value.int a) →
            Eval env rhs (Value.int b) →
            Eval env (.binOp .add lhs rhs ty) (.int (a + b))
  -- ...

Piece 2: a connection between extracted code and Lean mathematics. I need to show that “this extracted term, when evaluated” means the same thing as “this Lean function over Lean lists.” This is the hardest part, because you are connecting running code to the math you actually care about.

Piece 3: the proof itself. Once the first two pieces exist, I can state and prove:

theorem reverse_length (xs : List α) :
    length (concreteFn_reverse xs) = length xs := by
  -- proof using Lean's standard list lemmas
  -- concreteFn_reverse is the Lean-level interpretation
  -- of the Concrete function's Core representation

That basic shape survived, but the implementation became more honest. The proof boundary is not “the whole compiler is now a theorem.” It is an extracted proof representation, a source-linked theorem, a fingerprint that ties the theorem to the current body, and an evidence class that says exactly what was proved and what remains trusted.

#Why I think Concrete’s design makes this feasible

Writing the compiler in Lean is not enough on its own. If Concrete had the same feature surface as Rust or C++, the Core IR would be enormous and formalization would be just as painful. The reason I think this can actually work is that I designed Concrete to be small, and several of the design choices I made for other reasons turn out to help here.

In Rust, reasoning about ownership requires modeling Drop: implicit destructors that run at scope exit, invisible control flow the programmer never wrote. In Concrete, owned values must be consumed exactly once and cleanup is explicit with destroy and defer. When you formalize Core, what you see is what executes.

Capabilities make effects visible in the type system. If a function has no capability annotations, it is pure; the compiler enforces that. with(File) means file I/O. I can mechanically carve out the pure fragment of a codebase and reason about it without dragging the operating system into the proof.

The trust boundaries double as proof boundaries. Safe code is compiler-checked. trusted code hides pointer-level implementation behind a safe API. Unsafe covers foreign calls and raw system access. The language already marks where each one is, so I do not have to figure out where trust enters the picture.

No operator overloading, no implicit conversions, no closures with hidden captures, no exceptions, no trait objects, no Deref coercions. I originally left these out because I think they make code harder to read and audit. It turns out they also make formalization harder. Not having them keeps the proof surface small.

#How I compare this to other projects

Nobody gets this for free. Verus gets Rust’s ecosystem but has to model a language that fights verification at every turn. Fiat Cryptography generates verified code that no human wrote. RefinedC takes on all of C, and it shows.

What I want is something different: write real low-level code in Concrete, with explicit ownership that compiles to native executables, and then prove properties about it in Lean using Lean’s existing libraries. If the bridge works, the code you prove would be the code you ship, not a model that gets translated. And you would not need a bespoke verification ecosystem because Lean already has one.

Concrete does not have Rust’s ecosystem or C’s installed base. I am betting that a small, explicit language can make the proof part cheap enough to be worth it anyway.

#What changed since the roadmap

Here is where this actually stands now.

What exists now is the first working version of the bridge I was imagining. A Concrete function can carry a contract. The compiler can turn that contract, or a runtime-safety concern like an array bound, into an obligation. A proof can be linked back to the source. A fingerprint ties that proof to the current body. If the body changes, the proof stops being current instead of silently remaining trusted.

The examples matter because they show the shape of the promise and the boundary at the same time. constant_time_tag proves value correctness, but it does not pretend to prove machine-level timing. hmac_sha256 carries a deeper refinement story. Bounds, division, and overflow obligations can be discharged by omega or bv_decide. The negative examples are just as important: assumptions remain assumptions, fake proof names get caught by concrete prove --check, stale proofs go stale, and vacuous contracts do not get to dress up as real proofs.

What still does not exist is just as important. There is no formal proof of the whole checker. There is no verified path from Core through SSA and LLVM to the final binary. There is no whole-program verification story. The proof model is cleaner than the machine that eventually runs the code, and that gap has to stay visible. Concrete now proves real selected claims, but it does not prove the whole program correct end to end.

#Where I expect problems

Pure functions over algebraic data types are the easiest proof target: arithmetic, structural transformations, parsers over bounded inputs. The first proofs should live here.

FFI, Unsafe, and trusted code all sit outside the proof boundary. Foreign functions are black boxes. trusted and Unsafe code do things the type system cannot fully track. You model their contracts as axioms and you do not pretend otherwise. I prefer it this way: the proof tells you exactly where you are trusting something you have not verified, instead of pretending everything is covered.

Mutable heap code is where things start getting expensive again. Separation logic can model it. I would rather earn the right to worry about that later.

Concurrency is last. Real concurrency proofs need explicit models of scheduling, memory ordering, and synchronization, and I do not want to formalize any of that before the simpler cases work well. Concrete defers concurrency to later phases of the language for this reason.

There is another problem I have not mentioned yet: even after a proof representation has clean evaluation semantics, those semantics can still diverge from what the compiler’s lowering passes actually do. But this is a single boundary inside a single codebase, not two separate tools that have to agree on what C or Rust means. Closing that gap, proving lowering preserves semantics, is still a well-defined proof target for later.

#What comes next

The next step is no longer “one proof of one real function.” That happened. The next step is scale and honesty: grow the provable subset, keep evidence classes separate, make proof authoring less painful, tighten the soundness connection between extracted proof terms and the compiler pipeline, and keep the trusted computing base visible enough that nobody mistakes a local proof for a universal guarantee.

Written with an LLM in the loop, like everything here. The ideas and the mistakes are mine. More on how I write.