Project results

Research articles

• To be completed

Software

• qrhl-tool – A theorem prover for quantum security proofs
• scala-isabelle – A Scala library for controlling the Isabelle theorem prover

Formal proof developments

• Quantum and Classical Registers – Isabelle/HOL formalization of the theory of quantum registers.
• Complex Bounded Operators – Isabelle/HOL formalization of parts of complex operator theory.
• Banach-Steinhaus Theorem – Isabelle/HOL formalization of the Banach-Steinhaus theorem.
• Verification of Fujisaki-Okamoto – Post-quantum security verification of a Fujisaki-Okamoto variant