CACoq Fomalization of Constraint Automata in the Coq proof assistant. Coq version >= 8.9 Please notice it does not work on Coq versions lower than 8.8 due to some tactics' implementation we rely on.