В ЕС полный CRA, с ФМ всё куда хуже: с 11 декабря 2027-го активируется Cyber Resilience Act, и тогда все цифровые продукты должны будут соответствовать требованиям CRA. Для игр/утилит достаточно минимального подтверждения (хотя всё равно надо), а вот классов "Важные" и "Критические" требуется обязательная оценка соответствия CRA третьей стороной, а штрафы за несоблюдение могут достигать 15 млн. евро.

Механика у них и у нас в целом идентична: классифицируешь продукт, попадаешь в "критическую" категорию, платишь деньги чтобы кто-то подтвердил, что ты прошёл формальную проверку (экспертная организация или notified body), получаешь сертификат или декларацию.
Ну и саму формальную верификацию надо предварительно делать за свой счёт конечно.

За свой SaaS среднего уровня отвалишь от 5,000 евро только за сертификацию у аккредитованной лаборатории, а если продукт для более серьёзных целей, не обойтись без 500+ тыс. евро на одно только юридическое сопровождение.

При том, что сами по себе штрафы -- слабый стимул для глубокого внедрения формальных методов, т.к. они продвигают реактивную, а не проактивную культуру безопасности. Штрафы по сути налог на риск: проще заплатить если поймают, чем вкладываться в дорогую верификацию, и компании будут скорее скрывать утечки, а не вкладываться в их предотвращение, потому что для этого надо много дополнительно инвестировать по взрослому ещё с самого начала проекта - ну или бесконечно патчить легаси.

Это всё я к тому, что в целом польза от формальных методов огромна на всех уровнях, но участь их крайне печальна :) Продвигать ФМ тупым менеджерам, рассказывая про контракты, инварианты и TLA+ это гарантированный провал.

Ментатам на Функциональных архитектурах расскажу, как можно получить различную пользу от ФМ в своём проекте буквально за 1 день, и как это "упаковать и продать" хотя бы своему тимлиду/CTO.