The use of formal methods in safety critical code is already well-established. MBD is a very common method to write ECU software, for example. It's not universal though and proofs of the more complicated system requirements are challenging at best.