In this paper we give a partially mechanized proof of the correctness of Steane's 7-qubit error correcting code, using the tool Quantomatic. To the best of our knowledge, this represents the largest and most complicated verification task yet carried out using Quantomatic.
Cite
@article{arxiv.1306.4532,
title = {Verifying the Steane code with Quantomatic},
author = {Ross Duncan and Maxime Lucas},
journal= {arXiv preprint arXiv:1306.4532},
year = {2014}
}