What Was Actually Hard: Finishing a Verified Compiler in Lean 4

2026-07-26 • 15 min read

Last updated: 2026-07-26 • Commit 515157d

A while back I wrote a post about phi, a formally verified LISP compiler in Lean 4, titled "The Verification Gap." It was a list of the things I expected to be hard. The proof is done now, and I ranked almost every item on that list wrong.

This is the correction, and it is a more interesting post than the original would have been if I'd been right.

First, the theorem I stated was not a theorem

The old post opened with this:

theorem compiler_correct (e : LispExpr) (env : Env) (fuel : Nat) :
  execute (compile e) env fuel = evaluate e env fuel

That signature never type-checked and never could have. It equates a stack machine's output with an integer, silently. Here is what actually got proven:

theorem compiler_correct (e : LispExpr) (env : Env) (s : Stack) :
    execute (compile [] e) env s = eval e env :: s

$$\forall e, \rho, \sigma.\quad \mathrm{execute}(\mathrm{compile}([\,], e), \rho, \sigma) \;=\; \mathrm{eval}(e, \rho) :: \sigma$$

Three differences, each of which is a thing I learned:

  1. The result is a stack, not an integer. The compiled code pushes one value onto whatever stack it was handed. Stating it this way rather than as execute ... = [eval e env] is what makes the theorem compose with itself, which turns out to be the whole ballgame. More below.
  2. compile takes a compile-time context ([] at top level). That argument did not exist when I wrote the first post, because let-bindings did not exist.
  3. fuel is gone from the statement. For most of this project's life that was its honest gap. It is closed now, and closing it turned up a bug in my own definitions — that story is below.

What I thought was hard and wasn't

Jump offsets. The old post: "The challenge: jumps are encoded as relative offsets during compilation. The executor must maintain PC state and handle forward/backward jumps correctly. Get this wrong and the proof is impossible."

This was maybe two hours of work. There is no program counter. execute recurses on the instruction list itself and a jump is just List.drop:

def execute (insts : List StackInst) (env : Env) (stack : Stack) : Stack :=
  match insts with
  | [] => stack
  | .jump n :: is => execute (is.drop n) env stack
  | .jumpIfFalse n :: is =>
    match stack with
    | v :: rest =>
      if v = 0 then execute (is.drop n) env rest
      else execute is env rest
    | _ => stack
  | i :: is => execute is env (runInst i env stack)
termination_by insts.length

termination_by insts.length discharges immediately because drop never lengthens a list. The entire jump-correctness burden collapses into one arithmetic lemma:

theorem drop_succ_cons_append {α : Type} (x : α) (l1 l2 : List α) :
    List.drop (l1.length + 1) (l1 ++ x :: l2) = l2

That is it. Forward-only relative jumps into a list you already have in your hand are not a hard verification problem. They are a hard implementation problem in a real machine with mutable PC state, and I imported that intuition from the wrong domain.

Stack depth preservation, jump target validity, fuel consumption matching. I listed these as four required lemma families. Zero of them exist in the final proof. They are all consequences of the compositional statement rather than prerequisites for it.

What was actually hard

1. Correctness alone is not provable. You need the append property simultaneously.

The cond case compiles to:

| .cond c t e =>
  let tc := compile ctx t
  let ec := compile ctx e
  compile ctx c ++ [.jumpIfFalse (tc.length + 1)] ++ tc ++ [.jump ec.length] ++ ec

To reason about this you need two facts at once. You need correctness of the condition, because jumpIfFalse pops a value and you cannot take that step until you know the stack is a cons. And you need an append property — that running l1 ++ l2 is running l2 on the output of l1 — to compose the pieces at all.

Neither is provable from the other. Correctness is used inside the append proof, and the append property is used inside the correctness proof. So the theorem is a conjunction, proven by one induction:

theorem compile_correct_and_append (ctx : CEnv) (e : LispExpr) :
    (∀ env genv s, Matches ctx s env genv →
        execute (compile ctx e) genv s = eval e env :: s) ∧
    (∀ l2 genv s,
        execute (compile ctx e ++ l2) genv s
          = execute l2 genv (execute (compile ctx e) genv s))

