A notation to describe the design of a system without implementing it. Can test the design for bugs rather than the implementation.
TLA^+ is a formal specification langauge used to model concurrent and distributed systems; it's best respected as testable pseudocode and is similar to the drawing of blueprints for complex software systems. It is also designed to check liveness properties of systems.
Hillel has a good article on modeling a complex system in the software development world with formal methods.
Prism :: Used to model probabilistic specifications, in which different things have different chances of happening and events are all dependent. Its syntax is very restrictive in order to be tractable, but the opportunity to model probabilistic systems is incredible.
Spin :: As expressive as TLA+, but written to model network protocols.
There are a lot more, but I'll investigate them further as I learn more.
Joey Eremondi on Twitter: "Has anyone seen a "reference" implementation of an SMT solver? Not one that is fast like Z3 or CVC4, but one that implements the algorithm in a fairly straightforward way that's slow but grokkable. I'm particularly interested in how it handles uninterpreted functions (UF)." / Twitter alloy: the neat formal method http://www.ccs.neu.edu/home/pete/courses/Computer-Aided-Reasoning/2018-Fall/