(заключительное и спасибо за внимание; всё додумал с вашей помощью ❤️❤️❤️)

Насколько это всё серьёзно?

Навскидку, это прежде всего военные и аэрокосмические контракты, типа "Formal program verification in avionics certification"
Five years after the official adoption of the new DO-178C/ED-12C standard and its supplements, including the DO-333/ED-216 supplement on formal methods, no avionics-certification project has yet acknowledged using this new supplement. However, formal method technologies do exist that would ease the development of avionics software.

У них там преимущественно, формально верифицируется Язык Ада :)

Суммы? Georgia Tech Applied Research Corporation, Atlanta, Georgia, was awarded a $8,051,218 cost-plus-fixed-fee task order for development of a software-based system certification tool. Air Force Research Laboratory, Eglin Air Force Base, Florida, is the contracting activity

Думаете, у нас хотя бы 8 млн рублей МИАН Стеклова на подобное получил? Фиг.

Шикарный свежий обзор темки от индуса:
evolution-formal-verification-from-theory-to-industry (впн)

Короче говоря, я буду следовать роадмапу, который предлагает Центр технической информации Пентагона в своём контракте с Карнеги-Меллоном "Formal Verification of Mathematics in HoTT-Lean" (впн)

This project was used to support the research group in Formalization of Mathematics in the Homotopy Type Theory system, implemented in the Lean proof assistant at Carnegie Mellon University... Using this breakthrough, new computer systems are being developed for the formal verification of mathematical theorems and critical computer software.

(на лине делают, ха-ха, дурачки, стратегическая ошибка 😎 лин4 с 3м несовместим, и от хотт отказался)

И в заключение остаётся взять какую-то тестовую, но достаточно показательную задачу, по которой можно было бы сравнивать простоту и производительность моей реализации со всеми Этими. Далеко ходить не надо:

The value of the 5-state winning busy beaver was discovered by Heiner Marxen and Jürgen Buntrock in 1989, but only proved to be the winning fifth busy beaver — stylized as BB(5) — in 2024 using a proof in Rocq.

Вот для наглядности и реализую задачку поиска и конструирования Усердных Бобров (что это??) с 2-3-4-5 состояниями, и сравним (для шести состояний так-то надо 2,5 ⋅ 10^2879 шагов).

В тему: "Ехали тьюрмиты и тримувьи на машите Тьюринга"