Embedding Quantum Program Verification into Dafny
summary
QafnyC compiles quantum program verification into Dafny and then down to executable circuits (via Sqir/OpenQASM), implementing a type-driven verifier that introduces AA and En types plus nor/had/amplitude types to express amplitude structure. The system automatically translates compact QafnyC specs into large Dafny checks (Grover: ~23 Qafny lines → ~230 Dafny lines), produces developer feedback and debugging, and successfully verifies 37 quantum programs — claimed as the largest verified corpus so far. Type-guided automation drives proof generation and scales to amplitude-amplification and Shor/Grover families.
AI-written summary · about
chapters (11)
- 0:00Quantum verification intro
- 1:25Why quantum computing matters
- 2:30Quaffne and Kofnec proofs
- 3:56Quantum states basics
- 4:37Kofnec verification design
- 6:25Daphne verification with Quaffne
- 7:11Quantum types in Kofnec
- 8:15Grover’s algorithm
- 9:40Verified quantum programs
- 10:43Future research
- 11:24Q&A
related talks
21mVerified VCG and Verified Compiler for Dafny
19mLean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean
01h 02mLanguage Design meets Verifying Compilers
03mAttempts to design hardware using dafny
22mAn Automata-based Framework for Quantum Circuit Verification
17mQGAT: A Generate-and-Test Paradigm for Quantum Circuits
18mVerifying the Fisher-Yates Shuffle Algorithm in Dafny
16mCompiling and Running High-level Quantum Programs