Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
For developers of verified compilers, this work demonstrates a practical process integrating multiple validation techniques with AI-assisted proof generation, though it is incremental in applying existing verification methods.
The paper presents the Axon verified compiler, built in Lean by Claude Code, with fully machine-checked proofs guaranteeing generated code correctness, eliminating the need for manual code audits. It evaluates a development process combining testing, credible compilation, and verification.
This paper presents the use of testing, credible compilation/translation validation, verification, and audits in the Axon compiler. Axon comes with fully machine checked proofs that guarantee the correctness of the generated code. All code and proofs were written in Lean by Claude Code, with the correctness proofs eliminating any need to audit or examine any verified code. I present a development process for using these validation techniques, evaluate the use of this process during the development of the compiler, and discuss implications for other development efforts.