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.
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…