Code written by coding agents may not behave as intended, so effective validation techniques are needed. The paper examines how testing, credible compilation, verification, and audits can be combined when an agent develops a verified compiler.

Axon, a compiler for a simple Fortran-inspired language targeting ARM64, was developed in 34 days by Claude Code in Lean 4 under one human supervisor. The AST→TAC→ASM path is machine-checked for refinement, behavior characterization, and totality. Optimization passes use credible compilation: a verified certificate checker validates each transformation. Testing was used to catch common-case bugs before attempting proofs.

The development reached about 38K lines of Lean, roughly 31K of them theorems, including nine optimizations such as register allocation, LICM, and CSE. Certificate generators were delivered much faster than full proofs, which narrowed correctness gaps. Agent time was dominated by proof search. On Livermore kernels, generated code with optimizations was compared against Fortran at several optimization levels.