[doublec]

Yes, it's possible to integrate ATS generated code into a C project. ATS provides control over the names of the generated functions so you can only convert the parts you want to be verified as safe by ATS if needed.