Mon 15 Jun 2026 11:20 - 11:40 at Meadows B - PAgE Session 1 Chair(s): Shraddha Barke

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.

Mon 15 Jun

Displayed time zone: Mountain Time (US & Canada) change

10:40 - 12:20
PAgE Session 1PAgE at Meadows B
Chair(s): Shraddha Barke Microsoft Research, Redmond
10:40
20m
Talk
Agentic Code Reasoning
PAgE
Shubham Ugare Meta, Satish Chandra Meta Platforms, Inc.
Pre-print
11:00
20m
Talk
Towards Verified Code Reasoning by LLMs
PAgE
Meghana Aparna Sistla Google DeepMind, Gogul Balakrishnan Google, Patrick Rondon Google, José Pablo Cambronero Google, USA, Michele Tufano Google, Satish Chandra Meta Platforms, Inc.
11:20
20m
Talk
Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude CodeRemote
PAgE
Martin C. Rinard Massachusetts Institute of Technology
11:40
20m
Talk
The Next Frontier for AI-Generated Kernels: Correctness
PAgE
Guido Martínez Microsoft Research, Tyler Sorensen University of California at Santa Cruz
DOI Pre-print
12:00
20m
Talk
Testing LLM-Generated Distributed Protocol Code
PAgE
Ankush Das Boston University, Brendan Coyne Boston University