Quave (QUantum Algorithm VErification) is a quantum program verification tool built using Lean. Implements quantum Hoare logic with classical variables to create formal, rigiourous proofs of the correctness of quantum programs.
- Clone the project to your local machine
git clone [email protected]:alexjgreig/Quave.git- Navigate to the project directory
cd Quave- Download the mathlib package
lake update