From Hillel Wayne's writing

A notation to describe the design of a system without implementing it.Can test the design for bugs rather than the implementation.

Examples

z
The first specification language to reach widespread use. Relies on settheory to describe states and schemas to describe behavior, firstcatalogued as a way of managing 'data semantics'.

Alloy
A response to Z's complex syntax and tooling. Alloy is an attempt tosimplify both of these, specifying everything as either a type signatureor relationship between signatures. Alloy is popular for SAT problemsand models; it easily visualizes models to share properties withnontechnical people as well. This would be the tool to try! More here:alloy: the neat formalmethod.

• TLA^+ is a formalspecification langauge used to model concurrent and distributedsystems; it's best respected as testable pseudocode and is similar tothe drawing of blueprints for complex software systems. It is alsodesigned to check liveness properties of systems.Hillelhas a good article on modeling a complex system in the softwaredevelopment world with formal methods.
• Prism :: Used to model probabilistic specifications, in whichdifferent things have different chances of happening and events areall dependent. Its syntax is very restrictive in order to betractable, but the opportunity to model probabilistic systems isincredible.
• 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.

Terms

Temporal logic
Extending standard mathematical notation to allow temporal logic tochange over time. Temporal logic of actions is a subset of this conceptthat scales to real world systems.

Liveness properties
Similar to the definition in the compiler sphere, liveness propertiesare properties of systems that must eventually be true for the spec tobe valid.