At Correct Computation (https://correctcomputation.com/, we are hiring), we are developing a tool called 3C to provide automation assistance for the conversion of C code into Checked C. A completely automated approach is impractical (i.e., without making lots of changes to the target program's code and adding lots of overhead), but we have found a "best effort" approach works well.

See here for more info (which transitively links to a tutorial of 3C's use): https://github.com/correctcomputation/checkedc-clang/blob/ma...