Abstract
Quantum computers are known to handle hard computational problems and provide unbreakable security protocols. Among different quantum computer implementations, those based on quantum optics and nuclear magnetic resonance show good advancement in building large scale machines. However, the involvement of optical and nuclear techniques makes their development very critical. This motivates us to apply formal techniques, in particular theorem proving, in quantum circuits analysis. In this work, we present the formalization of multi-inputs/multi-outputs quantum gates (technically called multi-modes optical circuits). This requires the implementation of the Hilbert space of Lebesuge square integrable complex-valued functions, namely $L^2$ space. We then build formal model of single optical beams and extend it to cover circuits of multi optical beams, with the help of tensor product algebra. As an application, we formally verify the behavior of the optical quantum CNOT gate and Mach-Zehnder interferometer.