The ambitious goal of this project is the automation of code optimization by using LLM agents to convert a lean DSL to optimized C code with provably equivalent results.

Status

The first two steps are done. A Lean 4 DSL for in-place array programs emits C. Its first task is sorting: bubble sort and insertion sort are written in it and proven correct in Lean. The result is sorted and a permutation of the input, with no out-of-bounds access, underflow or overflow. The DSL, the C model, the emitter and their proofs are generic, so other tasks can follow.

The emitter is proven correct too, against a model of C11 written in Lean: any contract proven for a program holds for its emitted C function, which also returns without undefined behaviour. The C model and the printer are trusted, so the C is also tested against the Lean semantics with gcc and sanitizers. See lean/README.md for details.

Plan	Goal	Status
01	Sorting DSL, semantics, C emitter, proofs for bubble and insertion sort	Complete
02	Prove the C emitter correct (C model in Lean)	Complete
03	Function signatures as an explicit concept, so programs need not all be void f(int32_t *a, size_t n)	Proposed

Example: bubble sort

Bubble sort in the DSL (lean/LeanToC/Sorts/BubbleSort.lean):

def bubbleBody : Stmt :=
  .ite (.vlt (.read (.add (.var "j") (.lit 1))) (.read (.var "j")))
    (.swap (.var "j") (.add (.var "j") (.lit 1)))
    .skip

def bubblePass : Stmt :=
  .forRange "j" (.lit 0) (.sub (.sub .len (.var "i")) (.lit 1)) bubbleBody

def bubbleSort : Stmt :=
  .forRange "i" (.lit 0) .len bubblePass

The C that lake exe emit_c generates from it, in out/sorts.c. The comment above the function is its proof anchor. It names the Lean theorem that proves this C function correct against the C model, and the theorem's precondition and postcondition in C terms:

// PROOF_ANCHOR: LeanToC.ArrayProgram.c_correct, from LeanToC.Sorts.bubbleSort_correct
// Pre:  a points to n readable and writable int32_t (a may be NULL if n == 0)
// Post: returns without undefined behaviour, with a[0..n) sorted ascending
//       and a permutation of its initial contents
void bubble_sort(int32_t *a, size_t n) {
  size_t i = 0, j = 0;
  for (i = 0; i < n; i++) {
    for (j = 0; j < n - i - 1; j++) {
      if (a[j + 1] < a[j]) {
        { int32_t swap_tmp = a[j]; a[j] = a[j + 1]; a[j + 1] = swap_tmp; }
      }
    }
  }
}

Only bubbleSort_correct was written for this algorithm. It proves that bubbleSort sorts every array in the DSL, with no out-of-bounds access and no index overflow or underflow; for example, n - i - 1 never wraps around. The step from DSL to C is proven once for all programs.

Repository layout

Path	Contents
lean/	The Lake project: DSL, semantics, emitter, proofs, tests (README)
tests/harness.c	C side of the differential tests (lake exe difftest)
plans/	Plans: goals, design, phases, and notes on what was built
studies/	Studies of design questions, with measurements and a recommendation (e.g. whether to use Mathlib)
references/	Links to background reading (the Truth Research ZK article) and the C11 standard, which initialize-devcontainer.sh downloads to references/n1570.pdf (README)
.agents/agents.md	Instructions for agents working in this repository (via CLAUDE.md)
.devcontainer/	Devcontainer definition, the Forgejo server's pinned SSH host keys (known_hosts), and how the Git remote is set up (README)
initialize-devcontainer.sh	Idempotent setup: gcc, PDF tools and the C11 standard, SSH, elan/Lean, first build. Runs on container creation
setup-ssh.sh	Idempotent SSH setup for the Forgejo remote (details); run by initialize-devcontainer.sh
run_claude.sh	Starts Claude Code inside the devcontainer
out/	Generated C and test builds (gitignored)

Quick start

./initialize-devcontainer.sh   # only needed outside a freshly created container
cd lean
lake build                     # library, proofs and build-time tests
lake exe emit_c ../out         # write every suite, e.g. out/sorts.c and out/sorts.h
lake exe difftest              # compare the C with the Lean semantics (--minic: and the C model)