Comment by tehologist

Why not just use a verifiable subset of C? https://compcert.org/compcert-C.html