###########################################################
____ _____ ____ _
/ __ \ / ____| | _ \ | |
| | | | (___ _ __ ___ ___| |_) | ___ _ __ ___| |__
| | | |\___ \| '_ \ / _ \/ __| _ < / _ \ '_ \ / __| '_ \
| |__| |____) | |_) | __/ (__| |_) | __/ | | | (__| | | |
\___\_\_____/| .__/ \___|\___|____/ \___|_| |_|\___|_| |_|
| |
|_|
###########################################################
A shared benchmark suite for checking quantum correctness claims — with honest evidence.
Quick start · Contribute · Tracks · Dashboard · Docs
Quantum software makes bold promises: this circuit is equivalent to that one, this error-correcting code fixes single-bit flips, this simulation step is accurate within a bound. Tools and papers evaluate these claims in incompatible ways — mixing up the statement, the input files, the checker output, and what was actually proved.
QSpecBench gives everyone the same vocabulary. Each benchmark is a small, reviewable package: what you claim, what would count as success, the files to check, and what evidence exists today — including what is still assumed or unverified.
| Piece | What it is | Where it lives |
|---|---|---|
| Claim | Plain-language statement of what should be true | README.md |
| Specification | Machine-readable contract (preconditions, postconditions, bounds) | spec.yaml |
| Artifacts | Circuits, Hamiltonians, code tables, source text | artifacts/ |
| Evidence | Checker output, proofs, simulations, review notes | evidence/ + notes/ |
| Trust boundary | What is proved, what is trusted, what is still open | README.md + spec.yaml |
Nothing is labeled "verified" unless a declared checker passed and the trust boundary says so.
flowchart LR
C["Claim\n(README)"] --> S["Specification\n(spec.yaml)"]
S --> A["Artifacts\n(circuits, models)"]
A --> E["Evidence\n(proofs, tools, review)"]
E --> T["Trust boundary\n(honest status)"]
Pick the area that matches your expertise. Each track has seed examples you can copy and adapt.
| Track | Focus | Examples |
|---|---|---|
| Algorithms | Protocols and quantum algorithms | Teleportation, Grover, phase estimation |
| Equivalence | Circuit and compiler transformations | Gate cancellation, QFT identity, Clifford simplification |
| QEC | Error correction and fault tolerance | Bit-flip code, stabilizer codes, surface code |
| Hamiltonian | Simulation, mappings, resource bounds | Hermiticity, Trotter steps, Jordan–Wigner |
| AI formalization | Turning informal claims into formal specs | Rubric-scored formalization tasks |
Browse the full list in the live dashboard.
We separate what you checked from what you hope to check later. Common evidence types:
| Type | Meaning |
|---|---|
| Proof assistant | Theorem checked by the Lean 4 kernel (CI runs lake build) |
| Equivalence checker | Circuits compared with tools such as QCEC |
| Solver certificate | SAT/SMT output verified by a certificate checker |
| Simulation | Numerical or stochastic check — supportive, not a proof |
| Human review | Expert review of derivations or rubrics |
| AI draft | Model-generated content — always untrusted until independently checked |
Simulation and LLM output can inform a benchmark; they do not by themselves make a claim proved.
Prerequisites: Python 3.10+, pip. Lean 4 is optional locally; CI installs it via elan when running proofs.
git clone https://github.com/fraware/QSpecBench.git
cd QSpecBench
# Install the CLI and dev tools
pip install -e ".[dev]"
# Validate every benchmark against the schema
qspecbench validate benchmarks/
# Inspect one benchmark end-to-end
qspecbench check-evidence benchmarks/equivalence/cnot_self_inverse_cancellation/
# Summary table of maturity and evidence
qspecbench status benchmarks/
qspecbench dashboard benchmarks/ --out docs/status.md
# Run the test suite
pytestLean proofs (optional, for contributors adding machine-checked theorems):
cd lean && lake buildWe welcome benchmarks, better evidence, documentation fixes, and new checker adapters. You do not need a finished proof to open a pull request — a clear claim with honest status is a valuable contribution.
- Read Adding a benchmark and CONTRIBUTING.md.
- Copy
benchmarks/_template/into the right track folder. - Use a nearby reference scaffold as a style guide (each demonstrates the format; none yet proves its full headline claim):
- Algorithms →
teleportation_preserves_state_up_to_pauli_correction - Equivalence →
cnot_self_inverse_cancellation - QEC →
three_qubit_bit_flip_code_corrects_one_x - Hamiltonian →
small_fermionic_hamiltonian_is_hermitian - AI formalization →
formalize_no_cloning_statement
- Algorithms →
- Validate locally:
qspecbench validate benchmarks/<track>/<your_id>/ - Open a PR with the benchmark issue template.
Maturity is scoped: it separates "this benchmark has some checked evidence" from "the full informal headline claim is proved".
| Level | What we expect |
|---|---|
| seed | Claim, spec, and trust boundary — proof optional |
| usable | Complete card, runnable artifacts, evidence path, CI green |
| reference_scaffold | Passing CI plus at least one checked-evidence obligation, but the headline claim is only partially checked. Demonstrates the evidence format and trust-boundary discipline. |
| reference_contract | Like reference_scaffold, for benchmarks whose checked evidence is a declared contract (e.g. a resource or error-bound contract) rather than a proof of the bound itself. |
| reference_artifact | Like reference_scaffold, where the checked evidence is artifact-structural (e.g. stabilizer commutation) rather than a proof of the headline claim. |
| reference_claim | The headline claim is fully proved: every required obligation passes, all required evidence exists and passes, and headline_claim_status is checked. |
| deprecated | Retained for history; README explains why. |
Most current entries are reference scaffolds: they demonstrate the QSpecBench evidence format and
trust-boundary discipline, but they do not yet prove the full informal headline claim. A benchmark is
only reference_claim when its claim_scope / proved_scope obligations are all checked.
Promotion is documented in reference benchmarks and reviewed per GOVERNANCE.md.
- Improve an existing benchmark's evidence or documentation
- Add or extend adapters for new checkers
- Extend the Lean library under
lean/QSpecBench/ - Fix issues labeled
good first issue
Be precise about verification claims: say what was checked and with which tool.
QSpecBench versions the schema, the tooling, and the benchmark corpus separately so that a change in one does not imply maturity in the others. See versioning.
| Component | Version |
|---|---|
Schema (qspecbench_version) |
0.3 |
Tooling (qspecbench CLI / Lean lib) |
0.2.0 |
| Corpus (benchmark suite) | 0.2.0 |
| Release tag | v0.2.3 |
Release honesty (v0.2.3): tag v0.2.3 (49e8899) delivered the first six artifact_bound_reference_claim
kernel bridges with dual named reviews and hash anchor chain, schema 0.3 (elaborator/AST authority fields), and
ast_authority: lean_mirror on kernel-checked codegen-trace bridges. The working tree has since expanded ABRC
(see status block / docs/status.md); most benchmarks remain reference scaffolds.
Only reference_claim and artifact_bound_reference_claim entries assert a checked headline under declared scope.
See versioning.md and definition_of_completion.md.
Even when the definition of completion is met, QSpecBench remains a scoped research benchmark — not a complete quantum formal-verification standard. The following are permanent trust boundaries; they are not unfinished promotions:
| Item | Disposition |
|---|---|
unbounded_all_codes_mwpm |
not_applicable; Lean impossibility note (unbounded_all_codes_mwpm_infeasible_open_ended) |
Device hardware_semantics / device_fidelity / pulse_schedule_semantics |
Stay not_checked; ISA-layer checks are separate |
Unnormalized denotateOps3C Toffoli equality |
Out of scope (wrong semantics) |
| QBricks / ZX | Adapters exist; still not a complete FV standard |
| Rocq / Isabelle skip stubs | Never counted as checked evidence |
| Full industrial Stim/Blossom all-codes | Outside declared universe stim_repetition_memory_odd_d_le_7_R_eq_d_p0p01 |
Details: research_tracks.md, definition_of_completion.md.
Honest status: most entries are reference scaffolds demonstrating the evidence format. 9
benchmarks are reference_claim and 10
are artifact_bound_reference_claim under declared scope.
| Benchmarks | 50 across 5 tracks |
| Reference scaffolds (any scoped reference level) | 42 |
With headline claim checked (reference_claim + artifact_bound_reference_claim) |
19 |
| With any checked evidence | 46 |
| Manifest-checked theorem bindings | 4 |
| Python denotation consistency checks | 1 |
| Kernel-checked codegen-trace bridges | 1 |
| Coq/Rocq/Isabelle (optional CI) | excluded from default maturity counts |
| CI | Schema validation, evidence checks, Lean proofs, verify-bridge, bridge-metadata verify, circuit equivalence (QCEC) |
Details and per-benchmark breakdown: dashboard (regenerate with qspecbench dashboard benchmarks/ --out docs/status.md).
| Topic | Guide |
|---|---|
| Core concepts | Claim model |
spec.yaml fields |
Schema reference |
| Evidence types and checkers | Evidence model |
| What is proved vs assumed | Trust boundaries |
| When “community-grade” applies | Definition of completion |
| Scientific leftovers + permanent N/A | Research tracks |
| Lean setup | Lean setup |
| Schema v0.3 migration (active) | Migration guide |
| Schema v0.2 migration (historical) | Migration guide |
MIT — use, modify, and contribute freely.