Investigadores del MIT, Carnegie Mellon, Google y ETH Zúrich presentan la primera cadena de herramientas de desarrollo de software capaz de generar demostraciones de primer principio sobre cotas temporales concretas para código máquina interactivo, manteniendo toda la programación y verificación a nivel de código fuente. El trabajo, publicado en CPP '26 (Rennes, 12-13 de enero de 2026), permite demostrar programas en estilo C frente a especificaciones de lógica de separación que también restringen su tiempo de ejecución, componiendo esas demostraciones con la verificación de un compilador hacia código máquina RISC-V.
La motivación se sitúa en sistemas ciberfísicos de tiempo real, donde los plazos dependen de lecturas de sensores —por ejemplo, cerrar una válvula solo cuando un sensor detecta que un depósito está a punto de desbordarse— y donde un fallo por exceso de latencia puede dañar maquinaria industrial. Los autores argumentan que los análisis estáticos automáticos y las herramientas semi-automatizadas basadas en lógica de Hoare son software complejo y propenso a errores, por lo que optan por un enfoque foundational: probar juntos aplicación, herramientas de verificación y compilador dentro del asistente de pruebas Rocq.
El artículo introduce un estilo de especificación que combina trazas de eventos de E/S con estado fantasma para métricas temporales. Tras pasar por la cadena, el resultado es un teorema Rocq cuyas hipótesis dependen únicamente de la semántica formal de RISC-V y de construcciones de especificación básicas. Como caso de estudio culminante, los autores ampliaron una verificación previa de un sistema ciberfísico basado en microcontrolador para acotar el tiempo entre la llegada de paquetes de red y la actuación del dispositivo conectado. El modelo de costo mide, entre otros, número de instrucciones ensamblador, accesos a memoria y saltos, lo que permite obtener cotas conservadoras del tiempo de reloj en microcontroladores con cachés mínimas, aunque potencialmente pesimistas en procesadores más complejos.