Formal modeling: check the design before you build it

A model is a small description of what a system is allowed to do, written in a language a solver can search. You state a property. The solver then searches every case inside a bound you set and either finds a case that breaks the property or reports that none exists. A test checks the cases you thought of. A model checker checks the cases you did not.

This skill is a router. Start with Alloy 6, which is the default tool here. Read the reference for the topic in front of you rather than reading everything.

Why this is worth doing

Formal modeling used to need a specialist. It does not any more, because you can write the model. The cost of learning a language like Alloy used to be the whole barrier. Running one more check is now cheap enough that checking a design can be a normal part of the work.

The evidence that it finds real bugs is not new.