A description of a system in a well-defined formal language such as PiSPEC or HLL. Read more about Formal specification here.