Здравствуйте, koenig, Вы писали:

С>>А в случае известного мне вида доказуемого кода, тесты — это декларации о том, что должен делать код, а сверкой деклараций и самого кода занимается верификатор, SMT.

K>вид известен, а код — нет, т.к. написать его ни у кого сил не хватает
K>в отличие от презренных тестов и т.п.

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