You built an n-version system. Three independent implementations of the same critical function, a voter that picks the majority result, and a warm feeling that you’ve outsmarted single points of failure.

You haven’t proven the functions are equivalent. You’ve just proven they compile.

Why equivalence is the hidden foundation of n-version programming

N-version programming is the idea that if one implementation has a bug, the others probably won’t, so a voter can discard outliers. This assumes the outputs are comparable.

If function A returns a float and function B returns a string, the voter has no ground to stand on. But even with matching types, semantic differences kill you. One sorts ascending, one sorts descending. One rounds half up, one rounds half to even. The voter sees three different answers and has no principled way to choose.

The literature on n-version programming is full of studies showing that independently written programs often fail in correlated ways. Programmers make the same mistakes. They misread the same ambiguous specifications. If your specification is “sort this list,” and one programmer implements quicksort while another implements mergesort, you might assume they’re equivalent. They are, until you ask about stability. Or until the input contains NaN.

Most teams skip equivalence checking because it feels like extra work. It isn’t. It’s the work that makes the rest of the system meaningful.

Why your test suite is giving you false confidence

You write unit tests. Both functions pass. You declare victory.

That’s a category error. Tests can prove the presence of bugs, never their absence. With infinite input spaces, or even just large finite ones, your test coverage is a rounding error. Two functions can agree on every case you thought of and diverge on the one that matters at 3 AM in production.

I learned this the hard way on a project with two JSON parsers. One used Python’s built-in json.loads, the other used a hand-rolled parser for performance. Our test suite had fifty cases. Both passed. In production, a customer sent a JSON object with a duplicate key. Python’s parser kept the last value. Our hand-rolled parser kept the first. The voter saw two different objects and panicked.

Property-based testing gets closer. Instead of hand-picking inputs, you describe the properties both functions must satisfy and let a generator hunt for counterexamples. Here’s a real example using Python’s Hypothesis library:

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

Run this and Hypothesis will quickly find a counterexample. round_half_up(2.5) returns 3. Python’s built-in round(2.5) returns 2 because it uses banker’s rounding, which rounds to the nearest even number. Both functions are “correct” by some standard. They are not equivalent.

Property-based testing won’t prove equivalence. It will find the edge cases your unit tests missed. That’s valuable, but it’s still falsification, not verification.

How SMT solvers can actually prove equivalence

If you want a proof, you need to leave the comfort zone of testing and enter the world of SMT solvers. The idea is straightforward. Encode both functions as logical formulas and ask the solver whether any input exists where they differ.

For bounded domains, this is mechanical. Here’s an example using Z3 to prove two integer max implementations are equivalent:

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 returns unsat, meaning no counterexample exists. The functions are equivalent for all integers in Z3’s model. That’s a real proof, bounded to the theory Z3 is reasoning about.

You can do this for more complex functions too. The trick is expressing your functions as logical formulas. For loops, you unroll them. For arrays, you use Z3’s array theory. For floating point, you use Z3’s FP theory and accept that the solver might time out on complex expressions.

The gap between “mechanical” and “easy” is where most teams get stuck. Translating a Python function into Z3’s language requires understanding both. But once you have the translation, the solver does the hard work.

The trade-off table nobody wants to publish

Full formal verification, proving equivalence for all possible inputs including every IEEE 754 edge case, is possible. People do it for cryptographic primitives and avionics systems. It costs weeks or months of expert time and requires tools like Coq or Isabelle.

Property-based testing costs minutes and catches real bugs, but offers no guarantees.

Bounded verification with SMT solvers sits in the middle. It gives you a guarantee for a well-defined scope. That scope might cover 99.9% of your production inputs. Whether that’s good enough depends on what failure costs.

There’s no free lunch. Pick the tool that matches your risk tolerance and your team’s expertise.

A voter that knows when to give up

Most n-version systems implement a naive majority voter: return the most common result, or fail if there’s no majority. A better voter knows its own ignorance.

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

When the voter sees persistent disagreement on specific input classes, that’s a signal. Either your equivalence assumption is wrong, or you’ve found a bug in one implementation. Both are worth knowing.

The voter isn’t just there to pick winners. It’s there to tell you when your assumptions about equivalence were wrong.

What to actually do next

Start with property-based testing. It’s cheap, it finds bugs, and it forces you to articulate what “equivalence” means for your domain. Is it bitwise identical outputs? Outputs within some epsilon? Outputs that satisfy the same postcondition?

Once you’ve defined equivalence precisely, move to bounded verification if the domain is finite and the stakes are high. Use Z3, CBMC, or a similar tool to get a mechanical proof for your bounded scope.

Reserve full formal verification for the parts where a bug literally kills people. For everything else, know the limits of your proof and monitor for disagreement in production. The best n-version system is one that knows what it doesn’t know.