This repository formalises and verifies the CVM algorithm in the Isabelle proof assistant, as presented in the ITP 2025 paper "Verification of the CVM algorithm with a Functional Probabilistic Invariant".
- isabelle contains the Isabelle sources for our formalisations.
-
paper contains
$\LaTeX$ sources for our paper. -
presentation contains
$\LaTeX$ sources for the presentation at the ITP conference. - tools contains miscellaneous tools.
- archive contains obsolete experiments and formalisations.