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.

翻译：本文介绍了在Axon编译器中应用测试、可信编译/翻译验证、形式化验证及审计的方法。Axon编译器配备了完全机器可检查的证明，以确保生成代码的正确性。所有代码及证明均由Claude Code以Lean语言编写，正确性证明消除了对任何已验证代码进行审计或检查的必要性。本文提出了一种采用这些验证技术的开发流程，评估了该流程在编译器开发过程中的应用效果，并探讨了其对其他开发项目的启示。