Inside Axiom’s Verification Kernel: BMC, UAP, Lean Replay, and the Proof Vault

When people hear “formal verification”, they imagine a single solver run that prints Verified . That’s not what Axiom is optimizing for. Axiom is built around one requirement: if you say something is verified, you must be able to reproduce that claim deterministically —including the exact query shape, the exact counterexample (if SAT), and the exact Lean replay (if promoted to safe). 1) BMC Core: Bounded Models, Not Hand-Wavy Guarantees The BMC core is the “boundary model” layer of the engine: i