Architects draw detailed plans before construction begins. Software engineers don't. Can this be why buildings seldom collapse and programs often crash? A blueprint for software is called a specification. TLA+ specifications have been described as exhaustively testable pseudo-code. High-level TLA+ specifications can catch design errors that are now found only by examining the rubble after a system has collapsed.