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 sensación de seguridad de que has superado los puntos únicos de fallo.

No has demostrado que las funciones sean equivalentes. Solo has demostrado que compilan.

Por qué la equivalencia es el cimiento oculto de la programación en N versiones

La programación en N versiones parte de la idea de que si una implementación tiene un error, las demás probablemente no lo tendrán, así que un votante puede descartar los valores atípicos. Esto asume que las salidas son comparables.

Si la función A devuelve un float y la función B devuelve un string, el votante no tiene base para decidir. Pero incluso con tipos coincidentes, las diferencias semánticas te arruinan. Una ordena de forma ascendente, otra de forma descendente. Una redondea por exceso a la mitad, otra redondea a la mitad hacia el par más cercano. El votante ve tres respuestas diferentes y no tiene una forma fundamentada de elegir.

La literatura sobre programación en N versiones está llena de estudios que demuestran que programas escritos de forma independiente a menudo fallan de maneras correlacionadas. Los programadores cometen los mismos errores. Leen mal las mismas especificaciones ambiguas. Si tu especificación es “ordena esta lista”, y un programador implementa quicksort mientras otro implementa mergesort, podrías asumir que son equivalentes. Lo son, hasta que preguntas sobre estabilidad. O hasta que la entrada contiene NaN.

La mayoría de los equipos omiten la verificación de equivalencia porque parece trabajo extra. No lo es. Es el trabajo que le da sentido al resto del sistema.

Por qué tu batería de pruebas te da una falsa confianza

Escribes unit tests. Ambas funciones pasan. Declaras la victoria.

Eso es un error de categoría. Las pruebas pueden demostrar la presencia de errores, nunca su ausencia. Con espacios de entrada infinitos, o incluso solo finitos pero grandes, tu cobertura de pruebas es un error de redondeo. Dos funciones pueden coincidir en cada caso que se te ocurrió y divergir en el que importa a las 3 de la mañana en producción.

Aprendí esto por las malas en un proyecto con dos analizadores JSON. Uno usaba json.loads integrado de Python, el otro usaba un analizador hecho a mano por rendimiento. Nuestra batería de pruebas tenía cincuenta casos. Ambos pasaron. En producción, un cliente envió un objeto JSON con una clave duplicada. El analizador de Python conservó el último valor. Nuestro analizador hecho a mano conservó el primero. El votante vio dos objetos diferentes y entró en pánico.

Las pruebas basadas en propiedades se acercan más. En lugar de seleccionar entradas a mano, describes las propiedades que ambas funciones deben satisfacer y dejas que un generador busque contraejemplos. Aquí tienes un ejemplo real usando la biblioteca Hypothesis de Python:

from hypothesis import given, strategies as st
import math

def round_half_up(n):
    return math.floor(n + 0.5)

@given(st.floats(allow_nan=False, allow_infinity=False))
def test_rounding_equivalence(n):
    assert round_half_up(n) == round(n)

if __name__ == "__main__":
    test_rounding_equivalence()

Ejecuta esto y Hypothesis encontrará rápidamente un contraejemplo. round_half_up(2.5) devuelve 3. La función integrada round(2.5) de Python devuelve 2 porque usa banker’s rounding, que redondea al número par más cercano. Ambas funciones son “correctas” según algún estándar. No son equivalentes.

Las pruebas basadas en propiedades no demostrarán equivalencia. Encontrarán los casos límite que tus unit tests omitieron. Eso es valioso, pero sigue siendo falsificación, no verificación.

Cómo los solucionadores SMT pueden demostrar equivalencia realmente

Si quieres una demostración, necesitas salir de la zona de confort de las pruebas y entrar al mundo de los solucionadores SMT. La idea es sencilla. Codifica ambas funciones como fórmulas lógicas y pregúntale al solucionador si existe alguna entrada en la que difieran.

Para dominios acotados, esto es mecánico. Aquí tienes un ejemplo usando Z3 para demostrar que dos implementaciones de max con enteros son equivalentes:

from z3 import Int, Solver, If, Abs

x = Int('x')
y = Int('y')

