Uma abordagem para analisar especificações e projetos de sistemas usando modelos e propriedades que podem ser verificados logicamente.
Hillel Wayne apresenta princípios de métodos formais para detectar falhas de design antes da implementação do sistema, com foco na força das propriedades, na exploração do espaço de estados e nas suposições sobre o ambiente. Os exemplos mostram como uma análise simplificada de concorrência, falhas e novas tentativas pode revelar cedo erros dispendiosos.