Eilenberg machines have been introduced in 1974 in the field of formal language theory. They are finite automata for which the alphabet is interpreted by mathematical relations over an abstract set. They generalize many finite state machines. We consider in the present work a class of Eilenberg machines for which we provide an executable complete simulator. This program is described using the Coq specification language. The correction of the algorithm is also proved formally and mechanically verified using the Coq proof assistant. The Coq extraction code technology allows to translate the specification into executable OCaml code. The algorithm and proofs are inspired from the reactive engine of Gérard Huet.