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

> в том числе верифицировать-то по идее не помодульно нужно, а весь код в совокупности! В верификции модульность не проблема. Поскольку фактически создается полная модель кода, то теоремы для корректности взаимодействия модулей тоже генерируются. Т.е. если вызывается функция, то генерируется теорема для preconditions и для инвариантов. Таким образом, если все теоремы доказаны, то код в совокупности тоже отверифицирован (разумеется с учетом полноты спецификации и модели, ибо иногда полная верификация не нужна). Хуже того, атом верификации - это какое-то одно утверждение для одного пути исполнения кода в одном модуле :). Обычно для него генерируется отдельная теорема и надо ее доказать. В простеньком методе несколько путей и по нескольку утверждений для проверки. Т.е. суммарно на один несложный метод выходит 20-30 теоремок. Правда они обычно автоматически доказываются. Но доказать надо все теоремы, ибо они друг на друга полагаются, тут принцип все или ничего :).