Вы спрашивали про формальную верификацию. Сегодня добрался до нее. Теперь могу ответить. Есть несколько способов её осуществить в OCaml-приложении.

1.Gospel (синтаксис формальной спецификации встраиваемой в исходный код).

1.1. Ortac/wrapper → runtime-ассерты в сгенерированной обёртке (поймает нарушение во время исполнения). Рабочий вариант. Ortac-wrapper генерирует исполняемый код и встраивает в него утверждения (asserts). Этот assert должен реально исполниться, что предъявляет определенные требования к исходному коду.

1.2. Ortac/qcheck-stm → QCheck-тесты, проверяющие спеку на случайных сценариях (поймает нарушение при фаззинге). На практике не пробовал.

1.3. Monolith → направленный фаззинг по спеке. На практике не пробовал.

1.4. Cameleer → Why3 → статическое доказательство через SMT (поймает нарушение на уровне кода без запуска). Вот этот вариант был бы очень интересен и через единую Gospel-спецификацию позволил бы применить практически все формальные доказатели. Но запустить не удалось, т.к. требует версию Gospel, которая не поддерживает OCaml 5.2+. А посему пришлось рассмотреть следующий вариант.

2. Why3 (формальная спецификация в отдельных *.mlw файлах)

В Why3 всё иначе. Why3 ничего в рантайме не делает - он доказывает формулы на бумаге (в SMT-решателе). Поддерживает три SMT-решателя.

2.1. Z3 (Microsoft Research) - лучше покрывает bitvectors, нелинейную арифметику, quantifier instantiation с эвристиками, и часто доказывает то, что Alt-Ergo не тянет (и наоборот). На практике реализован.

2.2. Alt-Ergo (OCaml, INRIA/OCamlPro) - исторически заточен под Why3, хорошо справляется с линейной арифметикой, теориями записей, некоторыми индуктивными паттернами. Может работать и без Why3 - он понимает собственный синтаксис .ae и стандартный .smt2 (SMT-LIB). На практике реализован через Why3 спецификацию в *.mlw файлах.

2.3. CVC5 — третий популярный, полезен в тех же нишах, что Z3. На практике не пробовал.

Посмотреть можно в *.wml файлах здесь:
https://github.com/krew-solutions/trading-ml/tree/main/lib/domain

Из интересного - если код имеет side-effect, то доказатель его не станет доказывать. Доказать можно только чистую функциональную парадигму. Это обязывает следить за функциональной чистотой и изоляцией доменной логики. И это еще одна из причин, почему мой интерес сместился с OOP на FP.

Еще успел реализовать Railway Oriented Programming by Scott Wlaschin. Пока только один pipeline, посмотреть можно здесь:
https://github.com/krew-solutions/trading-ml/tree/main/lib/application