verification

7 artículos

23 ago 2026

La ejecución simbólica encontró un integer overflow que mi cobertura de tests del 94% se perdió

Tus unit tests comprueban entradas específicas. La ejecución simbólica comprueba cada entrada posible. Así es como funciona, qué cuesta y por dónde empezar.

3 ago 2026

Cómo demostrar que tu código no tiene errores en tiempo de ejecución (y por qué probablemente desistirás)

La interpretación abstracta te permite probar que ciertos errores en tiempo de ejecución son imposibles antes de ejecutar el código. Así es como funciona en realidad, por qué es difícil y dónde encaja en tu cadena de herramientas.

abstract-interpretation static-analysis runtime-errors verification

25 jul 2026

¿Alguien realmente verificó 10.000 líneas con cero defectos? IBM lo hizo, y la metodología es más extraña que el resultado.

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.

cleanroom-correctness zero-defects verification case-study

9 jul 2026

AutoVerus convierte 40 horas de escritura de proofs en 3 llamadas a LLM. El truco es saber cuándo rendirse.

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.

model-checking autoverus rust verification

6 jul 2026

Puedes verificar código con model checking sin aprender temporal logic

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.

model-checking temporal-logic formal-methods verification

5 jul 2026

Puedes probar que tu código Rust es correcto sin escribir una sola prueba, pero el espacio de estados es la factura

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.

model-checking rust verification formal-methods

14 jun 2026

Las pruebas no demostrarán que dos funciones sean equivalentes. Esto es lo que sí lo hará.

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.

n-version-programming equivalence-testing formal-methods verification