Building an Independent Verification Oracle

Here is a defect I found in my own work, and it is the reason this article exists.

A pipeline parsed structured documents and reported how much of each document it had successfully captured — a completeness percentage. A verification gate then checked that percentage. The gate computed the denominator by calling a module to count the structural elements in the source. That module was the same one the parser used to walk the document.

So when the parser missed a whole category of element, the counter missed it too. Numerator and denominator both shrank. The gate reported one hundred percent, correctly, against a total that was itself wrong. Parser, gate and contract were wrong together, and nothing in the pipeline could see it.

What independence actually requires

"Write a second implementation" is the easy part. The hard part is being specific about what must not be shared, because sharing sneaks in through the parts nobody thinks of as logic.

Four axes, and all four matter:

1. No shared application code. Not one import. Not a constants module, not a "small helper", not the schema definitions.
2. A different library. If both sides use the same parser library, a bug in that library is common to both.
3. A different traversal model. Same library, different approach still leaves you sharing the library's model of the document. Full-tree materialisation and streaming events fail differently.
4. Different text assembly. How character data is gathered — including what happens to text between and after child elements — is a classic source of quiet disagreement, and it is worth having the two sides do it differently on purpose.

In the system above, production used the standard library's tree parser with a hardened loader and a full-tree walk. The oracle uses a different library entirely, in streaming mode, with an explicit tag stack, accumulating character data from each element's own text and its trailing text separately. Its complete import list is three standard-library modules plus that one parser. Zero application imports.

That is a stronger independence argument than "the oracle uses the standard library", which is what an earlier draft of my own documentation claimed. Different library, different traversal model, different text assembly, zero shared code — each clause is doing work.

A worked shape

The oracle's job is narrow. It produces an inventory of the source, and nothing else. It does not know what the production schema looks like, it does not know what correct means, and it never writes.

from dataclasses import dataclass, field
from lxml import etree  # deliberately not the library production uses


@dataclass
class Inventory:
    """A structural census of one document. No interpretation, no judgement."""
    element_counts: dict[str, int] = field(default_factory=dict)
    text_length: int = 0
    paths: set[str] = field(default_factory=set)


def take_inventory(path: str) -> Inventory:
    inv = Inventory()
    stack: list[str] = []
    for event, element in etree.iterparse(path, events=("start", "end")):
        if event == "start":
            stack.append(element.tag)
            inv.element_counts[element.tag] = inv.element_counts.get(element.tag, 0) + 1
            inv.paths.add("/".join(stack))
        else:
            # Own text and trailing text, gathered separately and on purpose.
            inv.text_length += len(element.text or "") + len(element.tail or "")
            stack.pop()
            element.clear()
    return inv

The gate then compares production's stored structure against this inventory. Because the inventory was produced without any production code, a defect in production cannot hide inside the number it is measured against.

Prove the prover first

An independent oracle still has to earn the right to issue a verdict. The mechanism I use is a self-proof that runs before any new claim:

Before certifying anything, re-derive every already-certified record under today's rules. If any of them no longer reproduces, issue no verdict at all — including for the record being certified.

def prove_baseline(certified: list[Record]) -> None:
    failures = [r.key for r in certified if take_inventory(r.source_path) != r.recorded_inventory]
    if failures:
        raise BaselineBroken(
            f"the prover has not proven itself; no verdict issued ({len(failures)} regressions)"
        )

The refusal is the point. The tempting behaviour is to report the regressions as warnings and carry on certifying, and that is precisely the behaviour that lets a rule change quietly invalidate a back catalogue while the pipeline keeps stamping new approvals.

Test the oracle against a second subject

The defect that started this article was real, and unit tests did not find it. What found it was running the gate against a second document.

The first document happened to carry exactly one piece of source evidence. The gate's query pooled evidence documents without grouping, so with one document it was accidentally correct. The second document carried three — one current and two superseded — and every finding was suddenly multiplied by three. The bug was in the gate, not the data, and only a second subject with a different shape could expose it.

The general rule is worth stating plainly: a verification component tested against one instance is tested against that instance's accidents. Choose the second subject for a structural difference, not for coverage.

Where independence cannot be total

State the boundary, because "all our tooling is independent" is almost always false.

In the same toolset there are roughly four dozen operational tools, and at least one deliberately imports the production parser — it is a differential that runs both implementations over the same input and reports where they disagree. That tool is not independent and is not meant to be; its whole purpose requires both sides.

So the claim is narrow and checkable: the oracle imports no application code. That is a property you can assert in a test.

def test_oracle_has_no_application_imports():
    tree = ast.parse(Path("tools/oracle.py").read_text())
    imported = {
        node.module.split(".")[0]
        for node in ast.walk(tree)
        if isinstance(node, ast.ImportFrom) and node.module
    }
    assert imported <= {"io", "re", "dataclasses", "lxml"}

An independence claim that no test enforces decays within a release or two, because the shortest path to fixing an oracle bug is always to import the thing that already solves it.

When this is worth the cost

A second implementation is expensive. It is worth it when:

• the output is used as evidence rather than as a convenience,
• a wrong answer is quiet — nothing crashes, the number just reads well,
• the cost of being confidently wrong is higher than the cost of the second implementation.

It is not worth it for most business logic, where failures are loud and cheap. It was worth it here because a corpus that has drifted from its source produces confident citations of text the publisher no longer serves, and nobody downstream can tell.

Related

Equal counts do not prove two stores agree sets out the ladder of comparisons this oracle supplies the denominator for. Knight and Leveson's experiment on multiversion programming is the honest counterweight to all of this: independently written implementations still correlate their failures more than the theory predicts, which is an argument for choosing different libraries and models rather than merely different authors.