A model-checking tool for quantum programs verified selected examples with up to 100 qubits within seconds, according to a new arXiv preprint. The results show that its performance can change dramatically with the shape of a circuit and the precision of the numbers used in it.
The software, called QisMC, was evaluated on benchmark programs and case studies. The authors asked whether it could express and debug properties beyond existing quantum model checkers, and how it would scale against those tools.
A formal check for quantum code
QisMC's qCTL algorithm repeatedly updates two fixed-point calculations in both directions, checks whether quantum propositions are satisfiable, and reduces qCTL checking to classical CTL checking.
The implementation combines Python and C++ layers. CFLOBDD serves as the C++ symbolic backend, while NuSMV is invoked from Python as the external model-checking engine.
For the common benchmark workflow, the programs were supplied as OpenQASM 2 files and loaded through standard Qiskit. The checks began from an all-zero state; the researchers then injected a randomly generated Pauli error and tested the altered program against a property derived from the correct output.
From a failed check to a suspected fault
In one deliberately faulty program, QisMC returned a failed model-checking result and produced a 46-location counterexample trace running from the initial location to the terminal. The trace supplied source-level diagnostic information for the tested fault.
A separate VQSS case study produced unsatisfiable formulas during verification, indicating that the secret state had been altered during protocol execution.
The comparison favored QisMC on selected sizes
The comparison with QPMC and QTC-Maude used simple termination properties because equivalent full debugging specifications were difficult to reproduce across the tools. On the reported cases, QTC-Maude took 229 seconds and more than 4.7 million rewrites for a 17-qubit Grover benchmark. For an 11-qubit Bernstein–Vazirani benchmark, it took 1,515 seconds and more than 7.93 million rewrites. QPMC verified instances of no more than four qubits; larger cases ended in runtime exceptions.
The random-error tests did not produce a verification failure for every altered program. After injection, 7 of 49 Grover cases and 28 of 99 Bernstein–Vazirani cases were verified as True. Stim confirmed that all 28 True Bernstein–Vazirani instances preserved the correct program output.
Across distributed phase-estimation and quantum Fourier transform programs, along with conventional unitary counterparts, verification time rose exponentially as program size increased. Clean distributed and non-distributed versions performed comparably, but the distributed versions became noticeably slower after random Pauli errors were injected.
The Benchpress-medium suite contained 40 circuits ranging from 10 to 30 qubits. Eleven instances timed out in the evaluated benchmark set. The bwt cases contained more than 100,000 gates, and timeouts were also reported for dnn, ising, swap_test, knn, wstate and a quantum Fourier transform case.
Where the method still breaks down
Circuit layout mattered as much as the nominal qubit count in one paired comparison. Tree-structured instances with at least 63 qubits exceeded the 3,200-second timeout, while corresponding linear variants remained efficient. The intermediate decision diagrams grew exponentially only for the tree versions.
The largest reported Grover examples also exposed a numerical weakness. Two programs containing more than 250 qubits failed to establish the expected subspace property, with the paper identifying accumulated floating-point error as the issue. The current implementation cannot eliminate that accumulation entirely.
The tool's current specification language does not support probabilistic properties, so it cannot presently express that a quantum program should meet a condition with a particular probability. The paper lists probabilistic reasoning as future work.
The larger QisMC results are limited to the reported benchmark families, and the baseline comparison did not use equivalent full debugging specifications. The evaluation therefore does not establish that QisMC is faster on every quantum program.
The document is an arXiv preprint dated 25 August 2026.
Paper data and sources
Original title: QisMC: A Model Checker for QISKIT Program Debugging
Authors: Aochu Dai, Mingsheng Ying
Journal/Repository: arXiv
Status: Preprint, not yet peer-reviewed
First online: 2026-08-25
DOI: Not available
Original paper · Full text