Basis hace que los LLM demuestren que su semántica coincide con el intérprete real

Ship Your Interpreter

Basis usó LLM para escribir una semántica formal de un pequeño lenguaje en Lean y probar que predice exactamente lo que imprime el intérprete en C una vez compilado a RISC-V. El experimento revela que una semántica puede pasar todas las pruebas y aun así estar mal: la suya fallaba al concatenar funciones con nombres de 59 caracteres por un límite de 64 bytes en el buffer de `snprintf`. La conclusión es que el cuello de botella de la verificación se desplaza de la demostración a la especificación.