  Quantum computations are expressed in general as quantum circuits, which are
specified by ordered lists of quantum gates. The resulting specifications are
used during the optimisation and execution of the expressed computations.
However, the specification format makes it difficult to verify that optimised
or executed computations still conform to the initial gate list specifications:
showing the computational equivalence between two quantum circuits expressed by
different lists of quantum gates is exponentially complex in the worst case. In
order to solve this issue, this work presents a derivation of the specification
format tailored specifically for fault-tolerant quantum circuits. The circuits
are considered a form consisting entirely of single qubit initialisations, CNOT
gates and single qubit measurements (ICM form). This format allows, under
certain assumptions, to efficiently verify optimised (or implemented)
computations. Two verification methods based on checking stabiliser circuit
structures are presented.
