Democratizing quantum formal verification: the path-sum way
summary
A verification tool called Cubri uses the path-sum symbolic execution format to represent quantum states as phased sums, claims compact proofs for many circuits and is complete+confluent for Clifford fragments (complete but not confluent for Clifford+Rz). Parameterized programs lift gate-to-gate rules to functions over registers, and rewriting rules (including a QFT rule and register substitution) live as explicit object-language commands. Implementation links to Why3 + SMT backends and verifies phase estimation and modular-addition with mostly automated proofs but still requires occasional human hints; measurement is handled by pass projection when patterns appear.
AI-written summary · about
chapters (18)
- 0:00Quantum formal verification intro
- 1:27Quantum programming challenges
- 4:16Static analysis importance
- 6:06Current verification tools
- 7:51Simpler verification needed
- 9:37Programs vs circuits
- 11:35Human-readable specs
- 14:07Path-sum explained
- 17:46Path-sum limitations
- 19:34Path-sum advantages
- 21:00Parameterized programs
- 23:06Deductive verification with Why3
- 26:01Rewriting theory update
- 27:51Quantum measurement handling
- 28:36Path-sum experiment
- 32:35Natural specs
- 34:23Future directions
- 34:47Q&A
related talks
21mToward Certified Quantum Programming
27mParameterized Verification of Quantum Circuits
15mToward A Quantum Programming Language for Higher Level Formal Verification
42mQuantum program analysis: Verification and Testing
22mEfficient Formal Verification of Quantum Error Correcting Programs
29mEfficiently Verifying Quantum Programs with Few T Gates
18mHybrid Path-Sums for Hybrid Quantum Programs
22mCoqQ: Foundational Verification of Quantum Programs