About Qafny
Quantum program verification using separation logic in Dafny. Automated by Z3. Programs can be compiled to SQIR/OpenQASM. Verified Shor’s algorithm in 36 LOC, 36.3s.
Verification Approach
| Aspect | Qafny | Fanal |
|---|---|---|
| Pipeline | Qafny source -> type-guided proof system -> compiled to SEP -> Dafny/Z3 discharge | Lean 4 definitions + theorems -> interactive/tactic proofs -> kernel-checked |
| Soundness | Type soundness and proof system soundness/completeness proved in Coq | Proofs are kernel-checked by construction in Lean 4 |
| Automation strategy | Escape to classical verification infrastructure (Dafny/Z3) | Build certified automation within Lean 4's type theory |
| Metatheory | Verified in Coq (separate from implementation) | Verified in Lean 4 (same framework as implementation) |
Quantum State Encoding
| Aspect | Qafny | Fanal |
|---|---|---|
| Encoding style | Operational: arrays of basis-kets manipulated by type-guided rewrites | Denotational: Dirac notation terms with matrix semantics |
| State types | Nor (computational basis), Had (superposition), EN (entanglement) | DiracSort: scalar, ket, bra, operator with DataType parameters |
| Entanglement tracking | Loci partition quantum heap into entanglement groups | LDirac layer with disjointness premises on register atoms |
| No-cloning enforcement | Flow-sensitive type system with frozen basis stacks | Planned at type system level |
| Mixed states | Not supported (pure states only) | Potentially supported via density matrix semantics |
Automation
| Aspect | Qafny | Fanal |
|---|---|---|
| State rewrites | Automatic: type-guided canonical state transformations | dirac_eq tactic for certified equational reasoning |
| Predicate transformers | F (freeze), U (unfreeze), M (measure) — automatic | Planned: assertion manipulation tactics |
| Backend | Dafny + Z3 SMT solver for final proof discharge | Lean 4 kernel checks every proof step |
| User effort | Very low: provide program + pre/postconditions + loop invariants | Medium: tactic-assisted proofs (automation under development) |
| Example: Shor's | 36.3 seconds, 36 LOC | Final verification goal (with foundational proof) |
Programming Language
| Aspect | Qafny | Fanal |
|---|---|---|
| Status | Complete, implemented language | Design/early implementation phase |
| Classical constructs | let-binding, sequential composition, classical if-else | CExpr layer with variables, arithmetic, booleans |
| Quantum operations | H, QFT, QFT^-1, OQASM oracles, dis, reduce | Planned: general quantum operations |
| Measurement | let x = measure(y) in e with probability tracking | Planned in Program module |
| Quantum conditionals | if (b) e where b is Boolean guard on qubits | Planned in Program module |
| Variable kinds | C (classical), M (measurement result), Q (quantum array) | UnifiedType: ctype, dtype, qtype |
Assertion Language
| Aspect | Qafny | Fanal |
|---|---|---|
| Form | State-mapping predicates: kappa |-> q with separating conjunction * | Planned: labelled Dirac notation with orthomodular lattice structure |
| Expressiveness | Specialized for automation; describes pure-state arrays | General Dirac assertions; can express mixed states, projections, Loewner order |
| Predicate manipulation | F, U, M transformers designed for type-guided proof rules | Planned: proof automation for assertion implication |
| Naturalness | Custom notation tailored for Qafny's type system | Standard Dirac notation familiar to physicists |
Trust Base
| Aspect | Qafny | Fanal |
|---|---|---|
| Layer 1 | Coq proofs — type soundness, proof system soundness/completeness | Lean 4 kernel — small, well-studied type checker |
| Layer 2 | Qafny-to-SEP compilation — correctness is future work | Mathlib — community-maintained, continuously checked |
| Layer 3 | Dafny verifier + Z3 SMT solver — trusted | Fanal definitions — syntax, typing, semantics in Lean 4 |
| Extra axioms | Periodical theorems for Shor's added as Dafny assumptions | None beyond Lean standard axioms |
| Overall | Large trust base with implementation gap | Small trust base with all proofs kernel-checked |
Case Studies
| Aspect | Qafny | Fanal |
|---|---|---|
| GHZ | Verified: 14.2s, 16 LOC, <1 day effort | Not yet |
| Deutsch-Jozsa | Verified: 8.3s, 13 LOC, <1 day effort | Dirac encoding available |
| Grover's Search | Verified: 26.7s, 27 LOC, 2 days effort | Not yet |
| Shor's Algorithm | Verified: 36.3s, 36 LOC, 5 days effort | Final verification goal |
| Quantum Walk | Verified: 43.1s, 49 LOC, 3 days effort | Not yet |
Compilation
| Aspect | Qafny | Fanal |
|---|---|---|
| To quantum circuits | Qafny -> SQIR -> OpenQASM 2.0 | Future work |
| To classical code | Dafny -> C#/Java/PHP (for classical parts) | Not planned |
| Compilation correctness | Theorem 7 (tested, not fully proved) | N/A yet |
Summary: Key Differences
| Aspect | Qafny | Fanal |
|---|---|---|
| Proof System | Dafny / Hoare logic + Z3 | Lean 4 / Dependent type theory |
| Trust Base | Dafny verifier + Z3 (unverified) | Lean 4 kernel (fully verified) |
| Assertion Logic | Separation logic for quantum | Labelled Dirac notation + Hoare logic |
| Automation | Highly automated via Z3 | Tactic-assisted, D-Hammer integration |
| Compilation | Compiles to SQIR / OpenQASM | Compilation planned |