Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code

TL;DR

This paper discusses the Axon compiler's use of testing, verification, and machine-checked proofs in Lean and Claude Code to ensure code correctness, emphasizing a validation process that reduces the need for audits.

Contribution

It introduces a development process integrating testing and formal verification in the Axon compiler, with proofs fully machine-checked in Lean and Claude Code.

Findings

Proofs guarantee correctness of generated code

Validation process reduces need for manual audits

Evaluation shows effectiveness during compiler development

Abstract

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.