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.
The VQC (Verified Quantum Computing) Lab is led by Prof. Runzhou Tao in the Department of Computer Science at the University of Maryland. We design programming languages, compilers, and operating systems for quantum computers, and we 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.
Languages and compilers that make it easier to write, optimize, and reason about quantum programs.
Machine-checked proofs of correctness for quantum compilers, algorithms, and quantum error-correcting codes.
Operating systems, hypervisors, and runtime infrastructure that manage quantum hardware and virtual machines.
End-to-end verified implementations and resource estimates for algorithms such as Shor's algorithm.
Formal models of stabilizer and CSS codes, with automated, SAT-assisted verification of code properties.
Courses on quantum computing and quantum software systems for undergraduate and graduate students.
Our paper on quantum virtual machines, with collaborators at Columbia University, was accepted to the 19th USENIX Symposium on Operating Systems Design and Implementation.
The lab released ForShor, ShorECDLP, and Lean-QEC — ongoing efforts to formally verify quantum algorithms and error-correcting codes in Lean and Rocq.
Runzhou Tao joined the Department of Computer Science at the University of Maryland as an Assistant Professor and a Fellow at QuICS.
A formal verification of Shor's algorithm in Lean 4, including a machine-checked end-to-end resource estimation.
View on GitHub →End-to-end formalization of Quantum Error Correction in Lean, from qubits and the Pauli group to stabilizer codes.
View on GitHub →A verified, end-to-end resource estimate for Shor's algorithm on the elliptic-curve discrete-logarithm problem underlying Bitcoin's ECDSA.
View on GitHub →We're recruiting. The VQC Lab is looking for motivated PhD students, RAs, and postdocs interested in Quantum Computing, Formal Verification, Programming Languages, or Operating Systems.
Email Prof. Tao