For a more practical approach (though limited to C) you can try the Frama-C suite. It works by annotating C code, instead of having to manually rewrite the code

For a more practical approach (though limited to C) you can try the Frama-C suite. It works by annotating C code, instead of having to manually rewrite the code in Coq. One thing that the post does not mention is that things get nasty real quick if you use actual machine integers (or number generally) instead of ideal ones in Coq- though that can also be due to my own ignorance as an amateur.