About QBricks
Automated verification of quantum circuit-building programs using Why3 and SMT solvers. Achieves 94%+ automated proof rate through path-sum semantics. Verified Shor’s order-finding circuit.
Verification Paradigm
| Aspect | QBricks | Fanal |
|---|---|---|
| Approach | Deductive verification with SMT solvers | Foundational interactive theorem proving |
| Logic | Hybrid Quantum Hoare Logic (HQHL) embedded in Why3 | Planned: Quantum Hoare Logic over labelled Dirac assertions |
| Proof discharge | Proof obligations sent to SMT solvers (Alt-Ergo, CVC4, Z3) | Proofs checked by Lean 4 kernel; planned D-Hammer tactic |
| Workflow | Write code + specs -> HQHL generates obligations -> SMT solvers discharge | Write definitions + state theorems -> prove interactively with tactics |
Semantics
| Aspect | QBricks | Fanal |
|---|---|---|
| Core representation | Higher-Order Path-Sums (HOPS) — symbolic decomposition of unitaries | Concrete matrices via Mathlib with Dirac notation layer |
| Scalability | Avoids matrix explosion; symbolic path-sum representation | Matrices grow exponentially; mitigated by symbolic Dirac layer |
| Compositionality | HOPS closed under sequential/parallel composition | Dirac terms compose; matrix semantics via tensor product |
| Register management | Contiguous blocks of qubits; bit-vectors | Hierarchical access-path labels |
| Parametricity | Native — HOPS terms reference DSL variables | Supported via Lean variables and CExpr |
| Partiality | Uses bottom element for invalid circuits | Option-returning eval for dynamic premises |
Automation Level
| Aspect | QBricks | Fanal |
|---|---|---|
| Deutsch-Jozsa | 72 obligations, >84% automated | Dirac encoding available; full verification planned |
| Grover | 698 obligations, >95% automated | Not yet verified |
| QFT | 62 obligations, >85% automated | Not yet verified |
| QPE | 423 obligations, >93% automated | Not yet verified |
| Shor-OF | 1522 obligations, >95% automated | Final verification goal (planned) |
| Overall | 2777 obligations total, >94% automated | Automation under development (D-Hammer integration) |
Expressiveness
| Aspect | QBricks | Fanal |
|---|---|---|
| Circuit description | First-class via QBricks-DSL (SEQ, PAR, ANC, CTL, invert) | Planned via Program module |
| Dirac notation | Indirect (via HOPS path-sums) | First-class, multi-layered (Dirac + LDirac) |
| Classical computation | Integers, booleans, iteration | CExpr with data types, variables, arithmetic |
| Measurement | Not a language construct; probabilistic reasoning via specs | Planned in Program module |
| Classical control | Not supported | Planned in Program module |
| Specification language | QBricks-Spec (first-order predicate logic) | Planned Assertion module (orthomodular lattice-based) |
Trust Base
| Aspect | QBricks | Fanal |
|---|---|---|
| Core TCB | Why3 + SMT solvers (Alt-Ergo, CVC4, Z3) | Lean 4 kernel (~10K lines of C++) |
| TCB size | Large (Why3 + multiple SMT solvers) | Small (Lean 4 kernel) |
| Axioms | 32 axiomatic definitions for math structures | Lean standard axioms only |
| Proof certificates | SMT solver output (not independently checkable) | Lean kernel-checked terms |
| Logic soundness | Claimed, not mechanized | Would be mechanized within Lean |
| Math library | 14,000+ lines WhyML with axioms | Mathlib (kernel-verified, no custom axioms) |
Case Studies
| Aspect | QBricks | Fanal |
|---|---|---|
| QFT | Verified parametrically — 65 LOC, 62 proof obligations | Not yet verified |
| QPE | Verified parametrically — 319 LOC, 423 proof obligations | Not yet verified |
| Shor-OF | Verified parametrically — 809 LOC, 1522 proof obligations, includes complexity proof | Final verification goal |
| Grover | Verified parametrically — 416 LOC, 698 proof obligations | Not yet verified |
| Deutsch-Jozsa | Verified parametrically — 53 LOC, 72 proof obligations | Dirac encoding available |
| Development effort | 1.5 person-years for framework + 1-10 person-days per algorithm | Active development with AI-assisted workflow |
Strengths and Trade-offs
| Aspect | QBricks | Fanal |
|---|---|---|
| Automation | 94%+ proof obligations discharged automatically | Automation under development; aims for kernel-checked push-button proofs |
| Complexity reasoning | Can reason about circuit size (polynomial gate count) | Not yet addressed |
| Foundational assurance | Pragmatic (cross-checking via multiple SMT solvers) | Strong (every proof independently verifiable by Lean 4) |
| Ecosystem | WhyML (smaller community) | Lean 4 + Mathlib (growing community) |
Summary: Key Differences
| Aspect | QBricks | Fanal |
|---|---|---|
| Proof System | Why3 / First-order logic + SMT | Lean 4 / Dependent type theory |
| Trust Base | Why3 + SMT solvers (not kernel-checked) | Lean 4 kernel (fully verified) |
| Automation | 94%+ automatic via SMT | Tactic-assisted, D-Hammer integration |
| Semantics | Path-sum semantics | Labelled Dirac notation |
| Expressiveness | Circuit-building programs | General classical-quantum programs |