Formal Assurance for Railway Interlockings: Verifying Z3 SAT Proofs with Tseitin in Rocq
summary
Verifies Z3 SAT proof logs by checking RUP format steps and Tseitin transformations inside Rocq, extracting a fully verified proof checker and proving each RUP/Tseitin step correct by turning steps into tautologies. Handles railway interlocking encodings (7–10k safety properties), speeds verification from weeks of testing to ~1 hour and often 30 seconds for inductive cases, successfully checks huge proof logs from bounded model checking, and plans to extend the same technique to SMT rules.
AI-written summary · about
chapters (14)
- 0:00Formal assurance intro
- 0:25Formal methods for safety
- 1:29Trusting verification tools
- 2:52Z3 SAT proofs need certs
- 3:54RUP and Z3 proof structures
- 5:40Rocq correctness proofs
- 7:06Logical entailment in Rocq
- 8:33Evaluating proof checker
- 9:39Summary of independent verification
- 10:21Future steps for SMT logic
- 11:07Q&A: SMT certificate verification
- 12:11Q&A: Certification authorities
- 12:52Q&A: What proofs verify
- 13:54Q&A: Z3 vs DRA proof formats
related talks
19mA Correct-by-Construction Checker for Validation of Railway Data
01h 09mProofs - Practice 1
21mMechanised Hypersafety Proofs about Structured Data
22mTurning Catala into a Proof Platform for the Law
21mA Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
32mSatisfiability Modulo Custom Theories in Z3 (Tool Paper)
01h 08mTutorial on Proof Systems
19mAutomated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs