Decision Tables[1] is probably the simplest formal method, i.e. instead of writing imperative nested if and switch/case statements, your provide a declarative solution.
But IMO the most useful formal method in Software Engineering is modeling your code as an FSMs, for example using StateCharts UML notation [2,3].
That way even junior developers can reason about complex realtime systems.
Next close come Algebraic Type Systems, but they're usually not available in mainstream PLs.
Unfortunately Formal Specification/Verification tools like TLA+, Alloy, etc. are less practical for most real life projects.
State machines are handy, and along with modelling they can be implemented directly. A simple implementation is you define the possible states for your application, or module or whatever, and the valid transitions from state to state. You assign the new state when the state should transition, and this assignment is wrapped by some simple check that the transition is valid. If not, throw an error, or handle it, etc. The state path can also be logged to aid with debugging. I've found it invaluable in building web apps, finding odd things not caught in traditional testing e.g. like cases of trying to transition from the current state to the same state.
But IMO the most useful formal method in Software Engineering is modeling your code as an FSMs, for example using StateCharts UML notation [2,3].
That way even junior developers can reason about complex realtime systems.
Next close come Algebraic Type Systems, but they're usually not available in mainstream PLs.
Unfortunately Formal Specification/Verification tools like TLA+, Alloy, etc. are less practical for most real life projects.
--
[1] https://en.wikipedia.org/wiki/Decision_table
[2] https://en.wikipedia.org/wiki/UML_state_machine
[3] https://en.wikipedia.org/wiki/State_diagram#Harel_statechart