Enfoque para analizar las especificaciones y los diseños de sistemas mediante modelos y propiedades que pueden verificarse lógicamente.
Hillel Wayne presenta principios de los métodos formales para detectar fallos de diseño antes de implementar el sistema, con énfasis en la fuerza de las propiedades, la exploración del espacio de estados y las suposiciones sobre el entorno. Los ejemplos muestran cómo un análisis simplificado de la concurrencia, los fallos y los reintentos puede revelar errores costosos en una etapa temprana.