Proof assistant for qRHL
25
stars
1,306
commits
Scala
primary language
May 24, 2026
updated
README
Qrhl-tool is an interactive theorem prover for qRHL (quantum relational Hoare logic), specifically for quantum and post-quantum security proofs.
- Installation – how to install
- Web page – for more information
Acknowledgments
Development was supported by the Air Force Office of Scientific Research (AOARD Grant FA2386-17-1-4022), by the ERC consolidator grant CerQuS (819317), and by the PRG946 grant from the Estonian Research Council.
Contributors
Similar repos
Languages
Scala
41.0%
Isabelle
36.6%
Standard ML
21.5%
Proof assistant for qRHL
25
stars
1,306
commits
Scala
primary language
May 24, 2026
updated
README
Qrhl-tool is an interactive theorem prover for qRHL (quantum relational Hoare logic), specifically for quantum and post-quantum security proofs.
- Installation – how to install
- Web page – for more information
Acknowledgments
Development was supported by the Air Force Office of Scientific Research (AOARD Grant FA2386-17-1-4022), by the ERC consolidator grant CerQuS (819317), and by the PRG946 grant from the Estonian Research Council.
Similar repos
Contributors
Languages
Scala
41.0%
Isabelle
36.6%
Standard ML
21.5%