avlasov предложил proof-based software and systems engineering -- http://avlasov.livejournal.com/26832.html. Как я его понял, он предлагает не столько доказательство того, что модель описывает систему, которая достигнет определенного результата, сколько доказательство правильности самой модели (что модель, например, не начнет в какой-то момент делить на ноль где-то внутри себя, или не зациклится в самый неожиданный момент).
Очень приятно, что появляются люди, обсуждающие такие проблемы. Понятно, что это все не сегодняшний день, но это явно будет реализовано в том или ином виде -- весь вопрос только в том, завтра это будет или послезавтра (хотя в силу приближающейся сингулярности завтра и послезавтра вполне могут оказаться уже неразличимыми).