Talos: интерпретатор WebAssembly с формальными доказательствами на Lean

Talos решает классическую проблему: обычно есть интерпретатор для исполнения и отдельная спецификация для доказательств, которые со временем расходятся. Здесь обе роли выполняет один код на Lean 4. Проект под активной разработкой, пока покрывает подмножество Wasm (то, что генерируется компиляторами из Rust/C без оптимизаций), но целью стоит полная поддержка. Доказательства строятся на исчислении слабейших предусловий (WP calculus), что позволяет рассуждать по аналогии с программой в обратном направлении: от постусловия к предусловиям. Это дает структурированные, композиционные доказательства без повторного развёртывания интерпретатора на каждом шаге.

Ключевые факты

Одна кодовая база для исполнения и доказательства: отсутствует расхождение между спецификацией и реальностью
Поддержка исчисления слабейших предусловий (WP calculus) для структурированных, композиционных доказательств
Фокус на ясности рассуждений, а не на скорость: оптимизация производительности идёт вторично и должна быть отдельно доказана
Открытый исходный код под AGPL 3.0; монорепозиторий с тремя пакетами Lake (interpreter, codelib, programs)
Раннее развитие с активным сообществом, требует Lean 4 и инструменты WASM

Ред. В мире formal methods это называется синхронизацией спецификации, обычно проигрывается.

Почему это важно

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

Ред. Когда в вашей системе живут две версии истины, рано или поздно одна из них врёт.

Кому это важно

Этот проект адресован разработчикам компиляторов, авторам безопасностных стандартов и исследователям формальных методов. Если вы пишете обычное веб-приложение, это не для вас. Если вы ответственны за крупинку кода, от которой зависит безопасность критичной системы, это стоит внимательно рассмотреть.

Ред. Формальная верификация сейчас в примерно том же состоянии, что тестирование в 2000-м: есть, но ещё дорого.

Как это применить

Перепишите критичную часть вашего WebAssembly-стека на Lean и докажите в нём её корректность. Пока это имеет смысл для подмножества, которое Talos уже поддерживает (то есть для WASM, генерируемого из типизированных языков без aggressivной оптимизации). Если ваша система преимущественно собирается из Rust, это особенно актуально.

Ред. Проблема: доказательства пишутся медленнее, чем код. Проблема выше.

Можно ли доверять

Исходники лежат на GitHub, утверждения о корректности опираются на Lean's proof kernel, который годами прошёл внешнюю рецензию. Сам проект молодой и находится в стадии активной разработки (API и интерфейсы доказательств ещё могут измениться), но фундамент надежен.

Ред. Утверждение «доказано на Lean» примерно равносильно «проверено четырьмя независимыми аудиторами».

Риски и подводные камни

AGPL лицензия ограничит использование в закрытом коде. Проект в ранней стадии, поэтому документация скудна, а API нестабилен. Главное: производительность интерпретатора сознательно принесена в жертву ясности доказательств. Это не замена для высокооптимизированного Wasm-движка.

Ред. Если вам нужна скорость, это не ваш инструмент. Если вам нужна уверенность, это то, что вы искали.