The Verification Gap: Building a Proven-Correct Compiler in Lean 4

2024-07-25 • 3 min read

Last updated: 2026-07-25 • Commit 16a36f9

I'm working on phi, a formally verified LISP compiler written in Lean 4. The goal is ambitious: prove mathematically that the compiler's output bytecode is semantically equivalent to the source program. Not "test extensively" or "fuzz until confident" — actually prove correctness.

The Core Theorem

The entire project hinges on one property:

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

This says: executing the compiled stack bytecode produces the same result as evaluating the high-level expression tree. If Lean accepts this theorem, the compiler is guaranteed bug-free for all inputs.

What's Working

The compilation pipeline itself is straightforward:

def compile (e : LispExpr) : List StackInst :=
  match e with
  | .num n => [.pushInt n]
  | .binOp op a b => compile a ++ compile b ++ [.callOp op]
  | .cond c t e =>
    let tc := compile t
    let ec := compile e
    compile c ++ [.jumpIfFalse (tc.length + 1)] ++ tc ++ [.jump ec.length] ++ ec

Source evaluation is done:

def evaluate (e : LispExpr) (env : Env) (fuel : Nat) : Int :=
  match fuel with
  | 0 => 0
  | fuel' + 1 =>
    match e with
    | .num n => n
    | .binOp op a b =>
      evalPrim op (evaluate a env fuel') (evaluate b env fuel')
    | .cond c t e =>
      if evaluate c env fuel' != 0 then evaluate t env fuel'
      else evaluate e env fuel'

The Missing Pieces

Here's where I'm stuck:

1. Stack Machine Semantics

The compiler outputs bytecode (List StackInst), but there's no execution model. Need to implement:

def execute (code : List StackInst) (env : Env) (fuel : Nat) : Int

This requires: - Stack representation (List Int) - Program counter tracking - Instruction dispatch logic - Jump offset resolution

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.

2. Proof Infrastructure

Even with working execute, proving correctness requires lemmas about: - Stack depth preservation - Jump target validity - Instruction sequence equivalence - Fuel consumption matching

Lean's tactics (induction, simp, cases) need careful application. The proof structure likely needs:

-- Prove each instruction preserves semantics
lemma compile_binOp_correct ...
lemma compile_cond_correct ...

-- Compose into full theorem
theorem compiler_correct ...

3. The Induction Problem

The natural proof strategy is structural induction on LispExpr. But the compiled bytecode is a flat list — the structure is destroyed. Need to establish invariants relating: - Source expression depth - Stack height after execution - Remaining fuel at each step

This is where most compiler verification projects get stuck.

Why Lean 4?

Lean's dual nature is crucial here: 1. Programming language: Write actual executable compiler code 2. Theorem prover: Prove properties about that code

The same function that compiles LISP also serves as the subject of mathematical proof. No model mismatch between specification and implementation.

Next Steps

Priority order: 1. Implement stack machine execution with PC/stack state 2. Test execution against evaluation on sample programs 3. Write trivial lemmas (e.g., execute [.pushInt n] env f = n) 4. Build up to conditional/jump lemmas 5. Attempt full induction proof

The gap between "working compiler" and "proven compiler" is exactly where the interesting work lives. That's the goal of phi.

References