Leslie Lamport inventor of Paxos and developer of LaTeX introduces techniques and tools that help programmers think above the code level to determine what applications and services should do and ensure that they do it. Depending on the task, the appropriate tools can range from simple prose to formal, tool-checked models written in TLA+ or PlusCal