Came here to suggest Idris, as it compiles to C. F* is still experimental and Idris is just coming up on a RC. They could also drop down into C and manually verify it.