Los LLMs pueden generar código en Rust. Las pruebas formales son un problema completamente distinto.
Los grandes modelos de lenguaje escriben código en Rust sorprendentemente bueno, pero cuando les pides una prueba formal alucinan invariantes e inventan sintaxis que ningún verificador acepta. Esto es lo que realmente hacen bien, dónde fallan y cómo usarlos de todos modos.
