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: B