Skip to content

Differential Equivalence Test

Cross-implementation equivalence audit — instantiates Specification-to-Execution Lowering

Feeds the same inputs through two implementations and flags any divergence, establishing that a new or lowered version behaves like a trusted reference — without needing a full specification of the correct output.

A Differential Equivalence Test answers a narrower question than "is this correct?": it asks "does this behave the same as that?" It runs identical inputs through two implementations — typically a new or optimized version against a trusted reference — and treats any observable divergence as a defect to localize. Its defining strength is that it needs no full specification of the right answer: where a spec-based test must state what each output should be, a differential test needs only a reference already trusted and a criterion for when two outputs count as the same. That makes it the workhorse for validating a lowering when writing down correct behavior for every input is infeasible but a slower, simpler, or older implementation exists to compare against.

Example

A team replaces a math library's exp() with a faster polynomial approximation. No one can write down the "correct" bits for every one of the 2⁶⁴ possible inputs — but the existing, trusted exp() is right enough to be the reference. The differential test generates millions of inputs (uniformly, plus dense sampling near zero, at overflow edges, and among denormals) and runs both implementations on each, comparing results under an explicit correspondence criterion: agreement to within one unit in the last place, not bit-for-bit, because an approximation is allowed to differ slightly but not meaningfully.

Most inputs agree; a cluster near a polynomial-segment boundary exceeds the tolerance, revealing a coefficient error in one segment. The test never knew the true value of exp(x) for any input — it only knew the two implementations must correspond, and where they didn't, it pointed. It then minimizes the failing region to the smallest triggering input, handing the team a reproducible defect rather than "they disagree somewhere."

How it works

  • Two implementations, one input stream. The version under test and a trusted reference run on identical inputs — generated, fuzzed, or replayed from production traffic.
  • A correspondence criterion, not a spec. Equivalence is defined explicitly: bit-exact, within-tolerance, or observationally equal up to some projection. Divergence beyond the criterion is a finding.
  • Localize the divergence. A mismatch is shrunk to the smallest input that triggers it, turning "they differ" into a reproducible defect.
  • Report the strength, not just the verdict. The result is only as strong as the inputs exercised, so the test characterizes how much of the behavior space agreement was shown over.

Tuning parameters

  • Correspondence criterion — the definition of "same": bit-exact, numeric tolerance, or observational equivalence up to reordering. Loose criteria admit benign differences but can hide real ones; tight criteria catch everything, including differences that don't matter.
  • Input generation strategy — uniform random, coverage-guided fuzzing, or replayed real traffic. Each probes a different region; the strategy decides which divergences you are able to find at all.
  • Volume and budget — how many comparisons to run. More inputs strengthen the assurance but cost compute; the dial trades confidence against time.
  • Reference choice — which implementation is trusted as the oracle (a prior version, an Executable-Specification Interpreter, a Reference Implementation). A stronger, more independent reference makes agreement mean more.
  • Divergence handling — whether the first mismatch halts the run or the test catalogues all divergence classes, trading fast failure against a fuller picture.

When it helps, and when it misleads

Its strength is validating a lowering without anyone having to write the spec of correct output — invaluable when behavior is intricate but a trustworthy comparison target exists. It is how optimized, ported, or regenerated implementations are held to a reference at scale, and it localizes any drift to a minimal failing case.

Its central trap is that agreement is not correctness. Two implementations can share a common ancestor, a library, or the same misreading of the spec and agree on the same wrong answer — a correlated failure the test is blind to by construction.[1] It also only ever demonstrates equivalence over the inputs it happened to run, so a clean result is bounded by the input strategy, not a proof over all inputs. And a mis-set criterion either drowns real divergence in tolerated noise or flags cosmetic differences as defects. The discipline is to make the reference genuinely independent where the stakes justify it, to state the correspondence criterion explicitly rather than defaulting to bit-exact, and to report agreement as evidence over the tested domain, never as universal equivalence.

How it implements the components

Differential Equivalence Test fills the two components that define and grade a comparison, not the ones that produce an artifact:

  • correspondence_criterion — it makes explicit what "behaves the same" means (bit-exact, within-tolerance, observational), the rule by which any two outputs are judged equivalent or divergent.
  • assurance_strength_profile — its verdict carries a strength: equivalence shown over these inputs to this criterion — an empirical, coverage-bounded guarantee rather than a proof.

It produces no reference of its own — it consumes one (reference_model_or_oracle, from a Reference Implementation or Executable-Specification Interpreter) — and it proves no property over all inputs (proof_and_test_obligation_set, domain_of_validity_statement — a Model Checker and Static Analyzer); it adjudicates sameness against a trusted twin.

References

[1] Differential testing — running the same inputs through independent implementations and investigating any output difference — is a standard way to find bugs without an oracle for the correct output. Its known blind spot is correlated failure: implementations that share code or assumptions can agree on the same error, so agreement is only as strong as the reference's independence. ↩