Coq и Gallina под ключ: строгие доказательства для критичного кода

Занимаюсь инженерией доказательств на базе интерактивной системы Coq и языка спецификаций Gallina. Смысл моей работы прост: там, где раньше стояло «вроде бы верно», должно появиться утверждение, истинность которого подтверждает компьютер, а не человеческая интуиция. Вы приносите алгоритм, сетевой протокол или математическую задачу — я формулирую её спецификацию на Gallina и вручную, шаг за шагом, довожу до конца доказательство того, что код действительно ей отвечает, не пропуская ни одной ветки рассуждения. Здесь нет места допущениям: любая лемма строго выводится и повторно проверяется инструментом coqc при каждой сборке проекта. Чаще всего меня зовут доказать инварианты структур данных, показать, что рекурсивные функции завершаются и считают правильно, перевести на язык машины теоремы из алгебры, логики или комбинаторики, описать автоматы для свойств безопасности и многопоточности. Уверенно работаю с тактиками Ltac и Ltac2, методикой SSReflect и библиотекой Mathematical Components, зависимыми типами, обоснованной рекурсией и индуктивными предикатами. После того как все цели закрыты, запускаю извлечение Coq и получаю аккуратный рабочий код на OCaml, а при запросе — на Haskell или Scheme, так что доказанные свойства доходят до боевого окружения. В комплекте идут: собранная без admit и посторонних аксиом разработка на Coq, понятная спецификация, извлечённый и проверенный модуль и небольшой разбор того, что теоремы гарантируют и чего они не покрывают. За плечами — механизация этапов компилятора, проверка арифметических и криптографических примитивов, починка доказательств, развалившихся после обновления библиотек. Нужна не строчка в отчёте о тестах, а настоящая уверенность — сделаю результат, верный по построению и устойчивый к дальнейшим правкам.