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.