Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs

Aarthi Sundaram; Robert Rand; Kartik Singhal; Youngchan Cho; Brad Lackey

doi:10.22331/q-2026-07-23-2172

Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs

Aarthi Sundaram¹, Robert Rand², Kartik Singhal², Youngchan Cho², and Brad Lackey¹

¹Microsoft Quantum, Redmond, WA
²University of Chicago, Chicago, IL

Published:	2026-07-23, volume 10, page 2172
Editor:	Miriam Backens
Eprint:	arXiv:2101.08939v6
Doi:	https://doi.org/10.22331/q-2026-07-23-2172
Citation:	Quantum 10, 2172 (2026).

Find this paper interesting or want to discuss? Scite or leave a comment on SciRate.

Abstract

We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a common subset of quantum programs. Our applications include (i) certifying whether auxiliary qubits can be safely disposed of, (ii) determining if a system is separable across a given bipartition, (iii) checking the transversality of a gate with respect to a given stabilizer code, and (iv) computing post-measurement states for computational basis measurements. Further, this logic is extended to accommodate universal quantum computing by deriving Hoare triples for the $T$-gate, multiply-controlled unitaries such as the Toffoli gate, and some gate injection circuits that use associated magic states. A number of interesting results emerge from this logic, including a lower bound on the number of $T$ gates necessary to perform a multiply-controlled $Z$ gate.

Featured image: The Hoare triples that make up the core rules of our stabilizer logic and capture Gottesman's semantics of the Heisenberg representation.

Popular summary

Quantum computers promise extraordinary computational power but ensuring that a quantum program behaves correctly is notoriously difficult. We introduce a lightweight logic that borrows ideas from software verification and quantum information science, allowing programmers to reason about a wide variety of quantum circuits without tracking their exponentially large state. The framework can certify properties such as disentanglement, safe qubit disposal, and fault-tolerant gate behavior, offering a practical route toward more reliable quantum software.

► BibTeX data

