Использование средств доказательства теорем для обнаружения атак

Я немного слышал об использовании автоматических средств доказательства теорем в попытках показать, что уязвимости безопасности не существуют в программной системе. В общем, это чертовски сложно сделать.

Мой вопрос: проводил ли кто-нибудь работу по использованию аналогичных инструментов, чтобы найти уязвимости в существующих или предлагаемых системах?

Эйдт: Я НЕ спрашиваю о доказательстве того, что программное обеспечение система безопасна. Я спрашиваю о поиске (в идеале ранее неизвестных) уязвимостей (или даже их классов). Я думаю, что (но не) здесь черная шляпа: опишите формальную семантику системы, опишите, что я хочу атаковать, а затем позвольте компьютеру выяснить, какую цепочку действий мне нужно использовать, чтобы захватить вашу систему.