VQC LabProjects

Projects

Open-source, formally verified software for quantum computing — from algorithms and error correction to compilers and systems.

github.com/VerifiedQC

  1. f(x) = 7x mod 15 repeats with period r = 4 — the period Shor's algorithm finds

    P / 01Active

    ForShor

    Lean 4Quantum Algorithms

    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.

    Repository
  2. Distance-3 surface code, a CSS code: 9 data qubits, 8 stabilizers

    P / 02Active

    Lean-QEC

    Lean 4Quantum Error Correction

    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.

    Repository arXiv
  3. y² = x³ + 7, secp256k1’s curve drawn over the reals: the chord rule for P + Q

    P / 03Active

    ShorECDLP

    Lean 4Quantum AlgorithmsSecurity

    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.

    Repository
  4. Teleportation, an LOCC protocol: Alice's measurements reach Bob only as classical bits

    P / 04Active

    LocQHL

    RocqProgram Logic

    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.

    Repository
  5. r · 2c mod 21: highlighted cells equal 1, where r is the inverse of 2c

    P / 05

    Shor Table Optimization

    Lean 4Optimization

    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.

    Repository
  6. An open slot in the circuit

    P / 06

    More on the way

    The lab is continually starting new projects in verified quantum systems and software. Follow along or get involved on GitHub.

    github.com/VerifiedQC

Interested in contributing?

Explore each repository's issues and contribution guidance on GitHub.

Explore repositories