f* (one system on display in this paper) can extract to c/assembler suitable for inclusion in a hand-written c source tree, all the while giving a wider and more interesting set of guarantees with the added benefit that you won't have to depend on a rust toolchain to build your project (bootstrapping f* is considerably easier, and you only have to do it when you check in your verified bits)

funny enough, much like rust, one of its most widely-deployed applications lives in firefox; see project-everest.github.io