El equipo de Creusot ha lanzado la versión 0.14.0 de su herramienta de verificación formal para Rust, destacando mejoras significativas en la gestión de órdenes parciales y la generación de condiciones de verificación. Esta actualización, publicada el 9 de octubre de 2026, permite a los desarrolladores especificar estructuras de datos que no siguen una orden total, utilizando una función de comparación lógica que es irreflexiva y transitiva, lo que facilita la modelado de tipos más complejos sin afectar a las pruebas existentes.
Además, Creusot ahora genera condiciones de verificación (VC) para 'snapshots', expresiones lógicas incrustadas en el código. Esta función permite utilizar funciones de prueba como 'lemma functions' de manera más precisa, eliminando la necesidad de que el probador resuelva cuantificadores universales manualmente. La integración con rust-analyzer también ha sido mejorada, permitiendo ahora la navegación 'Go-to-definition' en especificaciones Pearlite. Para lograrlo, el equipo ajustó los spans de los tokens para que el analizador solo busque definiciones relevantes, mejorando la experiencia de desarrollo al reducir los resultados irrelevantes. Estas mejoras buscan cerrar la brecha entre la programación y la verificación formal, permitiendo a los desarrolladores escribir especificaciones más naturales y mantenibles.