We are building ATC (= ACL2 To C),
a proof-generating C code generator for the ACL2 theorem prover.
ATC translates ACL2 code of a specified form into C,
and it also generates an ACL2 proof of correctness of the generated C code with respect to the ACL2 code,
based on a formal model of C that we are also developing in ACL2.
ATC complements APT.
These two tools provide a way to synthesize verified C code from high-level specifications.
ATC is available here
and documented here.
Also see ATJ, a Java code generator for ACL2.
A Proof-Generating C Code Generator for ACL2 Based on a Shallow Embedding of C in ACL2
17th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2022)