Du hast ein n-version-System gebaut. Drei unabh�ngige Implementierungen derselben kritischen Funktion, ein Voter, der das Mehrheitsergebnis w�hlt, und ein gutes Gef�hl, dass du Single Points of Failure ausgetrickst hast.

Du hast nicht bewiesen, dass die Funktionen �quivalent sind. Du hast nur bewiesen, dass sie kompilieren.

Warum �quivalenz das verborgene Fundament von n-version programming ist

N-version programming beruht auf der Idee, dass wenn eine Implementierung einen Bug hat, die anderen ihn wahrscheinlich nicht haben, sodass ein Voter Ausrei�er verwerfen kann. Das setzt voraus, dass die Outputs vergleichbar sind.

Wenn Funktion A einen Float und Funktion B einen String zur�ckgibt, hat der Voter keinen Boden unter den F��en. Aber selbst bei �bereinstimmenden Typen t�ten dich semantische Unterschiede. Eine sortiert aufsteigend, eine absteigend. Eine rundet halbe Werte auf, eine rundet halbe Werte auf gerade Zahlen. Der Voter sieht drei verschiedene Antworten und hat keine prinzipielle M�glichkeit zu w�hlen.

Die Literatur zu n-version programming ist voll von Studien, die zeigen, dass unabh�ngig geschriebene Programme oft auf korrelierte Weise fehlschlagen. Programmierer machen dieselben Fehler. Sie lesen dieselben mehrdeutigen Spezifikationen falsch. Wenn deine Spezifikation �sortiere diese Liste� lautet und ein Programmierer Quicksort implementiert, w�hrend ein anderer Mergesort implementiert, k�nntest du annehmen, dass sie �quivalent sind. Das sind sie, bis du nach Stabilit�t fragst. Oder bis der Input NaN enth�lt.

Die meisten Teams �berspringen �quivalenzpr�fungen, weil es sich wie Zusatzarbeit anf�hlt. Das ist es nicht. Es ist die Arbeit, die den Rest des Systems sinnvoll macht.

Warum deine Test-Suite dir falsche Sicherheit gibt

Du schreibst Unit Tests. Beide Funktionen bestehen. Du rufst Sieg aus.

Das ist ein Kategoriefehler. Tests k�nnen die Anwesenheit von Bugs beweisen, niemals ihre Abwesenheit. Bei unendlichen Input-R�umen, oder selbst nur gro�en endlichen, ist deine Test Coverage ein Rundungsfehler. Zwei Funktionen k�nnen bei jedem von dir bedachten Fall �bereinstimmen und bei dem einen abweichen, der um 3 Uhr morgens in Produktion wichtig ist.

Das habe ich auf die harte Tour bei einem Projekt mit zwei JSON-Parsers gelernt. Einer verwendete Pythons eingebautes json.loads, der andere einen handgeschriebenen Parser f�r Performance. Unsere Test-Suite hatte f�nfzig F�lle. Beide bestanden. In Produktion schickte ein Kunde ein JSON-Objekt mit einem doppelten Key. Pythons Parser behielt den letzten Wert. Unser handgeschriebener Parser behielt den ersten. Der Voter sah zwei verschiedene Objekte und panikte.

Property-based testing kommt n�her. Statt Inputs von Hand auszuw�hlen, beschreibst du die Properties, die beide Funktionen erf�llen m�ssen, und l�sst einen Generator nach Gegenbeispielen suchen. Hier ist ein echtes Beispiel mit Pythons Hypothesis-Bibliothek:

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

F�hre das aus und Hypothesis findet schnell ein Gegenbeispiel. round_half_up(2.5) gibt 3 zur�ck. Pythons eingebautes round(2.5) gibt 2 zur�ck, weil es banker’s rounding verwendet, das auf die n�chste gerade Zahl rundet. Beide Funktionen sind nach irgendeinem Standard �korrekt�. Sie sind nicht �quivalent.

Property-based testing wird �quivalenz nicht beweisen. Es findet die Edge Cases, die deine Unit Tests verpasst haben. Das ist wertvoll, aber es ist immer noch Falsifikation, keine Verification.

Wie SMT solver tats�chlich �quivalenz beweisen k�nnen

