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

На счет лапши полностью с Вами согласен, но реалии таковы, что ее пишут другие, а мне часто приходилось ее сопровождать :), с целью ускорения перфоманса, например. Там широкий простор для lightweight верификации. По поводу Вашей идеи что приходит в голову: использовать частично описанные узлы дерева, т.е. такие процедуры, которые не описаны полностью (но для которые известны пред- пост- условия и инварианты). Если бы это было возможно, применимость, как мне кажется, возросла бы. Да так можно делать. Кстати, это даже реализовано в KeY тулзе, ссылку на которую я Вам дал. В плане интерфейса, на мой взгляд это лучшее, что есть, в том числе там и эта фича есть :). Но впрочем, не слушайте меня, я подробно в этом никогда не разбирался. Вы на самом деле весьма неплохо разбираетесь. Я не лучше, просто я может чуть больше времени потратил на изучение деталей, но это решаемо :)