Talos — это WebAssembly-интерпретатор на Lean 4, названный в честь бронзового гиганта из греческой мифологии, охранявшего Крит. Идея простая: одни и те же определения, которые исполняют Wasm-программу, используются и для доказательств о её поведении. Никакого отдельного спека, который нужно синхронизировать. Оценка и доказательство живут в одном коде.
Проект в активной разработке, API и интерфейсы доказательств могут меняться. Цель — сделать feature-complete, исполняемую семантику WebAssembly, которая одновременно является формальным объектом. Можно запускать программы на конкретных входных данных, а можно формулировать и доказывать теоремы — корректность относительно спецификации, эквивалентность программ, свойства, которые выполняются для всех входов. Всё это через встроенные средства доказательств Lean.
Интерпретатор намеренно оптимизирован для ясности рассуждений, а не для скорости. Полное покрытие Wasm в планах, но сейчас Talos фокусируется на подмножестве фич, которые естественно возникают в неоптимизированном коде из Rust, C и т.п. — то есть на семантике, важной для верификации того, что программа делает, а не как быстро.
Доказательства строятся на слабейшем предусловии (weakest precondition calculus) — предикат-трансформерная семантика позволяет рассуждать задом наперёд: от постусловий к тем предусловиям, которые их гарантируют. Это даёт композициональные доказательства для циклов, ветвлений и вызовов функций, не переразворачивая интерпретатор на каждом шаге.
Примеры использования: запустить .wat-модуль можно через lake exe runner samples/factorial.wat fact 5, получить 120. Можно ограничить количество шагов топлива (по умолчанию 1 000 000). Для доказательства есть файл interpreter/Interpreter/Wasm/Examples/Factorial.lean — полное доказательство корректности с помощью WP-тактик.
Проект состоит из трёх пакетов в одном монорепозитории с жёсткой цепочкой зависимостей: Interpreter (AST Wasm, семантика, WP-тактики), CodeLib (вспомогательные леммы и хелперы для рассуждений), Programs (конкретные задачи верификации Rust-to-Wasm). CodeLib реэкспортирует нужные части интерпретатора, чтобы downstream-код не импортировал его напрямую.
Собрать всё можно одной командой just build или по отдельности через lake build в каждом пакете. Зависимости: Lean 4 (скачивается через elan) и wasm-tools (через brew или cargo). Лицензия — GNU Affero General Public License v3.0.