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编写，正确性证明消除了审计或检查任何已验证代码的必要性。作者提出了一种使用这些验证技术的开发流程，评估了该流程在编译器开发过程中的应用效果，并探讨了其对其他开发项目的启示意义。