A proof should break when the program changes
How Auths Proof translates its production Rust authority kernel through Charon and Aeneas, refines it against a readable Lean specification, and makes semantic drift fail CI.
Lean
1 entry exploring this thread.