This is the single structural insight of the project. The public compiler_correct is a one-line projection out of it.

The append property is also why the theorem is stated on an arbitrary incoming stack s rather than []. Generality here is not aesthetics — a statement about [] gives you no induction hypothesis when the subexpression runs on top of a partially-built stack.

2. Lean's derived induction principle does not work for variadic primitives

LispExpr has a constructor holding a nested list:

| primitive : String → List LispExpr → LispExpr

Lean 4's auto-derived recursor gives an induction hypothesis of the shape $\forall x \in \mathit{args}.\ \mathrm{motive}(x)$, not a clean per-argument hypothesis. A direct induction e with split simply does not go through for this case.

Standard answers are a custom recursor or threading a List.Forall argument. I did neither. Instead compile and eval were each split into a mutual block with list-shaped helpers, and the proof mirrors that exact shape:

mutual
def compile (ctx : CEnv) (e : LispExpr) : List StackInst := ...

def compilePrimArgs (ctx : CEnv) (op : String) : List LispExpr → List StackInst
  | [] => [.pushInt 0]
  | [e] => compile ctx e
  | e :: es => compile ctx e ++ compileRestWithOps (none :: ctx) op es

def compileRestWithOps (ctx : CEnv) (op : String) : List LispExpr → List StackInst
  | [] => []
  | e :: es => compile ctx e ++ [.callOp op] ++ compileRestWithOps ctx op es
end

Lean's termination checker accepts the mutual recursion because each helper recurses on a strict sublist while compile recurses on a strict subterm. The induction is then structural on the actual definitions rather than on the derived recursor, which sidesteps the problem instead of fighting it.

The corresponding proof lemmas — compilePrimArgs_correct_and_append, compileRestWithOps_correct, compileRestWithOps_append — live in the same mutual block as the main theorem. The last two are stated on a non-empty stack (acc :: rest), because the fold accumulator is already sitting there. Getting that shape right took longer than writing them.

Variadic arity is genuine left-fold semantics, not two-argument sugar: (+ 1 2 3 4) compiles and is proven.

3. Let-bindings, and the trick that made them work

Locals live on the value stack. pushLocal i reads $i$ slots down, slide drops the binding sitting underneath a result. The problem: a local's stack index shifts every time an unrelated temporary is pushed above it. Most visibly when compiling the right operand of a binary operation, where the left operand's value is already on the stack.

The obvious fix is a separate depth counter threaded alongside the context. That works and is miserable to prove things about, because now two things have to stay in sync.

Instead, the compile-time context is List (Option String) and the shift is recorded by pushing an anonymous slot:

abbrev CEnv := List (Option String)

| .binOp op a b => compile ctx a ++ compile (none :: ctx) b ++ [.callOp op]
| .letE x v b => compile ctx v ++ compile (some x :: ctx) b ++ [.slide]

The none entries carry no name and can never be looked up, so they cost nothing semantically — but they occupy an index, so lookupSlot returns the correct shifted depth automatically. Every place a temporary appears, an anonymous slot appears with it:

Correctness is stated against a relation tying context to runtime stack:

def Matches (ctx : CEnv) (s : Stack) (env genv : Env) : Prop :=
  ∀ x, env x =
    match lookupSlot ctx x with
    | some i => s.getD i 0
    | none => genv x

$$\mathrm{Matches}(\Gamma, \sigma, \rho, \gamma) \;\equiv\; \forall x.\ \rho(x) = \begin{cases} \sigma[i] & \text{if } \mathrm{lookupSlot}(\Gamma, x) = \mathrm{some}\ i \ \gamma(x) & \text{otherwise} \end{cases}$$

Two lemmas, matches_push_anon and matches_push_bind, say that pushing a value preserves this relation under the corresponding context extension. They carry essentially the entire let-binding proof.

4. The one piece of scaffolding that looks redundant and isn't

The append half of the combined theorem has no env in scope — it is a statement purely about instruction lists and stacks. But the cond and primitive cases still need to know the incoming stack is a cons, which is a fact about evaluation.

The resolution is a function that reads a canonical environment back off the stack:

