Tool Comparisons
How Fanal compares to existing quantum program verification and formalization tools across proof foundations, automation, and expressiveness.
Tool Overview
| Tool | Venue | System | Focus |
|---|---|---|---|
| CoqQ | POPL 2023 | Coq / MathComp | Labelled Dirac + qwhile + quantum Hoare logic |
| SQIR/VOQC | POPL 2021 | Coq / QuantumLib | Verified quantum circuit optimization |
| Lean-QuantumInfo | arXiv 2024 | Lean 4 / Mathlib | Quantum information theory (entropy, channels, GQSL) |
| QBricks | ESOP 2021 | Why3 / SMT | SMT-automated circuit-building program verification |
| Qafny | ECOOP 2024 | Dafny / Z3 | Separation logic for quantum programs |
| AutoQ 2.0 | TACAS 2025 | C++ standalone | Tree-automata-based automatic verification |
| D-Hammer | CAV 2025 | C++ / Mathematica | Automated labelled Dirac equational reasoning |
| Fanal | In development | Lean 4 / Mathlib | Foundational quantum program formalization & verification |
Proof Foundation
| Tool | Proof System | Trust Base | Proof Certificates |
|---|---|---|---|
| CoqQ | Coq / Calculus of Constructions | Coq kernel | Yes (Coq proofs) |
| SQIR/VOQC | Coq / Calculus of Constructions | Coq kernel | Yes (Coq proofs) |
| Lean-QuantumInfo | Lean 4 / CIC with quotients | Lean 4 kernel | Yes (Lean proofs) |
| QBricks | Why3 / First-order logic + SMT | Why3 + SMT solvers | Partial (SMT certificates) |
| Qafny | Dafny / Hoare logic + Z3 | Dafny verifier + Z3 | No |
| AutoQ 2.0 | None (algorithmic) | Unverified C++ implementation | None |
| D-Hammer | None (decision procedure) | Unverified C++ / Mathematica | None |
| Fanal | Lean 4 / CIC with quotients | Lean 4 kernel | Yes (Lean proofs) |
Automation
| Tool | Level | Mechanism | User Effort |
|---|---|---|---|
| CoqQ | Low | Manual Coq tactics | High — manual proofs |
| SQIR/VOQC | Low–Medium | Coq tactics + Ltac | High — manual proofs |
| Lean-QuantumInfo | Low | Lean tactics + Mathlib | High — manual proofs |
| QBricks | High (94%+) | SMT solvers (path-sum) | Low — mostly automatic |
| Qafny | High | Z3 SMT solver | Low — annotations only |
| AutoQ 2.0 | Very High | Tree automata algorithms | Minimal — fully automatic |
| D-Hammer | Very High | Decision procedure | Minimal — fully automatic |
| Fanal | Medium (developing) | dirac_eq tactic + D-Hammer integration | Medium — tactic-assisted |
Expressiveness
| Tool | Classical + Quantum | Loops | Measurement | Assertions | Compilation |
|---|---|---|---|---|---|
| CoqQ | Both | While loops | Yes | Labelled Dirac | No |
| SQIR/VOQC | Quantum only | No | Yes | Matrix-based | Yes (OpenQASM) |
| Lean-QuantumInfo | Quantum only | N/A | Channels | Operator algebra | No |
| QBricks | Both | Circuit-building | Limited | Path-sum | No |
| Qafny | Both | While loops | Yes | Separation logic | Yes (SQIR/OpenQASM) |
| AutoQ 2.0 | Quantum only | Bounded | No | Tree automata | No |
| D-Hammer | N/A | N/A | N/A | Labelled Dirac | No |
| Fanal | Both | While loops | Yes | Labelled Dirac | Planned |
Fanal's Unique Position
- Only Lean 4 project targeting quantum program verification
- Unique hierarchical access path register model with value-dependent labels
- D-Hammer integration path — combining automation with kernel-checked proofs
- Descriptive/Supportive code separation for AI-assisted development
- Specification-driven + AI-native development workflow
Detailed Comparisons
Fanal vs. CoqQ
POPL 2023 · Coq / MathComp
View comparison →Fanal vs. SQIR/VOQC
POPL 2021 · Coq / QuantumLib
View comparison →Fanal vs. Lean-QuantumInfo
arXiv 2024 · Lean 4 / Mathlib
View comparison →Fanal vs. QBricks
ESOP 2021 · Why3 / SMT
View comparison →Fanal vs. Qafny
ECOOP 2024 · Dafny / Z3
View comparison →Fanal vs. AutoQ 2.0
TACAS 2025 · C++ standalone
View comparison →Fanal vs. D-Hammer
CAV 2025 · C++ / Mathematica
View comparison →