验证方法与工具

量子程序 verification 需要先说明模型、性质和正确性等级。常见性质包括态变换等价、测量概率、纠缠关系、资源使用和 termination。对短线路，可以把 gate 乘成矩阵或 superoperator 并进行符号化比较；对带分支的程序，则要保留 classical outcome 或按规定对测量分支求和。可参考量子线路与量子霍尔逻辑建立规格。

方法层次

Static type checking（例如线性资源检查）适合发现 qubit 重复使用等结构错误，但不证明算法性质。Symbolic simulation 和 equivalence checking 可在有限规模下比较态、unitary 或 channel。Theorem prover 可以把量子谓词、矩阵恒等式和推理规则交给人工辅助证明；model checking 通常需要有限状态抽象。Randomized testing、statevector simulation 和 hardware runs 能发现反例或估计统计量，却不能单独给出对所有输入的证明。

一个谨慎的工作流

先写清楚输入空间、允许的噪声模型和 postcondition；再选择最弱前置条件或 Hoare-style 规则生成义务。对小规模例子，可独立计算

并与模拟器输出比较。若使用工具，要核对其文档是否真的支持 dynamic measurement、mixed state、noise 或 formal proof；“能运行”与“已经证明”是不同结论。不同工具版本、抽象层和浮点精度也会改变可复现性。

范围与参考

本文是个人学术用途的介绍性 demo，不伪造工具能力、审稿状态、更新日期或已完成的证明。下面的综述和定理证明论文用于了解研究方向，不能替代具体工具的当前文档。

参考文献：

• Lewis、Soudjani 与 Zuliani，Formal Verification of Quantum Programs: Theory, Tools and Challenges，arXiv:2110.01320。
• Liu 等，A Theorem Prover for Quantum Hoare Logic and Its Applications，arXiv:1601.03835。