def envOf (ctx : CEnv) (s : Stack) (genv : Env) : Env :=
  fun x =>
    match lookupSlot ctx x with
    | some i => s.getD i 0
    | none => genv x

theorem matches_envOf (ctx : CEnv) (s : Stack) (genv : Env) :
    Matches ctx s (envOf ctx s genv) genv := fun _ => rfl

It is Matches read as a definition instead of a proposition, which is why the theorem is rfl. It manufactures an environment out of thin air so the append proof can invoke the correctness half. It looks like duplication and deleting it breaks the build.

A verified optimizer, nearly for free

Once the compiler theorem is stated as an equation on eval, an optimizer proof composes with it directly. optimize does constant folding: binOp over two literals folds to a literal, cond on a literal condition drops the dead branch entirely.

theorem optimize_sound (e : LispExpr) (env : Env) :
    eval (optimize e) env = eval e env

And then the payoff is two rewrites:

theorem compile_optimize_correct (e : LispExpr) (env : Env) (s : Stack) :
    execute (compile [] (optimize e)) env s = eval e env :: s := by
  rw [compiler_correct, optimize_sound]

$$\mathrm{execute}(\mathrm{compile}([\,], \mathrm{optimize}(e)), \rho, \sigma) = \mathrm{eval}(e, \rho) :: \sigma$$

Measured: 6*7+8 goes from 5 instructions to 1. A cond with a constant condition goes from 9 to 1. An expression over unbound atoms is correctly left alone at 3.

There is deliberately no constant propagation into letE bodies. That requires substitution and a capture-avoidance argument, which is a real piece of work and not what this pass is for.

What is actually proven, stated precisely

lake build succeeds with zero sorry and zero admit. The full axiom check:

'Phi.compiler_correct' depends on axioms: [propext, Quot.sound]
'Phi.execute_compile_append' depends on axioms: [propext, Quot.sound]
'Phi.optimize_sound' depends on axioms: [propext, Quot.sound]
'Phi.compile_optimize_correct' depends on axioms: [propext, Quot.sound]
'Phi.evaluate_eq_eval' depends on axioms: [propext, Quot.sound]
'Phi.evaluate_depth_eq_eval' depends on axioms: [propext, Quot.sound]
'Phi.evaluate_stable' depends on axioms: [propext, Quot.sound]

No sorryAx, and not even Classical.choice. Every constructor of the AST is genuinely proven — atom, num, binOp, cond, letE, and variadic primitive — with no stub cases anywhere.

The last three lines of that check did not exist when I started writing this post. Getting them is the subject of the next section, and doing it exposed a bug.

The bug that writing this post found

I originally drafted this post with a section admitting that evaluate — the fueled evaluator — had zero theorems about it. Every proof targeted the fuel-free eval. The missing bridge was:

$$\forall e, \rho, n.\quad n \geq \mathrm{depth}(e) \;\Longrightarrow\; \mathrm{evaluate}(e, \rho, n) = \mathrm{eval}(e, \rho)$$

Writing that sentence down is what made me look at depth, which was this:

| .primitive _ _ => 1

That is wrong, and it makes the bridge false as stated. evaluate recurses into a primitive's arguments at fuel - 1, so a primitive's depth is not 1 — it is one more than the deepest argument. A four-element (+ 1 2 3 4) claimed depth 1 and needed depth 2. The theorem was unprovable, not because the proof was hard, but because the statement was a lie about my own code.

Nothing was running wrong. depth was dead code, used by nothing. The error was invisible to every test that could have been written, and it surfaced the moment I tried to state a property that mentioned it. This is the entire pitch for formal methods compressed into one bug.

The fix makes depth mutual, mirroring the mutual definition of eval:

mutual
def LispExpr.depth : LispExpr → Nat
  | .atom _ => 1
  | .num _ => 1
  | .binOp _ a b => 1 + max a.depth b.depth
  | .cond c t e => 1 + max c.depth (max t.depth e.depth)
  | .letE _ v b => 1 + max v.depth b.depth
  | .primitive _ args => 1 + LispExpr.depthArgs args

def LispExpr.depthArgs : List LispExpr → Nat
  | [] => 0
  | e :: es => max e.depth (LispExpr.depthArgs es)
