Investigadores presentan C*, una extensión del lenguaje C que incorpora de forma nativa capacidades de verificación formal, con el objetivo de acercar las prácticas de demostración de correctitud a los programadores de sistemas. El trabajo, publicado en arXiv el 3 de abril de 2025, aborda una de las principales barreras de la verificación de software de sistemas: la separación entre los entornos y paradigmas de programación y de prueba, que limita la accesibilidad y la verificación en tiempo real.
C* añade a C bloques de código de demostración que se intercalan con el código de implementación y permiten actualizar de forma interactiva el estado de la prueba. El diseño se apoya en un motor de ejecución simbólica y en un núcleo de pruebas de estilo LCF (Logic for Computable Functions), lo que habilita la construcción de bibliotecas reutilizables de definiciones lógicas, teoremas y automatización programable de pruebas. La pieza clave es que implementación y demostración comparten el propio C como lenguaje común.
Los autores implementaron un prototipo y lo evaluaron con un banco de pruebas de programas pequeños en C y con un caso real exigente: la función attach del asignador buddy de pKVM, el hipervisor basado en Linux para KVM protegido. Los resultados indican que C* admite la verificación de un amplio abanico de patrones idiomáticos de C y resuelve tareas de razonamiento complejas en escenarios reales, sugiriendo una vía para reducir los costes de desarrollo y mantenimiento del software verificado sin obligar a los programadores a cambiar de entorno.