CAVA consists of the DFG projects Computer Aided Verification of Automata (completed) and Verified Model Checkers (ongoing). Its aim is the formalization and verification of important 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 intended 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.