I just want to note, there exist two main flavors of formal methods: extrinsic techniques, which are disjoint from the code itself and generally reason about the specifications of code, and intrinsic techniques, which are inline with the code itself and reason about the code more directly. Historically, intrinsic techniques (such as type systems) reason about code at a functional level, while extrinsic techniques (such as decidable model checkers like Spin/P) reason about a model of the code, ascribed to formalism like an automata. But imo we're currently in a complete golden age of formal methods research, and extrinsic techniques are falling out of flavor in comparison to intrinsic methods as pushed by type system advancements and projects like Verus [1].
[1] https://github.com/verus-lang/verus