一句话：结合 Alloy 形式化的 QASM 3.0 模型与约束引导模糊测试，对量子模拟器做差分基准测试，发现 8 个缺陷（6 个未记录）。
量子计算平台依赖模拟器在硬件执行前建模电路行为，模拟器不一致会导致高代价错误。现有形式化验证多针对特定编译器组件以控制状态爆炸，常漏掉关键缺陷；而常规测试缺乏对边界情形与真实执行场景的系统探索，易产生误报与漏报。本文提出 FuzzQ：以 Alloy 形式化的 QASM 3.0 语义模型为核心，自动生成结构多样且满足约束与保证性质的量子电路，并结合差分基准测试、变异测试与不变式检查。框架引入多种测试预言，包括不变式检查、统计分布检验，以及新颖的跨模拟器酉一致性检查——在模全局相位意义下验证功能等价，可发现标准态矢量比较无法察觉的差异。作者在 Qiskit 与 Cirq 上评估，执行逾 80 万个电路，考察吞吐、代码与电路覆盖率以及灵敏度、正确性与内存开销，共发现 8 个模拟器缺陷，其中 6 个此前未记录，并给出扩展到含噪混合态模拟的路线。
Quantum computing platforms rely on simulators for modelling circuit behaviour prior to hardware execution, where inconsistencies can lead to costly errors. While existing formal validation methods typically target specific compiler components to manage state explosion, they often miss critical bugs. Meanwhile, conventional testing lacks systematic exploration of corner cases and realistic execution scenarios, resulting in both false positives and negatives. We present FuzzQ, a novel framework that bridges this gap by combining formal methods with structured test generation and fuzzing for quantum simulators. Our approach employs differential benchmarking complemented by mutation testing and invariant checking. At its core, FuzzQ utilises our Alloy-based formal model of QASM 3.0, which encodes the semantics of quantum circuits to enable automated analysis and to generate structurally diverse, constraint-guided quantum circuits with guaranteed properties. We introduce several test oracles to assess both Alloy’s modelling of QASM 3.0 and simulator correctness, including invariant-based checks, statistical distribution tests, and a novel cross-simulator unitary consistency check that verifies functional equivalence modulo global phase, revealing discrepancies that standard statevector comparisons fail to detect in cross-platform differential testing. We evaluate FuzzQ on both Qiskit and Cirq, demonstrating its platform-agnostic effectiveness. By executing over 800,000 quantum circuits to completion, we assess throughput, code and circuit coverage, and simulator performance metrics, including sensitivity, correctness, and memory overhead. Our analysis revealed eight simulator bugs, six previously undocumented. We also outline a path for extending the framework to support mixed-state simulations under realistic noise models.
@article{paperbot2911,
title = {Shaking Up Quantum Simulators with Fuzzing and Rigour},
author = {Vasileios Klimis and Avner Bensoussan and Elena Chachkarova and Karine Even-Mendoza and Sophie Fortz and Connor Lenihan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763100}
}