I don’t write software, but in asic and fpga design, formal method specifications enable the use of things like SAT solvers to determine if the underlying test article meets the specification.

You specify properties of the design and the tooling tests the design in a variety of ways to see if it can violate those properties.

Let’s say you have a system that controls turn signals. You can specify properties that say things like lanes that cross each other can’t both have a green light at the same time or even within some period of time of each other.

The tooling can exhaustively check the design for this and surface code traces that violate it.