@article{Sundaram2026hoaremeets,
  doi = {10.22331/q-2026-07-23-2172},
  url = {https://doi.org/10.22331/q-2026-07-23-2172},
  title = {Hoare meets {H}eisenberg: {A} {L}ightweight {L}ogic for {Q}uantum {P}rograms},
  author = {Sundaram, Aarthi and Rand, Robert and Singhal, Kartik and Cho, Youngchan and Lackey, Brad},
  journal = {{Quantum}},
  issn = {2521-327X},
  publisher = {{Verein zur F{\"{o}}rderung des Open Access Publizierens in den Quantenwissenschaften}},
  volume = {10},
  pages = {2172},
  month = jul,
  year = {2026}
}

► References

[1] Scott Aaronsonand Daniel Gottesman ``Improved Simulation of Stabilizer Circuits'' Physical Review A 70, 052328 (2004).
https://doi.org/10.1103/physreva.70.052328

[2] Jonas T. Anderson, Guillaume Duclos-Cianci, and David Poulin, ``Fault-Tolerant Conversion between the Steane and Reed-Muller Quantum Codes'' Phys. Rev. Lett. 113, 080501 (2014).
https://doi.org/10.1103/PhysRevLett.113.080501
arXiv:1403.2734

[3] Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev, ``Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics'' Proc. PLDI '20 286–300 (2020).
https://doi.org/10.1145/3385412.3386007
https://files.sri.inf.ethz.ch/website/papers/pldi20-silq.pdf

[4] Giuseppe Castagna ``Programming with union, intersection, and negation types'' Springer (2023).
https://doi.org/10.1007/978-3-031-34518-0_12

[5] Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoît Valiron, ``An Automated Deductive Verification Framework for Circuit-Building Quantum Programs'' Programming Languages and Systems, ESOP 2021 12648, 148–177 (2021).
https://doi.org/10.1007/978-3-030-72019-3_6

[6] Christophe Chareton, Dongho Lee, Benoît Valiron, Renaud Vilmart, Sébastien Bardin, and Zhaowei Xu, ``Formal Methods for Quantum Algorithms'' CRC Press (2023).
https://doi.org/10.1201/9781003090052-7

[7] Richard Cleveand Daniel Gottesman ``Efficient Computations of Encodings for Quantum Error Correction'' Phys. Rev. A 56, 76–82 (1997).
https://doi.org/10.1103/PhysRevA.56.76

[8] Patrick Cousotand Radhia Cousot ``Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints'' Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977 238–252 (1977).
https://doi.org/10.1145/512950.512973
https://courses.cs.washington.edu/courses/cse503/10wi/readings/p238-cousot.pdf

[9] David Deutsch ``Quantum theory, the Church–Turing principle and the universal quantum computer'' Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences 400, 97–117 (1985).
https://doi.org/10.1098/rspa.1985.0070

[10] Yuan Fengand Mingsheng Ying ``Quantum Hoare Logic with Classical Variables'' ACM Transactions on Quantum Computing 2 (2021).
https://doi.org/10.1145/3456877

[11] Alain Frisch, Giuseppe Castagna, and Véronique Benzaken, ``Semantic Subtyping: Dealing Set-Theoretically with Function, Union, Intersection, and Negation Types'' J. ACM 55 (2008).
https://doi.org/10.1145/1391289.1391293

[12] David Gosset, Vadym Kliuchnikov, Michele Mosca, and Vincent Russo, ``An Algorithm for the T-Count'' Quantum Info. Comput. 14, 1261–1276 (2014).
https://doi.org/10.26421/QIC14.15-16-1
arXiv:1308.4134

[13] Daniel Gottesman ``Class of quantum error-correcting codes saturating the quantum Hamming bound'' Phys. Rev. A 54, 1862–1868 (1996).
https://doi.org/10.1103/physreva.54.1862

[14] Daniel Gottesman ``The Heisenberg Representation of Quantum Computers'' Group22: Proceedings of the XXII International Colloquium on Group Theoretical Methods in Physics 32–43 (1998).

[15] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron, ``Quipper: A Scalable Quantum Programming Language'' Proc. PLDI '13 333–342 (2013).
https://doi.org/10.1145/2491956.2462177
arXiv:1304.3390

[16] Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks, ``Proving Quantum Programs Correct'' 12th International Conference on Interactive Theorem Proving (ITP 2021) 193 (2021).
https://doi.org/10.4230/LIPIcs.ITP.2021.21

[17] Kentaro Honda ``Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism'' Proc. QPL '15 195, 262–272 (2015).
https://doi.org/10.4204/EPTCS.195.19

[18] Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, and Mingsheng Ying, ``Efficient Formal Verification of Quantum Error Correcting Programs'' Proceedings of the ACM on Programming Languages 9, 1068–1093 (2025).
https://doi.org/10.1145/3729293

[19] Yipeng Huangand Margaret Martonosi ``Statistical Assertions for Validating Patterns and Finding Bugs in Quantum Programs'' Proceedings of the 46th International Symposium on Computer Architecture 541–553 (2019).
https://doi.org/10.1145/3307650.3322213

[20] Marco Lewis, Sadegh Soudjani, and Paolo Zuliani, ``Formal Verification of Quantum Programs: Theory, Tools, and Challenges'' ACM Transactions on Quantum Computing 5 (2023).
https://doi.org/10.1145/3624483

[21] Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, and Yuan Xie, ``Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs'' Proc. ACM Program. Lang. 4 (2020).
https://doi.org/10.1145/3428218

[22] Ji Liu, Gregory T. Byrd, and Huiyang Zhou, ``Quantum Circuits for Dynamic Runtime Assertions in Quantum Computation'' Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems 1017–1030 (2020).
https://doi.org/10.1145/3373376.3378488

[23] Michael A. Nielsenand Isaac L. Chuang ``Quantum Computation and Quantum Information: 10th Anniversary Edition'' Cambridge University Press (2010).
https://doi.org/10.1017/CBO9780511976667

[24] Simon Perdrix ``Quantum Entanglement Analysis Based on Abstract Interpretation'' Static Analysis 270–282 (2008).
https://doi.org/10.1007/978-3-540-69166-2_18
arXiv:0801.4230

[25] Simon Perdrix ``Quantum Patterns and Types for Entanglement and Separability'' Electron. Notes Theor. Comput. Sci. 170, 125–138 (2007) Proc. QPL '05.
https://doi.org/10.1016/j.entcs.2006.12.015

[26] Frédéric Prostand Chaouki Zerrari ``Reasoning about entanglement and separability in quantum higher-order functions'' International Conference on Unconventional Computation 219–235 (2009).
https://doi.org/10.1007/978-3-642-03745-0_25

[27] Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic, ``ReQWIRE: Reasoning about Reversible Quantum Circuits'' Proc. QPL '18 299–312 (2018).
https://doi.org/10.4204/EPTCS.287.17

[28] Robert Rand, Aarthi Sundaram, Kartik Singhal, and Brad Lackey, ``Gottesman Types for Quantum Programs'' Proceedings of the 17th International Conference on Quantum Physics and Logic (QPL), Paris, France, June 2–6, 2020 340, 279–290 (2021).
https://doi.org/10.4204/EPTCS.340.14

[29] Peter Selingerand Benoît Valiron ``A lambda calculus for quantum computation with classical control'' Mathematical Structures in Computer Science 16, 527–552 (2006).
https://doi.org/10.1017/S0960129506005238

[30] Andrew Steane ``Multiple-particle interference and quantum error correction'' Proceedings of the Royal Society of London. Series A: Mathematical, Physical and Engineering Sciences 452, 2551–2577 (1996).
https://doi.org/10.1098/rspa.1996.0136

[31] Andrew M. Steane ``Active Stabilization, Quantum Computation, and Quantum State Synthesis'' Phys. Rev. Lett. 78, 2252–2255 (1997).
https://doi.org/10.1103/PhysRevLett.78.2252

[32] Aarthi Sundaram, Robert Rand, Kartik Singhal, and Brad Lackey, ``A Rich Type System for Quantum Programs'' (2021).
arXiv:2101.08939v3

[33] Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler, ``Q#: Enabling Scalable Quantum Computing and Development with a High-level DSL'' Proc. Real World Domain Specific Languages Workshop (RWDSL) 2018 7:1–7:10 (2018).
https://doi.org/10.1145/3183895.3183901
arXiv:1803.00652

[34] Dominique Unruh ``Quantum Hoare Logic with Ghost Variables'' Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science 1–13 (2019).
https://doi.org/10.1109/LICS.2019.8785779
arXiv:1902.00325

[35] Anbang Wu, Gushu Li, Hezi Zhang, Gian Giacomo Guerreschi, Yuan Xie, and Yufei Ding, ``QECV: Quantum Error Correction Verification'' (2021).
arXiv:2111.13728

[36] Mingsheng Ying ``A practical quantum Hoare logic with classical variables, I'' Information and Computation 309, 105417 (2026).
https://doi.org/10.1016/j.ic.2026.105417

[37] Mingsheng Ying ``Floyd–Hoare Logic for Quantum Programs'' ACM Trans. Program. Lang. Syst. 33 (2012).
https://doi.org/10.1145/2049706.2049708

[38] Nengkun Yuand Jens Palsberg ``Quantum abstract interpretation'' Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation 542–558 (2021).
https://doi.org/10.1145/3453483.3454061

[39] Charles Yuan, Christopher McNally, and Michael Carbin, ``Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs'' Proc. ACM Program. Lang. 6 (2022).
https://doi.org/10.1145/3498691
arXiv:2205.02287

[40] Li Zhou, Nengkun Yu, and Mingsheng Ying, ``An Applied Quantum Hoare Logic'' Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation 1149–1162 (2019).
https://doi.org/10.1145/3314221.3314584
https://opus.lib.uts.edu.au/bitstream/10453/140615/2/3314221.3314584.pdf

Cited by

[1] Xin Sun, Xingchi Su, Xiaoning Bian, and Huiwen Wu, "Weakest precondition calculus and relative completeness of satisfaction-based quantum Hoare logic", Quantum Information Processing 25 8, 273 (2026).

[2] Anbang Wu, Gushu Li, Hezi Zhang, Gian Giacomo Guerreschi, Yuan Xie, and Yufei Ding, "QECV: Quantum Error Correction Verification", arXiv:2111.13728, (2021).

[3] Charles Yuan, Christopher McNally, and Michael Carbin, "Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs", arXiv:2205.02287, (2022).

[4] Andrea Colledan and Ugo Dal Lago, "Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages", arXiv:2408.03121, (2024).

[5] Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, and Mingsheng Ying, "Efficient Formal Verification of Quantum Error Correcting Programs", arXiv:2504.07732, (2025).

[6] Mathys Rennela, "Quasilinear Equivalence Checking for Detector Error Models", arXiv:2606.14677, (2026).

[7] Wei-Lun Tsai, Yu-Fang Chen, and Ondřej Lengál, "A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)", arXiv:2605.05786, (2026).

[8] Robert I. Booth and Cole Comfort, "Denotational semantics for stabiliser quantum programs", arXiv:2511.22734, (2025).

[9] Stefanie Muroya and Thomas A. Henzinger, "Formal Verification of Continuous-Variable Quantum Programs", arXiv:2607.17714, (2026).

[10] Tianshi Yu, Gilles Barthe, Minbo Gao, Mingsheng Ying, and Li Zhou, "Reasoning about Continuous-Variable Quantum Systems", arXiv:2607.23137, (2026).

The above citations are from Crossref's cited-by service (last updated successfully 2026-08-12 20:56:45) and SAO/NASA ADS (last updated successfully 2026-08-12 20:56:46). The list may be incomplete as not all publishers provide suitable and complete citation data.

This Paper is published in Quantum under the Creative Commons Attribution 4.0 International (CC BY 4.0) license. Copyright remains with the original copyright holders such as the authors or their institutions.