Verifying code
that has no reference

Everything so far leaned on a comfortable fact: there was an original. A package to re-derive, a legacy module to run. The oracle came from executing something that already worked. Pull that away — you're writing code that has never existed — and the obvious question is whether any of this still applies. If there's nothing to compare against, what does "verified" even mean?

It still applies. You just have to be honest about where truth comes from — and it turns out there are only a few places it can come from.

Truth source #1: properties

Most code that has no reference still has invariants — statements that must hold for every input, even though you can't enumerate the outputs. You don't need to know what serialize(x) returns to know that parse(serialize(x)) must equal x. That's a property oracle, and the classic families cover a startling amount of real code:

• — Round-trip — decode(encode(x)) == x. Serializers, codecs, compressors.
• — Idempotence — f(f(x)) == f(x). Normalizers, sanitizers, formatters.
• — Invariance — sorting preserves the multiset; a transform preserves a checksum; a rebalance preserves the total. Conservation laws.
• — Oracle-by-agreement — a slow, obviously-correct reference matches a fast, clever implementation on random inputs. The tortoise checks the hare.

Generate thousands of inputs, assert the property on each. This verifies correctness-of-contract rather than identity to a reference — a different, weaker, but completely real guarantee, and often exactly the one you want for new code.

Truth source #2: named sub-problems

Here's the move that does the heavy lifting. Most "novel" code isn't novel all the way down. A brand-new feature decomposes into pieces, and the pieces have names — names that appear in algorithm literature, RFCs, or standard library APIs. gcd. levenshtein. sha256_pad_message. parse_query_string.

This is why decomposition quality matters so much. gcd is a good leaf — it has an oracle. helper_that_does_three_vague_things is a bad leaf — it has none. Decompose until every leaf has a name, and you've turned "verify novel code" into "verify a handful of well-understood pieces plus their wiring."

Truth source #3: a human, once

Some things are genuine judgment calls — a business rule, a product decision, a "this is what we mean by valid." No property or reference settles them; a person has to. The discipline is to capture that ruling once, as a frozen vector, at the moment the human decides — and then never let a model re-litigate it. The human is the oracle for exactly the irreducible decisions, and their ruling is held out like any other. What you must never do is let the code's author also be the judge of whether the code is right; that's the rubber stamp the whole system exists to prevent.

The honest ranking

These aren't equal. Identity to a running original (brownfield) is the strongest. A published spec or reference is next. A property is real but partial — it constrains behavior without pinning it. A frozen human ruling is only as good as the human. The skill isn't pretending new code is as verifiable as old code; it's knowing which truth source you're standing on, and saying so. A verification that quietly downgrades from "matches the reference" to "seems plausible" is worse than none, because it lies about its own strength.

rederive makes you name the source. That's the point.