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

Только вот боюсь, аналитически доказать "правильность" этого предиката (я так понимаю, что таковым доказательством Вы видите его разложение по ряду предикатов - функциональных требований) вероятнее всего не получится. Задача верификации состоит не в доказательстве "правильности" предиката. Предикат как раз задает требования, которым должна удовлетворять реализация - последнее и нужно доказать. Конечно "правильность" предиката тоже нужно проверять, куда без этого. В частности, это можно делать методом доказательства - например доказывая, что у системы удовлетворяющей предикату, есть те или иные свойства. Хотя, в идеале, эти свойства лучше сразу задать как требования, т.е. включить в предикат. Но вообще, типа принимается, что требования изначально правильны :). Ну и предикат тоже :). Потому как, а с чем их еще сравнивать? Где взять эталон? А если есть где взять, тот как проверить правильность эталона? На практике, конечно, есть несколько разных документов, как формальных так и неформальных, ну и нужно их синхронизировать. Часть этого процесса можно формализовать и даже строго верифицировать. Но всегда будет и неформальная часть. Фактически, доказательство есть сведение к каким-то предположениям, аксиомам, которые принимаются изначально верными (в контексте доказательства). Если в процессе выясняется, что с аксиомами что-то не так - а это обычно выясняется - то это весьма и весьма ценная информация. Ибо неявные допущения присутствуют всегда. Задача формализации - вытащить их на свет божий.