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

Удается. Даже я на досуге верифицирую, правда, по мелочи. Но как нибудь соберусь с силами и отверифицирую реальный код. Первую версию одного метода я уже верифицировал, но она слишком простая. Вот вторая версия будет посложнее, но ее можно назвать реальным кодом. Правда, верификация императивного кода - очень геморройное занятие в силу того что нужно записывать ограничения на состояния массивов и объектов в куче. По-моему проще все на функциональных языках переписать. Кстати, появился функциональный язык ATS, у которого система типов достаточно мощная, чтобы задавать на ней спецификации программ. Благодаря этому он по скорости сравним с С, ибо там можно писать фактически в императивном стиле, параллельно доказывая корректность, и компилятор это учитывает. http://www.ats-lang.org/