This repositry contains the HOL formalization for the verification of optical quantum cicuits For using this formalization, see https://github.com/beillahi/FMV-QC-HOL/blob/master/README-quantumcad