QHL-Lean

Quantum Hoare Logic in Lean 4 is a quantum program verification tool. Implements quantum Hoare logic with classical variables to create formal, rigiourous proofs of the correctness of quantum programs.