[spoiler]Подобные технологии разрабатываются давно, и наработки существуют неплохие, но пока они не стали массовой практикой -- например, из-за сложности и ограниченности применения. Некоторые особо строгие стандарты сертификации защищенных систем подразумевают подобную формальную проверку, но пока удавалось проверять объемы кода в ограниченных пределах, до 10 тыс. строк кода (по кр. мере, официально сообщалось о таких объемах).
Чипы сегодня встраиваются куда только можно -- и в современном автомобиле программного кода уже больше, нежели в коммерческом авиалайнере (цикл проектирования самолетов гораздо дольше). И, соответственно, по мере всеобщей автоматизации растет и потенциальная опасность программных ошибок (например, известны случаи трагических сбоев медицинской цифровой аппаратуры).
Одна из компаний, наиболее активно инвестирующих в сферу математического доказательства -- MathWorks. Она готовит, по словам ее менеджера по аэрокосмической и оборонной индустрии Джона Фридмана, "новый класс верификационных инструментов", которые потенциально способны обеспечить абсолютную корректность кода. Еще один из редких игроков в этой узкой из-за высокого порога вхождения, но крайне перспективной нише -- компания LDRA, предлагающая верификационный софт для всего жизненного цикла. 20-го августа она, кстати, отметила юбилей своего индийского офиса, который активно взаимодействует с местными государственными структурами -- оборонными, космическими, ядерными, транспортными и др. Занимается она в Индии, что немаловажно, интенсивным обучением, семинарами по IEC 61508, DO-178B, IEC 62304, ISO 26262, MISRA C++, CERT C, работает в организациях, занимающихся стандартизацией программной инженерии...
А почему в России ее представительства нету? Сомневаюсь, что у нас имеются продвинутые компании схожего профиля -- судя хотя бы по падающим в океаны ракетам...
Спасибо про Ульяновск! Попробую с ними связаться.
Её обитатели собираются оперативно принять поправки к Закону всемирного тяготения.