2026
-
Launch
Launching ecdsa.fail/lean with Yukon
How big a quantum computer does it take to break Bitcoin? Together with Yukon, we launched ecdsa.fail/lean, a leaderboard for quantum attacks on secp256k1, the elliptic curve behind Bitcoin and Ethereum signatures. Every result on it needs a Lean proof that it works for every possible input, so each number is machine-checked rather than estimated. See also our ShorECDLP project.
-
Teaching
Teaching two quantum systems courses this spring
Prof. Tao is teaching CMSC 437: Quantum Software Lab (co-taught with Prof. Xiaodi Wu) and CMSC 858Y: Quantum Computing Systems in Spring 2026.
2025
-
PaperOSDI 2025
“Quantum Virtual Machines” accepted to OSDI 2025
Our paper, with Hongzheng Zhu, Jason Nieh, Jianan Yao, and Ronghui Gu, was accepted to the 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2025).
-
Projects
New verified quantum algorithms & systems projects
The lab is actively developing several open-source formal verification projects, including ForShor (verified Shor's algorithm in Lean 4), ShorECDLP (verified resource estimates for Shor's algorithm against ECDSA), and Lean-QEC (end-to-end formalization of quantum error correction). See the Projects page for details.
-
Teaching
Spring 2025: Introduction to Quantum Computing
Prof. Tao taught CMSC/PHYS 457: Introduction to Quantum Computing.
2024
-
Milestone
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 became a Fellow at the Joint Center for Quantum Information and Computer Science (QuICS).
-
PaperPOPL 2024
“A Case for Synthesis of Recursive Quantum Unitary Programs” accepted to POPL 2024
With Haowei Deng, Yuxiang Peng, and Xiaodi Wu — accepted to the 51st ACM SIGPLAN Symposium on Principles of Programming Languages.
-
Milestone
Runzhou Tao completes Ph.D. at Columbia University
Advised by Ronghui Gu, completing a dissertation on formal verification for quantum and distributed systems.
2022
-
PaperPLDI 2022
“Giallar: Push-button Verification for the Qiskit Quantum Compiler” accepted to PLDI 2022
With Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, and Ronghui Gu — accepted to the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation.
2021
-
PaperSOSP 2021
“Formal Verification of a Multiprocessor Hypervisor on Arm Relaxed Memory Hardware” accepted to SOSP 2021
With Jianan Yao, Xupeng Li, Shih-Wei Li, Jason Nieh, and Ronghui Gu — accepted to the 28th ACM Symposium on Operating Systems Principles.
-
AwardOSDI 2021
DistAI wins the Jay Lepreau Best Paper Award at OSDI 2021
“DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols,” with Jianan Yao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan, received the Jay Lepreau Best Paper Award at the 15th USENIX Symposium on Operating Systems Design and Implementation.
-
PaperPLDI 2021
“Gleipnir: Toward Practical Error Analysis for Quantum Programs” accepted to PLDI 2021
With Yunong Shi, Jianan Yao, John Hui, Frederic T. Chong, and Ronghui Gu — accepted to the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation.
2020
-
AwardFOCS 2020
“Edge-Weighted Online Bipartite Matching” wins Best Paper Award at FOCS 2020
With Matthew Fahrbach, Zhiyi Huang, and Morteza Zadimoghaddam — received the Best Paper Award at the 61st IEEE Annual Symposium on Foundations of Computer Science.