a formal specification language, like a blueprint for logical implementation
a tool to design systems and algorithms, the programmatically verify that those systems don't have critical bugs
created by Leslie Lamport (person behind Paxos Algo, Time Clocks Paper)
more source