Без заголовка

В инженерии такая верификация называется assurance case. Но я согласен: методы формальной верификации главным образом получили распространение именно в дизайне железа, эти методы вошли в состав кремниевых компиляторов как неотъемлимая часть. Как я понимаю, сейчас порождающие системы в CAD просто "генерируют по правилам", а сгенерированный ими код соответствует правилам "в силу того, что он сгенерирован по этим правилам" ;)