Spoq: Scaling Machine-Checkable Systems Verification in Coq
summary
Spoq produces machine-checkable Coq proofs by compiling unmodified C to LLVM IR and then translating LLVM into Coq with full C semantics so macros, inline assembly and compiler directives need no manual removal. It applies a rule-based program-structure reconstruction and automated layered spec generation and refinement proofs to shrink human effort. Evaluation verifies an unmodified multiprocessor KVM hypervisor and reports about 70% less proof effort than prior manual proofs.
AI-written summary · about
chapters (9)
- 0:00Spoq and system verification
- 3:16Traditional verification challenges
- 3:58Spoq’s formalizing approach
- 5:49Rule-based formal reconstruction
- 6:54Automating specs and proofs
- 8:21Simplifying to intermediate specs
- 10:04Applying simplification rules
- 11:28Spoq vs existing tools
- 12:55Summary and future
related talks
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
42mMetaCoq as a tool to prevent future unsoundness in Coq
23mVellvm: Formalizing the Informal
46mMechanizing Abstract Interpretation
22mVerified Programming of Turing Machines in Coq
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
54m10-Year Most Influential Paper Talk: Coq: the world's best macro assembler?
24mCode Extraction from Coq to ML-like languages