end

And then the bridge goes through:

theorem evaluate_eq_eval (fuel : Nat) (e : LispExpr) (env : Env)
    (h : e.depth ≤ fuel) : evaluate e env fuel = eval e env

The one interesting part is the termination measure. evaluate_eq_eval recurses at fuel - 1, while its mutual partner evaluateArgs_eq_evalArgs recurses at the same fuel on a structurally smaller argument list. Neither ordering alone is well-founded. The measure is lexicographic:

$$\left(\mathit{fuel},\ \mathrm{sizeOf}(e)\right)$$

First component drops when descending into a subexpression, second drops when walking the argument list. Once that is written down Lean accepts it without complaint.

Two corollaries fall out, and the second is the one I actually wanted:

theorem evaluate_depth_eq_eval (e : LispExpr) (env : Env) :
    evaluate e env e.depth = eval e env

theorem evaluate_stable (e : LispExpr) (env : Env) (m n : Nat)
    (hm : e.depth ≤ m) (hn : e.depth ≤ n) :
    evaluate e env m = evaluate e env n

evaluate_stable says any two sufficient fuel budgets agree — which is the precise sense in which fuel is currently vestigial. It stops being vestigial the moment recursive function application arrives, which is exactly why the parameter is staying.

Deleting the last stub

list was the final unhandled constructor. Both eval and compile defaulted it to 0 / [pushInt 0], and its case in the correctness proof was rfl — not a proof that lists compile correctly, only that the stub agreed with itself. Precisely the kind of thing that lets you say "all cases proven" while meaning nothing.

Giving it real semantics means Stack := List Int becomes a nested value type, rippling through runInst, execute, evalPrim, Matches, envOf, and every proof in the tree. That is a version-2 project, not a loose end.

So I deleted it from the AST. Six constructors, all of them genuinely proven, no stub cases anywhere:

inductive LispExpr where
  | atom : String → LispExpr
  | num  : Int → LispExpr
  | binOp : String → LispExpr → LispExpr → LispExpr
  | cond : LispExpr → LispExpr → LispExpr → LispExpr
  | letE : String → LispExpr → LispExpr → LispExpr
  | primitive : String → List LispExpr → LispExpr
  deriving Repr

Removing a feature to make a claim true is a better trade than keeping it to make a feature list longer. The stub was costing me the ability to say a clean sentence about the whole AST, and it was buying nothing.

What is still not proven, stated equally precisely

This is the part the last post should have had and didn't, so I am overcorrecting.

Everything is total, so nothing is rejected. Env := String → Int is a total function; unbound atoms return 0. Unknown operators, wrong arity, and fuel exhaustion also return 0. This was a deliberate choice to avoid Option-monad bookkeeping in the proofs, and it has a real cost: compiler_correct says the compiler is correct for well-formed programs. It does not say malformed programs are detected or rejected. A verified compiler that agrees with a permissive semantics is not the same as a verified compiler.

There is no parser. Phi/Parser.lean is def stubParser : Unit := () and this is on purpose. A hand-rolled unverified frontend would be the one unproven component on the critical path, and would weaken the claim rather than strengthen it. Depth over breadth.

The actual lesson

The old post said: "This is where most compiler verification projects get stuck", about structural induction over flattened bytecode. That was the one thing I got right, but for the wrong reason. The problem is not that structure is destroyed. It is that the naive statement of correctness is too weak to be its own induction hypothesis, and finding the stronger statement that is self-supporting is the work.

Every hard part of this project was a statement problem, not a tactic problem. The combined correctness-and-append conjunction, the none slots, envOf, the mutual helpers mirroring the mutual definitions, the lexicographic fuel measure — none of them are clever proof scripts. They are all cases of writing down the right thing, after which the proof is mostly mechanical. I spent the first post worrying about simp and induction invocations. Those were never the bottleneck.

The depth bug is the sharpest version of this. It sat in the source for weeks, was never wrong at runtime because nothing called it, and could not have been caught by any test. It became visible the instant I tried to state a theorem that mentioned it. That is not a story about proof assistants catching bugs in programs — it is a story about being forced to say precisely what you mean, and discovering you had not.

References