Creusot — это дедуктивный верификатор для Rust-кода. Он проверяет, что ваш код не паникует, не ловится на переполнении и не содержит проваленных утверждений. Если добавить аннотации, можно пойти дальше: убедиться, что программа делает именно то, что задумано.
Как это работает: Creusot транслирует Rust-код в Coma — промежуточный язык верификации платформы Why3. Дальше подключается вся мощь Why3, которая (полу)автоматически доказывает условия корректности. Технические детали лежат в ARCHITECTURE.md.
Если понадобится помощь или захочется обсудить — есть форум и Zulip-чат. В академических публикациях Creusot ссылаются на доклад ICFEM'22. Чтобы посмотреть, как выглядит верификация на практике, стоит заглянуть в подборку тестов — примеры лежат в examples и tests/should_succeed.
Крупный проект на базе Creusot — CreuSAT, верифицированный SAT-решатель, написанный на Rust. Он реально нагружает инструмент до предела и даёт представление, что значит «использовать всерьёз». Ещё один большой проект в разработке.
Установка: сначала ставят rustup для нужного тулчейна Rust, затем opam — менеджер пакетов OCaml. Клонируют репозиторий Creusot с GitHub и переходят в папку creusot. После этого устанавливают сам Creusot. Проверить успех установки можно отдельной командой. Гайд по установке — в документации Creusot.
Чтобы обновить уже установленный Creusot: заходят в ту же папку репозитория, обновляют исходники, папку с пакетами opam и переустанавливают Creusot. Информация для разработчиков, кто хочет копаться в кодовой базе, — в CONTRIBUTING.md.