Wenn du einen Beweis willst, musst du die Komfortzone des Testens verlassen und in die Welt der SMT solver eintreten. Die Idee ist geradlinig. Kodiere beide Funktionen als logische Formeln und frage den Solver, ob ein Input existiert, bei dem sie abweichen.

F�r bounded domains ist das mechanisch. Hier ist ein Beispiel mit Z3, um zu beweisen, dass zwei Integer-max-Implementierungen �quivalent sind:

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 gibt unsat zur�ck, was bedeutet, dass kein Gegenbeispiel existiert. Die Funktionen sind f�r alle Integers in Z3s Modell �quivalent. Das ist ein echter Beweis, begrenzt auf die Theorie, �ber die Z3 reasoned.

Das kannst du auch f�r komplexere Funktionen machen. Der Trick besteht darin, deine Funktionen als logische Formeln auszudr�cken. F�r Loops unrollst du sie. F�r Arrays verwendest du Z3s Array Theory. F�r Floating Point verwendest du Z3s FP Theory und akzeptierst, dass der Solver bei komplexen Ausdr�cken time outen k�nnte.

Die L�cke zwischen �mechanisch� und �einfach� ist der Punkt, an dem die meisten Teams steckenbleiben. Das �bersetzen einer Python-Funktion in Z3s Sprache erfordert, beides zu verstehen. Aber sobald du die �bersetzung hast, erledigt der Solver die harte Arbeit.

Die Trade-off-Tabelle, die niemand ver�ffentlichen will

Volle Formal Verification, die �quivalenz f�r alle m�glichen Inputs einschlie�lich jedes IEEE 754 Edge Case beweist, ist m�glich. Menschen machen das f�r kryptographische Primitive und Avionik-Systeme. Es kostet Wochen oder Monate Expertenzeit und erfordert Tools wie Coq oder Isabelle.

Property-based testing kostet Minuten und f�ngt echte Bugs ab, bietet aber keine Garantien.

Bounded Verification mit SMT solvern liegt dazwischen. Es gibt dir eine Garantie f�r einen klar definierten Scope. Dieser Scope k�nnte 99,9 % deiner Produktions-Inputs abdecken. Ob das gut genug ist, h�ngt davon ab, was ein Fehlschlag kostet.

Es gibt kein kostenloses Mittagessen. W�hle das Tool, das zu deiner Risikobereitschaft und dem Know-how deines Teams passt.

Ein Voter, der wei�, wann er aufgeben soll

Die meisten n-version-Systeme implementieren einen naiven Majority Voter: gib das h�ufigste Ergebnis zur�ck oder fail, wenn es keine Mehrheit gibt. Ein besserer Voter kennt seine eigene Unwissenheit.

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

Wenn der Voter bei bestimmten Input-Klassen anhaltende Uneinigkeit sieht, ist das ein Signal. Entweder ist deine �quivalenz-Annahme falsch, oder du hast einen Bug in einer Implementierung gefunden. Beides ist es wert, gewusst zu werden.

Der Voter ist nicht nur dazu da, Gewinner zu w�hlen. Er ist dazu da, dir zu sagen, wann deine Annahmen �ber �quivalenz falsch waren.

Was du als N�chstes wirklich tun solltest

Beginne mit property-based testing. Es ist g�nstig, es findet Bugs, und es zwingt dich dazu, zu artikulieren, was ��quivalenz� in deiner Domain bedeutet. Sind es bitwise identische Outputs? Outputs innerhalb eines Epsilon? Outputs, die dieselbe Postcondition erf�llen?

Sobald du �quivalenz pr�zise definiert hast, wechsle zu bounded verification, wenn die Domain endlich ist und die Eins�tze hoch sind. Verwende Z3, CBMC oder ein �hnliches Tool, um einen mechanischen Beweis f�r deinen bounded scope zu erhalten.

Reserviere volle Formal Verification f�r die Teile, in denen ein Bug buchst�blich Menschen t�tet. F�r alles andere: Kenne die Grenzen deines Beweises und �berwache Uneinigkeit in Produktion. Das beste n-version-System ist eines, das wei�, was es nicht wei�.