# Standard max implementation
max_standard = If(x > y, x, y)

# Algebraic max: (x + y + abs(x - y)) / 2
max_algebraic = (x + y + Abs(x - y)) / 2

solver = Solver()
solver.add(max_standard != max_algebraic)
result = solver.check()
print(result)  # unsat

Z3 devuelve unsat, lo que significa que no existe ningún contraejemplo. Las funciones son equivalentes para todos los enteros en el modelo de Z3. Esa es una demostración real, acotada a la teoría sobre la que Z3 está razonando.

Puedes hacer esto para funciones más complejas también. El truco consiste en expresar tus funciones como fórmulas lógicas. Para bucles, los desenrollas. Para arreglos, usas la teoría de arreglos de Z3. Para punto flotante, usas la teoría FP de Z3 y aceptas que el solucionador podría agotar el timeout en expresiones complejas.

La brecha entre “mecánico” y “fácil” es donde la mayoría de los equipos se atascan. Traducir una función de Python al lenguaje de Z3 requiere entender ambos. Pero una vez que tienes la traducción, el solucionador hace el trabajo duro.

La tabla de compensaciones que nadie quiere publicar

La verificación formal completa, demostrando equivalencia para todas las entradas posibles incluyendo cada caso límite de IEEE 754, es posible. La gente lo hace para primitivas criptográficas y sistemas de aviónica. Cuesta semanas o meses de tiempo de expertos y requiere herramientas como Coq o Isabelle.

Las pruebas basadas en propiedades cuestan minutos y detectan errores reales, pero no ofrecen garantías.

La verificación acotada con solucionadores SMT se sitúa en el medio. Te da una garantía para un ámbito bien definido. Ese ámbito podría cubrir el 99,9% de tus entradas de producción. Si eso es suficientemente bueno depende de lo que cueste el fallo.

No hay comida gratis. Elige la herramienta que se ajuste a tu tolerancia al riesgo y a la experiencia de tu equipo.

Un votante que sabe cuándo rendirse

La mayoría de los sistemas de N versiones implementan un votante mayoritario ingenuo: devolver el resultado más común, o fallar si no hay mayoría. Un votante mejor conoce su propia ignorancia.

from collections import Counter

def naive_voter(results):
    if not results:
        raise ValueError("No results to vote on")
    counts = Counter(results)
    winner, count = counts.most_common(1)[0]
    if count > len(results) / 2:
        return winner
    raise ValueError("No majority found")

def informed_voter(results, input_sample=None):
    if not results:
        raise ValueError("No results to vote on")

    distinct = set(results)
    if len(distinct) == 1:
        return results[0]

    # Log disagreement for later analysis
    if input_sample is not None:
        print(f"Disagreement on input {input_sample}: {distinct}")

    counts = Counter(results)
    winner, count = counts.most_common(1)[0]
    if count > len(results) / 2:
        return winner

    raise ValueError("No majority found")

Cuando el votante ve desacuerdos persistentes en clases de entrada específicas, esa es una señal. O tu suposición de equivalencia es incorrecta, o has encontrado un error en una de las implementaciones. Ambos merecen saberse.

El votante no está solo ahí para elegir ganadores. Está ahí para decirte cuándo tus suposiciones sobre la equivalencia estaban equivocadas.

Qué hacer realmente a continuación

Empieza con pruebas basadas en propiedades. Son baratas, encuentran errores y te obligan a articular qué significa “equivalencia” para tu dominio. ¿Es salidas idénticas bit a bit? ¿Salidas dentro de algún epsilon? ¿Salidas que satisfacen la misma postcondición?

Una vez que hayas definido la equivalencia con precisión, pasa a la verificación acotada si el dominio es finito y el riesgo es alto. Usa Z3, CBMC o una herramienta similar para obtener una demostración mecánica para tu ámbito acotado.

Reserva la verificación formal completa para las partes donde un error literalmente mata gente. Para todo lo demás, conoce los límites de tu demostración y monitorea los desacuerdos en producción. El mejor sistema de N versiones es aquel que sabe lo que no sabe.