Интерпретатор Wasm, который одновременно доказывает свою правоту

Talos не разделяет код, который запускает WebAssembly, и код, который описывает её правила. В одном репозитории на Lean 4 одни и те же определения выполняют Wasm-инструкции и служат основой для рассуждений о них.

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

Код лежит на GitHub.