Você construiu um sistema n-version. Três implementações independentes da mesma função crítica, um voter que escolhe o resultado da maioria, e uma sensação de que enganou os pontos únicos de falha.

Você não provou que as funções são equivalentes. Você apenas provou que elas compilam.

Por que a equivalência é a base oculta da programação n-version

A programação n-version é a ideia de que, se uma implementação tem um bug, as outras provavelmente não terão, então um voter pode descartar outliers. Isso assume que as saídas são comparáveis.

Se a função A retorna um float e a função B retorna uma string, o voter não tem base para se sustentar. Mas mesmo com tipos compatíveis, diferenças semânticas te matam. Uma ordena de forma crescente, a outra de forma decrescente. Uma arredonda metade para cima, a outra arredonda metade para o par mais próximo. O voter vê três respostas diferentes e não tem uma forma principiada de escolher.

A literatura sobre programação n-version está cheia de estudos mostrando que programas escritos independentemente frequentemente falham de formas correlacionadas. Programadores cometem os mesmos erros. Eles interpretam mal as mesmas especificações ambíguas. Se sua especificação é “ordene esta lista”, e um programador implementa quicksort enquanto outro implementa mergesort, você pode assumir que são equivalentes. E são, até que você pergunte sobre estabilidade. Ou até que a entrada contenha NaN.

A maioria das equipes ignora a verificação de equivalência porque parece trabalho extra. Não é. É o trabalho que dá sentido ao resto do sistema.

Por que sua test suite está te dando falsa confiança

Você escreve testes unitários. Ambas as funções passam. Você declara vitória.

Isso é um erro de categoria. Testes podem provar a presença de bugs, nunca sua ausência. Com espaços de entrada infinitos, ou mesmo apenas grandes espaços finitos, sua cobertura de testes é um erro de arredondamento. Duas funções podem concordar em todos os casos que você pensou e divergir no que importa às 3 da manhã em produção.

Aprendi isso na prática em um projeto com dois parsers JSON. Um usava o json.loads embutido do Python, o outro usava um parser feito à mão para performance. Nossa test suite tinha cinquenta casos. Ambos passaram. Em produção, um cliente enviou um objeto JSON com uma chave duplicada. O parser do Python manteve o último valor. Nosso parser feito à mão manteve o primeiro. O voter viu dois objetos diferentes e entrou em pânico.

O property-based testing chega mais perto. Em vez de escolher inputs manualmente, você descreve as propriedades que ambas as funções devem satisfazer e deixa que um gerador busque contraexemplos. Aqui está um exemplo real usando a biblioteca Hypothesis do 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()

Execute isso e o Hypothesis rapidamente encontrará um contraexemplo. round_half_up(2.5) retorna 3. O round(2.5) embutido do Python retorna 2 porque usa o arredondamento de banqueiro (banker’s rounding), que arredonda para o número par mais próximo. Ambas as funções são “corretas” por algum padrão. Elas não são equivalentes.

O property-based testing não provará equivalência. Ele encontrará os casos de borda que seus testes unitários perderam. Isso é valioso, mas ainda é falsificação, não verificação.

Como os solvers SMT podem de fato provar equivalência

Se você quer uma prova, precisa sair da zona de conforto dos testes e entrar no mundo dos solvers SMT. A ideia é simples. Codifique ambas as funções como fórmulas lógicas e pergunte ao solver se existe algum input em que elas diferem.

Para domínios limitados, isso é mecânico. Aqui está um exemplo usando Z3 para provar que duas implementações de max para inteiros são 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

O Z3 retorna unsat, o que significa que não existe contraexemplo. As funções são equivalentes para todos os inteiros no modelo do Z3. Isso é uma prova real, limitada à teoria sobre a qual o Z3 está raciocinando.

Você pode fazer isso para funções mais complexas também. O truque é expressar suas funções como fórmulas lógicas. Para loops, você os desenrola. Para arrays, você usa a teoria de arrays do Z3. Para ponto flutuante, você usa a teoria FP do Z3 e aceita que o solver pode atingir o timeout em expressões complexas.

A lacuna entre “mecânico” e “fácil” é onde a maioria das equipes fica travada. Traduzir uma função Python para a linguagem do Z3 requer entender ambas. Mas uma vez que você tem a tradução, o solver faz o trabalho difícil.

A tabela de trade-offs que ninguém quer publicar

A verificação formal completa, provando equivalência para todos os inputs possíveis incluindo cada caso de borda do IEEE 754, é possível. As pessoas fazem isso para primitivas criptográficas e sistemas de aviônica. Custa semanas ou meses de tempo de especialista e requer ferramentas como Coq ou Isabelle.

O property-based testing custa minutos e captura bugs reais, mas não oferece garantias.

A verificação limitada com solvers SMT fica no meio. Ela te dá uma garantia para um escopo bem definido. Esse escopo pode cobrir 99,9% dos seus inputs de produção. Se isso é bom o suficiente depende do que a falha custa.

Não existe almoço grátis. Escolha a ferramenta que corresponde à sua tolerância a riscos e à expertise da sua equipe.

Um voter que sabe quando desistir

A maioria dos sistemas n-version implementa um voter majoritário ingênuo: retorna o resultado mais comum, ou falha se não houver maioria. Um voter melhor conhece sua própria ignorância.

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")

Quando o voter vê desacordo persistente em classes específicas de input, isso é um sinal. Ou sua suposição de equivalência está errada, ou você encontrou um bug em uma das implementações. Ambos valem a pena ser conhecidos.

O voter não está ali apenas para escolher vencedores. Ele está ali para te dizer quando suas suposições sobre equivalência estavam erradas.

O que fazer de fato em seguida

Comece com property-based testing. É barato, encontra bugs, e te força a articular o que “equivalência” significa para o seu domínio. São saídas idênticas bit a bit? Saídas dentro de algum epsilon? Saídas que satisfazem a mesma pós-condição?

Uma vez que você definiu equivalência precisamente, mude para verificação limitada se o domínio é finito e os riscos são altos. Use Z3, CBMC, ou uma ferramenta similar para obter uma prova mecânica para seu escopo limitado.

Reserve a verificação formal completa para as partes onde um bug literalmente mata pessoas. Para todo o resto, conheça os limites da sua prova e monitore por desacordos em produção. O melhor sistema n-version é aquele que sabe o que não sabe.