You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Formally Verified Quantum Computing: a catalog of the code
A maintained map of public repositories whose purpose is machine-checked
verification of quantum programs, circuits, protocols, error-correcting codes,
or the mathematics underneath them — with the proof system each is written in,
where it came from, and when it was last touched.
What this is. The Quantum PL & Verification Bibliography
maps the literature of this field. This catalog is the companion piece: it
maps the artifacts — the actual code. Each entry records the repository, the
proof system, what it verifies, the associated paper, the licence, and a
build observation (whether the code built on our machine on a stated date).
How to read the build column.yes means the project built in the
environment recorded on its page, on the date recorded there. no means it did
not build in that environment — which is a statement about our machine on that
day, not a judgment of the project: the most common cause is simply that a
project targets a different prover version than the one we had installed. Where
the logs showed that we never gave a project the environment it declares (an
unsatisfiable dependency solve, a prover generation it predates, a distribution
we could not download), the record says not-attempted with the reason, rather
than blaming the project for our setup. Where a project ships its own build
recipe, we use it. Corrections are welcome: if your project builds and we say
otherwise, tell us what we got wrong and we will re-run it and fix the record.
What this is not. Not a ranking, not an audit, not an assessment of anyone's
proofs. Descriptions state what a project does, never how good it is. Entries
are sorted by proof system and then alphabetically. A dormant or archived
status is a fact about commit dates, nothing more; a builds: no is a fact
about our machine on the recorded date, nothing more.
Inclusion criteria. In scope: any public repository whose purpose is
machine-checked verification of quantum programs, circuits, protocols,
error-correcting codes, or their underlying mathematics, in a proof assistant
(Coq/Rocq, Lean, Isabelle/HOL, Why3, Dafny, F*, …). Foundational libraries
built as quantum substrate are included and tagged role: library.
Automated and SMT-backed formal tools appear in their own section.
Out of scope: simulators, SDKs, and compilers with no formal-verification
component. Inactive projects stay listed, marked by status.
Corrections and additions are welcome — please open an issue or a PR; an
entry is one small YAML file (see docs/SCHEMA.md).
Maintainers: if anything about your project is described inaccurately, tell us
and we will fix it.
Prior work. This catalog would be pointless without the surveys that
mapped the field first: the
Quantum PL & Verification Bibliography;
Chareton, Bardin, Lee, Valiron, Vilmart, Xu,
Formal Methods for Quantum Programs: A Survey (arXiv:2109.06493);
Lewis, Soudjani, Zuliani,
Formal Verification of Quantum Programs: Theory, Tools and Challenges
(arXiv:2110.01320, DOI:10.1145/3624483);
and A Review of Formal Methods in Quantum-Circuit Verification (Electronics, 2026).
Those map the papers; this maps the code.
This catalog was suggested by Robert Rand
(University of Chicago), whose feedback also shaped its structure.
Mathematical infrastructure whose stated purpose is broader than quantum
(for example the Isabelle entries Complex Bounded Operators and Hilbert Space
Tensor Product) is included only where it is the acknowledged substrate of
cataloged quantum developments, and its entry says so. See
docs/NOT_INCLUDED.md for everything we know about and
deliberately did not list — paper-only tools, out-of-scope software, and
related resources — so that "missing" is distinguishable from "not found".
A foundational verification framework for quantum programs: a quantum Hoare logic proved sound against a denotational semantics built on MathComp, with case studies including HHL, Grover, QPE, and hidden subgroup.
A Coq formalization of a Hoare logic for local reasoning about classical-quantum programs, with verified examples including Shor's algorithm, HHL, and order finding.
A Coq formalization (in the Hybrid framework) of the metatheory of the Proto-Quipper quantum programming language, proving type soundness in a linear specification logic.
A Coq prototype of an expectation-based quantum Hoare logic with a soundness proof and verified examples including Deutsch, Grover, GHZ, and teleportation.
A Coq library of linear algebra, complex numbers, and matrix infrastructure used as the shared foundation of the inQWIRE developments (QWIRE, SQIR/VOQC, VyZX).
A small quantum intermediate representation deeply embedded in Coq, with semantics used to prove quantum programs (Grover, QPE, GHZ, teleportation) correct.
Coq formalizations of metatheory for the vectorial and algebraic-linear lambda-calculi, quantum-motivated calculi in the Arrighi-Diaz-Caro-Valiron line.
A tool for formal verification of quantum error-correcting programs: a program logic formalized in Coq on top of CoqQ, paired with a Python/SMT automated verifier for fault-tolerant scenarios.
An interactive textbook on verified quantum computing in Coq, in the style of Software Foundations, covering matrix semantics, Deutsch's algorithm, and quantum teleportation.
An early-stage Lean 4 formalization of categorical quantum mechanics: dagger categories with projections, isometries, and unitaries, and standard gates proved unitary.
A Mathlib-based formalization of quantum information theory in Lean 4: distances, entropies, and capacities, with the Generalized Quantum Stein's Lemma as a guiding result.
An educational Lean 4 game whose levels formalize superposition, measurement probabilities, and mutually unbiased bases, culminating in a verified idealized model of the BB84 protocol.
A Lean 4 formalization over Mathlib of Hilbert-space foundations for quantum computing: qubit states, standard gates, density operators, tensor products, and partial trace.
A Lean 4 formalization of operator-algebraic quantum theory, including the GNS construction, the Gelfand-Naimark theorem, the bicommutant theorem, and von Neumann entropy results including strong subadditivity.
A Lean 4 formalization of a three-qubit quantum computer with a QWhile-style language and Hoare logic, including a verified Hoare triple for the Deutsch-Jozsa algorithm.
A formalization of complex Hilbert spaces and bounded operators, the mathematical foundation used by the quantum registers, Kraus maps, and qrhl-tool developments.
A formalization of the compressed-oracle methodology for reasoning about quantum random oracles in cryptographic proofs, including hardness of zero-finding and collision-finding.
A formalization of tensor products of Hilbert spaces, operators, and von Neumann algebras, including the infinite-dimensional case, underlying the quantum registers and Kraus maps entries.
A matrix-based library for quantum computation and quantum information formalizing the no-cloning theorem, quantum teleportation, the Deutsch and Deutsch-Jozsa algorithms, and the quantum Prisoner's Dilemma.
A formalization of quantum channels as Kraus maps over arbitrary (not necessarily finite-dimensional) Hilbert spaces, with their equivalence to completely positive maps.
A formalization of the One-way to Hiding theorem, a foundational lemma for security proofs against quantum adversaries in the quantum random oracle model.
A formalization of quantum projective measurements based on spectral theory, and of the CHSH inequality showing quantum mechanics admits no local hidden-variable model.
A formalization of the syntax and denotational semantics of a simple quantum program model with a quantum Hoare logic proved sound and complete for partial correctness, applied to verify Grover's algorithm.
An interactive proof assistant for quantum relational Hoare logic, built on Isabelle/HOL, for verifying the security of quantum and post-quantum cryptographic protocols.
A generic theory of registers (mutable parts of program state) instantiated for classical and quantum settings, with register composition and an analysis of quantum teleportation.
A formalization of density matrices, projective measurements, and Tsirelson's proof that the maximum quantum violation of the CHSH inequality is 2*sqrt(2).
An ACL2(r) interpreter for quantum-circuit netlists with states as vectors and gates as unitaries, including a proof of correctness of the quantum teleportation circuit.
An Agda formalization (in agda-categories) of completeness and expressivity results for the reversible language Pi extended with square roots, capturing unitary quantum computing.
An interactive theorem prover for string diagrams, representing morphisms as cospans of hypergraphs, used for equational reasoning in the ZX-calculus and quantum software line.
A diagrammatic proof assistant for equational reasoning about string diagrams such as the ZX-calculus, with user-defined equational theories and rewrite strategies.
A HOL Light framework for verifying optical quantum gates and circuits, including CNOT, Mach-Zehnder, a quantum full adder, and a Grover oracle circuit, with tensor-product infrastructure and a decision procedure.
A deductive verification framework for circuit-building quantum programs in Why3, with proof obligations discharged largely automatically by SMT solvers; verified developments include Deutsch-Jozsa, QPE, Grover, and Shor order-finding.
A quantum-program verifier that translates quantum operations to classical array operations in a separation-logic style, discharging proofs through Dafny; verified components include quantum walk, Grover, and Shor.
An equivalence checker for quantum circuits combining decision-diagram and ZX-calculus techniques, used to verify compilation results including Qiskit flows.
A verification tool for quantum-network entanglement-distribution protocols based on a sound and complete equational theory in the Kleene-algebra family.
A prototype tool for symbolic execution of quantum programs using symbolic stabilizer states, applied to debugging quantum error correction programs at scale.
Symbolic model checking of quantum circuits in Maude with Dirac-notation symbolic states, checking teleportation, superdense coding, secret sharing, entanglement swapping, and network coding.
An assistant tool for formal verification of partial correctness of nondeterministic quantum programs, using numerical methods over quantum Hoare logic.
A Haskell toolkit for quantum circuit analysis based on the sum-over-paths representation, supporting functional verification, equivalence checking, and optimization.
A tool that synthesizes quantum-circuit optimizers whose rewrite rules are automatically verified via polynomial-identity-testing equivalence, per gate set.
A push-button verification toolkit for the Qiskit quantum compiler that verified 44 of 56 compiler passes against semantics preservation, using Z3 automation over Coq-proved circuit rewrite rules.
A tool for automated symbolic verification of quantum programs against first-order specifications, via an SMT encoding of a symbolic quantum program model.
A C++ framework for synthesizing and optimizing quantum circuits that includes a formal equivalence checker based on stabilizer-tableau reduction with an exact tensor-contraction fallback.
An automata-based quantum circuit verifier using Hoare-style pre- and post-conditions represented as tree automata; version 2.0 extends to quantum programs with measurement, branching, and loop invariants.
A verifier for parameterized quantum circuits using synchronized weighted tree automata, providing automatic relational verification and equivalence checking.
A Python library for quantum circuit rewriting and optimisation using the ZX-calculus, including equivalence checking by diagram rewriting.
About
A maintained catalog of public repositories that machine-check quantum programs, circuits, protocols, and error correction in proof assistants — with the proof system, what each verifies, and a dated build observation.