Ну как, за миллион.... Год работы фристайл за 100k/месяц, отчёты раз в месяц, и вообще никто не трогает хоть целыми днями играй в HoMM и ACС.
Но я отказался: с (около)госами не хочу связываться принципиально, потом ещё и должен останешься, всю жизнь бесплатно сопровождать :)
Ну и цена раз в 5-10 должна быть больше.
А понадобилось, я так подозреваю, потому как если хочешь получить 4+ уровень доверия своей СЗИ, то нужно соответствовать приказу ФСТЭК России № 76 от 02.06.2020 по темке доказательства безопасности формальной математической модели твоей системы.
И кагбэ раньше практически официально рекомендовали Event-B and the Rodin Platform -- какую-то древнюю штуку 20-летней давности, созданную на гранты Евросоюза. Работает как плагин для Эклипса :) исходники до сих пор хостятся на сорсфорж...
Главное, Карл, "the use of set theory as a modelling notation"! Ну, да, тогда CIC и HoTT ещё не существовало, и что только не использовалось, кто во что горазд...
И вот под это дело (видимо, после 2022-го наступило какое-то прозрение :)
пацаны хочут "свой прувер" (дело-то благородное...).
Вообще, вряд ли в российской айтишке сегодня есть что-то более стратегически важное для КИИ -- и при этом абсолютно уязвимое -- чем "свой прувер". Сейчас всё, что есть в этой теме, активно развивается прежде всего европейскими организациями -- как в плане софта, так и в плане математики и, конечно, в плане обучения, со всеми вытекающими для РФ. Ну, да, пока опенсорс в основном...
В единственном русскоязычном чятике по соответствующим формальным технологиям все спецы работают за границей (от Европы и ОАЕ до США и Японии), или уже на чемоданах...
Как правильно: дать наконец МИАН и (последним) русским математикам денег на это всё. Пусть там сделают по-взрослому.
А впрочем, это же не миллиарды рублей