Sistem özelliklerini ve tasarımlarını, mantıksal olarak doğrulanabilir modeller ve özellikler kullanarak analiz etme yaklaşımı.
Hillel Wayne, sistemi uygulamaya geçirmeden önce tasarım kusurlarını tespit etmek için biçimsel yöntemlerden yararlanma ilkelerini ele alıyor; özelliklerin gücüne, durum uzayının keşfine ve ortam varsayımlarına odaklanıyor. Örnekler, eşzamanlılık, arıza ve yeniden deneme süreçlerinin basitleştirilmiş analizinin maliyetli hataları erken ortaya çıkarabileceğini gösteriyor.