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.
Hopefully soon, “moving in that direction” can be done by slowly porting to Checked C, while always retaining an executable artifact. https://github.com/Microsoft/checkedc
https://dl.acm.org/doi/abs/10.1145/3527322