Verified Quantum Computing

The VQC Lab builds the software stack — languages, systems, and formal verification — for quantum computers, so that quantum programs can be trusted to do what they claim.

View publications

01About

Trustworthy software for quantum machines

We design programming languages, compilers, and operating systems for quantum computers — and use formal verification to machine-check that these systems are correct, from circuit-level compilers to end-to-end resource estimates for landmark quantum algorithms.

The VQC (Verified Quantum Computing) Lab is led by Prof. Runzhou Tao in the Department of Computer Science at the University of Maryland.

Meet the team

02Research

The quantum software stack, verified.

  • 01

    Quantum Programming Languages

    Languages and compilers that make it easier to write, optimize, and reason about quantum programs.

  • 02

    Formal Verification

    Machine-checked proofs of correctness for quantum compilers, algorithms, and quantum error-correcting codes.

  • 03

    Quantum Systems & OS

    Operating systems, hypervisors, and runtime infrastructure that manage quantum hardware and virtual machines.

  • 04

    Quantum Algorithms

    End-to-end verified implementations and resource estimates for algorithms such as Shor's algorithm.

  • 05

    Quantum Error Correction

    Formal models of stabilizer and CSS codes, with automated, SAT-assisted verification of code properties.

  • 06

    Teaching

    Courses on quantum computing and quantum software systems for undergraduate and graduate students.

Published at

All publications →
  • OSDI
  • SOSP
  • PLDI
  • POPL
  • FOCS
  • SODA
  • PNAS
  • ITCS
  • APPROX

03Projects

Open source, formally verified.

All projects
f(x) = 7x mod 15 repeats with period r = 4

Lean 4Quantum Algorithms

ForShor

A formal verification of Shor's algorithm in Lean 4, including a machine-checked end-to-end resource estimation.
Distance-3 surface code, a CSS code: 9 data qubits, 8 stabilizers

Lean 4Error Correction

Lean-QEC

End-to-end formalization of Quantum Error Correction in Lean, from qubits and the Pauli group to stabilizer codes.
y² = x³ + 7, secp256k1’s curve drawn over the reals: the chord rule for P + Q

Lean 4Security

ShorECDLP

A verified, end-to-end resource estimate for Shor's algorithm on the elliptic-curve discrete-logarithm problem underlying Bitcoin's ECDSA.

04News

Latest updates

All news
  1. Launching ecdsa.fail/lean with Yukon A leaderboard for quantum attacks on Bitcoin's elliptic curve where every result is backed by a machine-checked Lean proof.
  2. “Quantum Virtual Machines” accepted to OSDI 2025 Our paper on quantum virtual machines, with collaborators at Columbia University, was accepted to the 19th USENIX Symposium on Operating Systems Design and Implementation.
  3. New verified quantum algorithms projects underway The lab released ForShor, ShorECDLP, and Lean-QEC — ongoing efforts to formally verify quantum algorithms and error-correcting codes in Lean and Rocq.
  4. Runzhou Tao joins UMD as Assistant Professor Runzhou Tao joined the Department of Computer Science at the University of Maryland as an Assistant Professor and a Fellow at QuICS.