VRAC is a set of Coq verified C code generators from C code annotated with ACSL (ANSI/ISO C Specification Language) annotations.