5 posts
Cleanroom software engineering prometió incrementos zero-defect mediante mathematical verification en lugar de debugging. Analizamos los datos reales del proyecto de IBM para ver si la afirmación se sostuvo.
El promedio de la industria del software en la década de 1980 era de 30 a 60 defectos por mil líneas de código. El equipo Cleanroom de IBM entregó un…
AutoVerus utiliza una red de agentes LLM para generar proofs de corrección de Verus para código Rust, automatizando más del 90% de las proof obligations mediante un bucle de generar-reparar-dischargar impulsado por el feedback del solver SMT.
La parte más difícil de la verificación formal nunca ha sido el verificador. Es escribir el proof. Dale a un ingeniero senior de Rust Verus, el verificador…
Los bounded model checkers como Kani y los relational model finders como Alloy permiten verificar propiedades con assertions y constraints ordinarios. Renuncias a las pruebas de liveness a cambio de una curva de aprendizaje medida en horas, no en semanas.
No necesitas aprender lógica temporal lineal para usar un model checker. Herramientas como Kani, CBMC y Alloy te permiten verificar propiedades con assertions…
Herramientas de model checking como Kani te permiten verificar propiedades de Rust con assertions en lugar de pruebas formales. El problema es lo que ocurre cuando tus bucles no tienen límites pequeños.
Puedes probar que tu código Rust es correcto sin escribir una sola prueba. La herramienta que lo hace se llama model checker, y para Rust el más práctico en…
La programación en N versiones asume que tus implementaciones coinciden. Analizamos por qué las pruebas no bastan, cómo los solucionadores SMT pueden demostrar equivalencia realmente y dónde trazar la línea entre lo suficientemente bueno y lo formalmente verificado.
Construiste un sistema de N versiones. Tres implementaciones independientes de la misma función crítica, un votante que elige el resultado mayoritario y una…