Another project in this space is the proof assistant [Quantomatic](https://quantomatic.github.io/), written by Aleks Kissinger and other folks associated with the Universities of Oxford and Edinburgh.