CAVA is a DFG-funded project that formalises and verifies important algorithmic parts of automata theory and model checking using the proof assistant Isabelle/HOL. While the algorithms are formalised on a mathematical, abstract level, they are still intended to be executable. The code that is automatically generated by Isabelle is indented to be used as a reference implementation. For a detailed description of the goals of the CAVA project, please have a look at the Project Description page.