Quantum verification via tangles, quandles, and automated reasoning

19^th March 2026, 11:00 Ashton 208
Alexei Lisitsa
UoL

Abstract

In this talk, I will present our recent work on automating the verification of
quantum programs and circuits, building on a method proposed by Reutter and
Vicary (2019). In this framework, quantum circuits and programs are modelled as
tangles—informally, finite collections of strings or laces embedded and
entangled in three-dimensional space. Verification of program equivalence is
then reduced to the problem of tangle equivalence (isotopy), yielding a
conceptually simple and visually appealing approach.
Drawing on our earlier work on applying automated reasoning to computational
topology, particularly knot theory, we translate the resulting topological
problems into an algebraic setting. This is achieved using variants of
algebraic structures known as quandles. Automated reasoning tools (theorem
provers and model finders) are then employed to establish (non-)equivalence of
tangles, and hence of the corresponding quantum circuits.
I will conclude by highlighting several open questions and challenges, both in
the theoretical foundations of the approach and in its practical application to
quantum program verification.

Joint work with Andrew Fish.

Additional Materials

• https://easychair.org/publications/paper/S8Gt