I'm interested in examples you may have, as someone who once flirted with formal methods. The most practical use of formal method I witnessed is model checking

I'm interested in examples you may have, as someone who once flirted with formal methods. The most practical use of formal method I witnessed is model checking (with TLA+), but that does not check the actual implementation. There's also CompCert, a formally verified C compiler written in Coq, but even then, some parts are not verified so the final product may still have bugs.