The Second Workshop on Verification of Quantum Computing (VQC 2027), co-located with CAV 2027 in Amsterdam, brings together researchers from formal methods and quantum information to address the unique challenges of verifying quantum software and hardware.
Since the first edition of VQC in 2025, the field has moved quickly. Hardware vendors have demonstrated surface-code memories operating below the error-correction threshold and the first small fault-tolerant computations on superconducting, trapped-ion, and neutral-atom platforms, and early fault-tolerant machines now appear on vendor roadmaps for the end of the decade. Resource estimates for cryptographically relevant algorithms have dropped by an order of magnitude, turning the migration to post-quantum cryptography into a near-term engineering concern. Quantum software stacks have grown correspondingly: compilers now target fault-tolerant architectures through lattice surgery and magic-state distillation, runtimes orchestrate error correction and classical co-processing in real time, and distributed and hybrid quantum–classical programs are becoming the norm. Each of these layers is a place where a subtle bug can silently invalidate an experiment, a security argument, or a resource estimate.
At the same time, verification technology has matured. Interactive theorem provers now host substantial quantum libraries; automated tools based on automata, decision diagrams, SMT, abstract interpretation, and ZX-calculus scale to circuits of practical size; verified compilers and machine-checked resource bounds have moved from case studies to full algorithms; and AI-assisted proof engineering is lowering the cost of mechanization. VQC 2027 aims to connect these developments with the needs of the quantum computing community.
The workshop provides a dedicated forum for researchers and practitioners to:
- Exchange ideas on the latest research in quantum verification
- Discuss challenges and potential solutions for verifying quantum systems, from programs to fault-tolerant hardware
- Bridge the gap between the quantum computing and formal verification communities
- Advance the development of tools and frameworks for verifying, analyzing, and simulating quantum programs
Workshop Topics
Topics of interest include, but are not limited to:
- Formal verification of quantum programs: program logics, refinement, and mechanized proofs
- Verified quantum compilers, optimizers, and compiler passes
- Verification and validation of quantum error correction: codes, decoders, and fault-tolerant protocols
- Machine-checked resource estimation for quantum algorithms, including cryptanalytic applications
- Automated reasoning for quantum systems: equivalence checking, model checking, automata- and diagram-based methods, SMT and synthesis
- Verification of distributed, networked, and hybrid quantum–classical programs
- Validation, benchmarking, and testing of quantum computing systems and simulators
- High-level quantum programming languages, type systems, and novel programming abstractions
- Quantum circuit and program optimization with correctness guarantees
- Hardware-aware compilation, mapping, and routing, including fault-tolerant architectures
- Error handling and mitigation in near-term devices
- Certification, robustness, and security of quantum machine learning and quantum cryptographic protocols
- AI-assisted proof engineering and program synthesis for quantum software
Submissions
We invite prospective speakers to submit talk proposals. A proposal consists of a two-page summary (excluding bibliography and appendices), optionally accompanied by a link to a published paper or preprint. We welcome presentations of recently published work, work in progress, tool and system demonstrations, and position statements. The workshop has no formal proceedings; submissions are non-archival and do not preclude publication elsewhere.
All submissions are handled via EasyChair. Proposals are reviewed by the program committee for relevance and quality, and selected for either a talk or a poster. At least one author of each accepted proposal is expected to attend the workshop in person and register through CAV 2027.
Important Dates
Organizers
- Alfons Laarman Leiden University
- Yu-Fang Chen Academia Sinica
- Runzhou Tao University of Maryland