Open-source, formally verified software for quantum computing — from algorithms and error correction to compilers and systems. All projects are developed openly on github.com/VerifiedQC.
A formal verification of Shor's algorithm in Lean 4, including its resource estimation. The development verifies an implementation of order finding built on fast (Toom–Cook) multiplication, from a high-level gate language down to a low-level abstract machine, and proves the whole circuit uses only O(n2+ε) gates.
An end-to-end formalization of Quantum Error Correction in Lean, from basic quantum computing concepts (qubits, quantum states, the Pauli group) to stabilizer and CSS codes, including a SAT-assisted pipeline for verifying code properties like code distance.
A verified, end-to-end resource estimate for Shor's algorithm on the elliptic-curve discrete-logarithm problem (ECDLP) over secp256k1 — the quantum attack underlying Bitcoin's ECDSA. Combines machine-checked functional correctness with a machine-checked Toffoli gate-count bound for the very same circuit.
A Hoare-style program logic for LOCC (Local Operations and Classical Communication) quantum protocols — the language, its operational semantics, the assertion language, and the proof system — fully mechanized in the Rocq Prover, with machine-checked soundness and zero admits.
Tooling for generating and verifying optimized instruction tables used in fast modular arithmetic for Shor's algorithm implementations, with an automated verifier and a public benchmark leaderboard.
The lab is continually starting new projects in verified quantum systems and software. Follow along or get involved on GitHub.
Interested in contributing? Most of our projects welcome outside contributors — check each repository's issues, or reach out directly.
Email Prof. Tao