There's lots of options. You can write an implementation in Coq (it has its own functional language you code in), prove it correct in Coq and then "extract" (li

There's lots of options. You can write an implementation in Coq (it has its own functional language you code in), prove it correct in Coq and then "extract" (like transpiling) it to another language like OCaml for executing. There's ways to map C code into Coq to prove it's correct as well. All of this is machine checked. See the sel4 kernel to get more of a feel for it. Property based testing sits somewhere between regular software testing with unit tests and theorem proving on the spectrum. It's much less time intensive to do but much less rigorous. My point isn't that formal verification is better than everything. It has its trade-offs, just like TDD.