CACoq Fomalization of Constraint Automata in the Coq proof assistant. Current 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.