Talos es un intérprete de WebAssembly escrito en Lean 4 cuyo objetivo no es la velocidad de ejecución, sino servir como objeto formal sobre el que demostrar propiedades. La misma definición que ejecuta un programa Wasm es la que se emplea para razonar, lo que elimina la necesidad de mantener un intérprete de especificación aparte sincronizado con el motor real. Está desarrollado por cajal-technologies, se distribuye bajo licencia AGPL v3 y su desarrollo es activo, por lo que las API y las interfaces de prueba pueden cambiar.
El proyecto adopta el cálculo de precondición más débil (WP) como base de las demostraciones, un marco de transformadores de predicados que permite razonar hacia atrás desde las postcondiciones hasta las precondiciones que las garantizan. Esto facilita pruebas estructuradas y composicionales de bucles, bifurcaciones y llamadas a función, sin necesidad de desplegar el intérprete en cada paso. Se busca una cobertura completa de Wasm, pero la prioridad inmediata son las características que aparecen de forma natural al compilar código fuente de alto nivel sin optimizar (Rust, C, etc.), las semánticas relevantes cuando se quiere verificar qué hace un programa y no su rendimiento.
El monorepo se organiza en tres paquetes Lake con una cadena de dependencias estricta: Interpreter, que contiene el AST de Wasm, la semántica y la capa de tácticas WP; CodeLib, con lemas de lifting y utilidades de razonamiento; y Programs, con tareas concretas de verificación de Rust compilado a Wasm. CodeLib reexporta las partes del intérprete que las demostraciones aguas abajo necesitan, de modo que el código que la importa no requiere importar el intérprete directamente. Para ejecutar un módulo .wat basta con lanzar el runner incluido con un límite de pasos configurable (1.000.000 por defecto). El repositorio incluye además un ejemplo completo de corrección del factorial mediante la capa de tácticas WP, así como la integración con wasm-tools para validar binarios y la Wasm testsuite.