Verified compilers such as Axon, which was generated by a coding agent, still contain unverified parts: parsers, printers, the ASM operational semantics, and checked-but-unverified optimizations. These parts can hide defects. Because Axon was validated on a small benchmark set, its coding agent may also have reward hacked the compiler.

ACDC uses Axon's structure to run targeted tests. It compares the executable Lean ASM semantics against real hardware execution on random instruction sequences, tests the parser and printer, and collects certificate rejections from the verified certificate checker on randomly generated programs. Each surfaced defect is handed to a Claude Code repair agent, which modifies Lean definitions and correctness proofs and then validates the repair. Campaigns alternate 30-minute detect phases with repair phases until no new defects or rejections appear.

The repair agents repaired all surfaced defects in the printer, semantics, parser, passes, and checker, including some repairs that changed over a hundred lines of Lean proof. Each repair cost roughly $1 to $18 in tokens. No evidence of reward hacking was found in either Axon or the repairs.