One real migration, walked end to end. Every number on this page was
measured on the run described here, not projected from what the product is
meant to do. The run finished with 1,290 elements matched, 243 differences
licensed, 3 elements the Prover declined to measure and that were approved as
exceptions, and nothing left open, over a recorded review decision of
approved with exceptions.
docs/prover/.
For the concepts these steps exercise, read
Overview first. For what a run is and how to watch
one, read How a run works. For who may do
each step, read
Roles and approvals.
Scenario
WideWorldImporters is Microsoft’s sample retail company: an operational SQL Server database of 48 tables and 4,713,833 rows, and a 14 table data warehouse that is rebuilt from it every night by 29 T-SQL stored procedures. In this run the warehouse was moved to Databricks. The Genesis agent Eve rebuilt all 14 warehouse tables as PySpark notebooks, working from a ticket and the legacy SQL rather than from a translation of it, while the operational source was transported as-is into awwi_bronze layer so the rebuilt warehouse had the same raw inputs to
read.
What the reviewer needed at the end was not a green light from a row count. It was
proof that the rebuilt warehouse holds the same data as the original, table by table
and column by column, with every remaining difference either licensed as a known
platform difference between SQL Server and Databricks or approved as an exception
by a named person.
That is the bar. This run cleared it on the measurement — and not on the
signature: the exceptions and the decision were accepted under the instance’s
service identity and journaled against a local reviewer identity, with a human
re-record still pending. The review decision sets out exactly
what that means and what a reproducer should do differently.
Register and characterize both sides
Register both estates
The step. Each side is registered once, under a name, a role, a dialect, a
database and a schema list. The source was registered as WWI DW — SQL Server
(source of truth) against the
mssql.wwi_dw connection, over the Dimension
and Fact schemas; the target the same shape against the Databricks catalog on
databricks.wwi_gold. No credentials appear anywhere in the registration —
the connection is referenced by name.What came back. Two estate ids, which are the pair everything later hangs
off: estate_44f6e19f936d4f56a1e5aa61b699121d (source) and
estate_fa46e5c1a4974e66841dec59effc8812 (target).What we decided. The pair is the unit. A comparison is between two
characterizations of these two estates — not between two live databases.Characterize the source, with the provenance assertion
The step. The source scan carried one provenance assertion: that the
Lineage Key column on 13 tables — Dimension.City, Customer, Employee,
Payment Method, Stock Item, Supplier and Transaction Type, and
Fact.Movement, Order, Purchase, Sale, Stock Holding and Transaction —
copies an engine-issued value from Integration.Lineage.There is no author field in the assertion, and that is deliberate: Genesis
mints the asserter and the timestamp from the authenticated caller, so nobody can
assert on another person’s behalf by putting their name in a payload.What came back. The assertion is verified against the catalog when it is
used, so it cannot manufacture provenance the database denies. It is also part of
the source boundary, so adding it changes the pair fingerprint.What we decided. Assert first, then scan, then bind, then compare. The
Lineage Key columns hold values issued by a sequence on Integration.Lineage,
but no foreign key declares that relationship, so nothing mechanical can reach
them and a name-pattern route is refused by design. A named person is the only
route.Characterize the target
The step. The same measurement against the Databricks side, in the target
role.What came back. Preflight reported the estate “not ready” on two counts:
no ETL code assets attached, and no clone adapter for SQL Server.What we decided. Proceed. Both of those concern the behavioural stimulus
path, not the characterize-and-compare path this run needed. Read which light
failed before acting on a not-ready preflight.
Compare
The step. The comparison takes the two snapshots plus the vocabulary needed to line the two engines up: an explicit case-insensitive object-name policy, a schema map (Dimension to dimension, Fact to fact), and an object map for the four tables whose names
contain spaces — Dimension.Payment Method, Dimension.Stock Item,
Dimension.Transaction Type and Fact.Stock Holding. Both estates were declared
quiescent, with a note recording that no writers were active.
What came back. Omitting those maps produced eight spurious object-level
findings in one run, because Databricks lowercases identifiers and the four spaced
names were renamed.
What we decided. Always send both maps. And re-run the comparison after every
binding change, because a comparison consumes only the bindings that existed when
it ran.
From 477 open findings to none
The first comparison, with nothing licensed, left 477 open findings. Getting to zero was not one act; it was nine, and only some of them were fixes to the migration. Read every “open after” figure below as a count read off a comparison that ran after that step. Neither a binding nor a fix moves a number that already exists — the re-run is what moves it. That is the same rule as Bindings do not rewrite a run that already happened, and it applies to every row.The intermediate values 77, 71 and 65 are measured endpoints of a session in
which four steps landed together. Which step produced which drop was not recorded,
and is deliberately not attributed here rather than guessed at.
Group findings by cause, not by table
The single most useful move on this run was sorting the 477 into five buckets by what caused them:Platform shape
Differences the two engines cause rather than the implementers. License
these.
Instrument defects
The Prover measured it wrong. Fix these — never license them, or the check
goes blind.
Out of scope by design
Not part of what this transition undertook to reproduce.
Genuine build defects
The delivered warehouse is wrong. Fix the migration.
The thirteen rules, and why two needed a ceremony
Correspondence rules are how platform variance gets licensed. 13 rules were bound on this pair:
The two ceremony-tier rules were R14 (engine-issued surrogate keys renumber on
rebuild) and R10 (text distinct-count under collation). They sit at that tier
because they license value-derived comparisons, which is a heavier thing to accept
than a difference in type spelling.
The pack for SQL Server to Databricks covers type spelling, unbounded text types,
integer and float widening, value rendering, unenforced key constraints, and
collation effects on distinct counts. The comparison’s own pack-consent read listed
the pack’s eleven rules:
R15 arrived by upgrade and was bound last — which is a story of its own, and it
is the second item under What to expect.
Rulings and abstentions
The last comparison left nothing open and three indeterminate elements. All three were onDimension.City, and all three trace to the same geography column:
- the boundary values of the
Dimension.City.Citycolumn, - the whole-table content digest on
Dimension.City, - the column digest on
Dimension.City.Location.
An indeterminate element is an abstention, not a finding. The Prover is
declaring that it could not measure, rather than guessing. No licence closes an
abstention — a person approves it as an exception, bound to the run and to the
population it was measured on.
Three abstentions, two packages
The three came back as two packages, not three, because the engine stamps two distinct cause codes:
Do not assume one object means one package. The grouping is by measured cause,
and the count is whatever the engine measured. Approving both packages took the
unresolved count to 0 and unlocked “Approve this run”.
Which route you get depends on your build, and this run predates the newer one.
Approving abstentions as packages — one signature per measured cause — is
available from Genesis commit
874f37c2ef onward. Before that, the fallback is
the per-finding route, once per abstention. That is the route this run used:
the same three abstentions were cleared one at a time, which is what took this run’s
unresolved count to zero and made the review decision recordable. The two-package
grouping above is what the engine returns for these same three elements on a build
carrying that commit.The review decision
The run was recorded asapproved_with_exceptions on run
ecrun_bd4c0f2ea92141aebaa113a0a1e8ce5e, over diff
56680664486b74c6ecbfe12452bcf45f37e83498eb0c98c549a823838d680d00.
The unresolved count must be zero before a decision can be recorded at all, which is
why the abstentions come first. And the relationship worth internalising runs the
other way from most dashboards: zero open findings only makes the decision
available to record. The tile turns green off the decision, never off the count.
Author and grade the specification
Everything above works with no specification attached. This run also exercised the other half: the spec agent authoring the Prover specification directly against the SQL Server source, reading the estate rather than a description of it. Three tickets were sealed on 2026-09-07:
Their sealed specification names are
wwi_mig_1a_dimension_date,
wwi_mig_1b_surrogate_keys and wwi_mig_1c_stock_holding.
Every asserted number was re-derived against the estate: 51 of 51 source-side SQL
statements clean, zero misbound loci, casing exact.
Two of the agent’s judgment calls are worth reading, because they are the kind of
thing a specification usually gets wrong quietly:
Reading an ambiguous 'excluded'
On the surrogate keys the author read the ticket’s “excluded” as values not
compared, columns still required — and backed that by measuring
WWI Invoice ID at 70,510 distinct over 228,265 Fact.Sale rows, against a
composite of 228,265.Settling a window function
On
Fact.Stock Holding it encoded the no-time-predicate
ORDER BY [Valid To] DESC resolution, put none of the sibling window
operators in any obligation, and proved the rival reading wrong across 227 of
227 rows.Three caveats measured on this run
Put a column in the column field
The naming gate refuses a locus that packs a column into
schema.table.column,
reading it as catalog-qualified. Use the separate column field. This cost a
finalize round.Retry a transient database drop before re-modelling
A dropped connection is reported as a specification defect, with wording that
reads like the specification is wrong. Retry before changing anything.
Alias every column in a measurement query
Unaliased duplicate result columns collapse silently to the first value, and
nothing warns you.
What to expect
Four things on this run surprised people who already understood the product. All four are the system working; none is a bug you can wait out.A provenance assertion changes the source boundary
The assertion rides on the source characterization, and adding it changes the pair fingerprint. That starts a new estate pair, and every rule binding must be redone on it by a person. Bindings cannot be inherited from yesterday’s pair. Order the work assert, scan, bind, compare, and you pay this once instead of twice.A new pack rule version is not offered until the pack is proposed again
A new rule version has no registry row on your pair until the pack is proposed again. Until then the Correspondence tab reads “Nothing is waiting for your sign-off” while the finding that rule would license stays open — and nothing in the interface hints that a rule exists but was never offered. This cost twenty minutes on this run. When an already-shipped rule’s definition changes, its earlier content ID remains recognized as shipped. An unratified copy under that earlier ID therefore remains identified as a platform default in unscoped rule worklists; the newly minted ID is a separate version and still needs to be proposed for your pair. Make it a reflex: after any Prover upgrade, ask what the pack ships against what your pair has been offered, and propose the pack if anything is unproposed. On this run, immediately after the upgrade that shipped the spatial rule, the reading was 11 shipped, 10 proposed, 1 unproposed.Bindings do not rewrite a run that already happened
Immediately after signing, the page showed 0 licenses and the same findings as before. Nothing is broken: a comparison consumes the bindings that existed when it ran. Re-run the comparison with the same inputs — and quote that diff hash, not the one you were looking at while you were signing.Proposals from another estate may appear on older builds, and refuse to bind
On builds predating the queue-hygiene fix, the Correspondence queue can show proposals drawn on objects that are not in your database. On this run four appeared, againstdbo.PRICING.IWGHT and dbo.CLOSE.IWGHT — objects belonging to an unrelated estate.
They refuse to bind, which is the right outcome. But they clutter the panel, and
approving one records your name against another project’s licensing. Check object
names before signing, and sign only what is tagged Platform default. The fix merged
and deployed on 2026-09-06, and the four are gone from this queue.
The artifacts you can cite
Every result on this page has an address. The deep links below are shown as paths against your own Genesis host; on this run they pointed at an internal lab instance and required sign-in. Treat them as a map of what to wire up.The builds these measurements were taken on
All of the above are superseded by current
main. They are stated as the builds
these measurements were taken on, not as versions to deploy.Acceptance of record
The spec agent’s acceptance-of-record re-run has now happened, onmain at
049189d10880547fb1520777672c9f530bfa22fb (genesis_version dev.049189d108). The
three tickets were run one after another, on a stack whose model was set by APP_CONFIG
alone — Bedrock, global.anthropic.claude-opus-5 — against the mssql.wwi_dw
connection registered in-process, under constitution constitution_v8_12.md
(sha256 73da08631eb1ae08bcea94c4858778b199d443ecdb5e831014dd187ac2c4a45a).
All three sealed. The numbers below are that run’s; the table under
Author and grade the specification records the
earlier pass, on the spec-agent builds 30970012e9 and 7d0e1b3414.
Each sealed specification has a hash, and the hash is what a later reader cites:
The one second round is the part worth reading. The surrogate-keys ticket’s first
finalize was refused on substance — the specification carried no membership
obligation at all. The author added
O25 through O30 and sealed on the second round.
That is the gate doing the job it exists for: a specification that measures nothing
about membership does not become a record just because it is well formed.
Two of the three wall times read straight. The third does not: about 29 of
Fact.Stock Holding’s 50 minutes were relay-drop backoff, not authoring.
What the run was read against
The readings were taken against a criterion pre-registered before the run, so the bar was not moved to fit what came back.The ambiguous 'excluded', read the same way again
The surrogate-keys ticket again read the ticket’s “excluded” as columns
required, values not compared, and measured 228,265 / 70,510 / 228,265 — the
Fact.Sale row count, the distinct WWI Invoice ID, and the composite. Its
invoice-line natural key is (WWI Invoice ID, Description), exactly unique.The window function, settled with plain equality
Fact.Stock Holding encoded ORDER BY [Valid To] DESC with plain equality and
an Unknown fallback of 0, and put no sibling window operator in any obligation
SQL.Every number re-derives
Every asserted number re-derived against the estate. The grader counts by
target_sql key, not by obligation, so its denominator is not the obligation
column above and is not meant to match it. It returned 13/0 on
Dimension.Date, 36/0 on the surrogate keys and 11/0 on
Fact.Stock Holding — nothing failed on any of the three.Loci bound, and bound at the right level
44 loci, zero misbound. Every one is schema-qualified and none is
database-qualified. Casing is exact.
Provenance complete
All three carry complete provenance: surface seat, bot
spec-author.Seen on this build, and not part of the acceptance. Transport drops (
08S01)
were returned to the author as specification defects (finding 40). Relation and
column names that need quoting are now rendered with the registered connection’s
dialect, so a name containing a space is no longer probed as two SQL identifiers.Next
- Overview — what the Prover measures and how its six components fit together.
- How a run works — statuses, provenance, and where to watch.
- Roles and approvals — what lands in front of you and what each button attests to.
docs/prover/.
This page is the account of one run and deliberately does not restate them.
