Skip to main content
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.
Like the rest of this section, this walkthrough is human-facing: what was measured, what came back, and what a person decided. The exact calls an agent makes at each step are not restated here — they belong to the API reference for agents in the Genesis repository under 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 a wwi_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.
Why a row count is not enough. An earlier migration in this same package reported zero failures with all 14 row counts matching exactly — while having silently changed a customer-tier threshold from >= 500000 to > 100000. No row count and no schema diff can see that.

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 fifth bucket is the one people miss: downstream digests that cannot match while a column digest is still unresolved. They are not independent findings; they clear when their cause clears. Fewer than half of the original 477 were defects in 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 on Dimension.City, and all three trace to the same geography column:
  • the boundary values of the Dimension.City.City column,
  • 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.
Confirm the count actually dropped. Both routes currently accept a stale population hash and still return a success response, while the read side ignores the approval. This is a known open defect. Check that the unresolved count moved rather than trusting the success response.

The review decision

The run was recorded as approved_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.
Who signed this one, stated honestly. Both the exception writes and the decision write on this run were accepted under the instance’s service identity and are journaled against the local reviewer identity — not against a person. A Genesis fix requiring a genuine human login on those two routes was in flight at the time of the run, and a human re-record was pending. Anyone reproducing this should drive the last step from the Prover interface while signed in, so the decision carries their own name. Roles and approvals explains why the local attribution is deliberately self-describing.

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, against dbo.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.
Deploy note carried from the run. Use the exact 40-hex commit that git rev-parse resolves, and confirm the registry tag exists before setting the image. A hand-completed commit took the instance down for 12 minutes.

Acceptance of record

The spec agent’s acceptance-of-record re-run has now happened, on main 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.
The classifier tripped zero times across the three tickets, and nothing was refused by name. The first of the three caveats above no longer bites: the three-part column loci that cost a finalize round the first time were accepted first time on this run, and finding 34 is closed.
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.
For agents and integrators. The exact calls, request shapes and refusals behind every step above live with the code, in the Genesis repository under docs/prover/. This page is the account of one run and deliberately does not restate them.