Genesis Prover

Migrations, rebuilds and large refactors all end with the same question, and it is usually answered with a spreadsheet and a feeling: did we actually deliver what we said we would, and is anything else different that nobody meant to change? The Prover answers it as a measurement. It reads both databases first-hand, records what it found and how it was permitted to look, enumerates every difference between them, and then accounts for each one. A difference is accounted for by a rule a person ratified, a disclosed platform assumption, or a person deciding it. Nothing accounts for itself, and nothing is quietly dropped. The result is a signed verdict with its evidence attached — and it can be re-derived later, because every step records which build produced it, which rules it was judged under, and which database it actually read. Connection access and run provenance are separate; the estate API reference defines how direct estate calls preserve agent transport and audit identity while opening saved connections as the authenticated human, including endpoint-specific reuse rules. Characterization resume state follows that same exact resolved transport identity. The opaque identity scope includes the bot and authenticated user pair, so an interrupted scan can resume only its own staged measurement progress; another identity never sees or consumes those rows. For Databricks sources, Prover scan reads use an internal 64 MB response ceiling and bound eligible degeneracy probes at the source; see Databricks scan behavior. How agents drive the Prover covers that division in full — what an agent starts, what you see once it has, and where the agent-facing reference lives.

​

Readiness tells you what happened

Before characterization, estate preflight reports access, ETL understanding, and clonability as separate readiness lights. A raw estate may be marked source_only=true: because no Genesis transform produces its data, it has no ETL light and can be ready without code assets. If the ETL agent turn reaches its configured wall-clock budget, the light reports a timeout and points to the budget setting rather than treating the partial reply as a format error. The API reference covers the response fields and the Advanced Settings page lists the budget. Attaching code assets does not pin them: it records their locations until the agent calls clone_code_assets. When registration or an edit returns that verb in next, the agent must clone the git repositories or capture the Databricks revisions before characterization. For a SOURCE with no transform code, the response suggests declaring source_only=true; that declaration is explicit, not inferred from an empty asset list. See estate registration and code assets for the agent workflow and clone-fault recovery behavior.

​

The data-work proving skill

The optional prove-data-work skill is the end-to-end playbook for proving data built to a written definition: a migration, cutover, rebuild or replatform, a dbt build, a pipeline output, or a new gold, mart or reporting layer. It explains when to use the Prover instead of hand-written row counts, how to choose the cross-engine settings, and how to read a comparison into a punchlist without treating indeterminate or errored as a clean result. For a copy leg whose data already landed, register and characterize both whole estates before authoring one spec. Put each keep-but-don’t-count table in excluded_objects on every estate that contains it. Give row identity only as row_identity; write renames into the spec and pass them to the proof as schema_map, column_map, and object_map. Other requirements become clarifications; ask all questions before commissioning at most one repair round. If an exclusion arrives after sealing, update the full excluded_objects list on each estate that holds the table, then characterize both estates again. A proof counts as proved only when the review page reads Verified: the person has accepted every remaining item with a reason, nothing is left open, and a partially specified spec has no open clauses. The skill gives the full order. In a Genesis thread, activate it with manage_context(action='ADD_CONTEXT', active_skills='prove-data-work'). An external MCP caller can read it through genesis(action='read_skill', skill_name='prove-data-work', relative_path='SKILL.md'). SKILL.md holds the core rules and identifies the supplementary files to read when needed: the-path.md for running a step, reading-results.md for comparisons, grades.md for grade reports, approvals.md for requests, getting-the-verbs.md for MCP or HTTP calls, and relaying-to-people.md before relaying an answer or asking a person. In a Genesis thread, read a listed file with read_assigned_skill_file; an external MCP caller uses read_skill with the file path as relative_path. See Context Tools for the assigned-skill reader details. The skill is optional: the plan_estate_comparison plan and the Prover’s verbs work without it, and their responses identify the skill when it is useful. The two Prover skills were previously named prove-a-migration and plan-a-migration. Those names still load, as thin pointer skills that keep the migration trigger words and send the agent to prove-data-work and plan-data-work. The pointers carry none of the doctrine, so a thread or caller that uses an old name should load the new one.

​

The data-work planning skill

prove-data-work verifies one comparison. A migration or spec-driven build may need several comparisons in a required order, and the companion plan-data-work skill is the recipe book for working out which ones. It applies to migrations as well as builds such as a dbt model or reporting layer checked against a written definition. For layered work, it teaches the general source-layer, ETL and target-layer shape, the named shapes seen so far, and a method for deriving a recipe for a project that matches none of them. For each it gives the proof sequence, what must be declared before the first proof, and the rule that the deliverable is a durable pipeline on the target rather than hand-assembled copies. There is no separate planning agent: the same agent plans the sequence and then runs each proof through prove-data-work. The detailed recipes are written down once in the skill. Activate it the same way: manage_context(action='ADD_CONTEXT', active_skills='plan-data-work'), or genesis(action='read_skill', skill_name='plan-data-work', relative_path='SKILL.md') from outside. The data-work skills direct the agent to take its own next step in the same turn: repair its own spec defect and act on choices already covered by the sponsor’s standing rule, including whether to open an adjudication. Required readiness items and sealed-spec ratification still wait for the person. For a review decision without a standing rule, the person must ask for it or include it in a goal, Blueprint, or mission; an agent records which basis it acted under. Readiness withholds another conversation’s answers and documents by default; ask the person here, and set include_other_conversations=true only if they ask you to use that record. Confirm any answer from it before relying on or repeating it. See the readiness tool reference for the response details and how the pair’s latest proof can supply the migration shape when no sealed spec is named.

​

Data-fidelity checks in the skills

When planning or proving spec-driven data work, profile each source column for missing-value markers that its declared type does not reveal, such as '', '-', 'N/A', '-1', or text 'inf'. Record each discovered marker and its required target representation in the mapping before it is ratified; an unreconciled count is not explained until the rows causing the difference are found. Choose conversions from the measured source values rather than the declared type, and verify every cast: a successful conversion can produce a misleading value such as 0.0 or Infinity. The mapping must state which values convert and where every other value lands.

​

Fresh licensing evidence

Questions about a comparison’s licensing audit or audit trail, what licensed a difference, why the result should be trusted, or what a provenance label means must be answered from stored evidence, not earlier assistant prose. On every such turn, including repeats and follow-ups, activate prove-data-work with manage_context(action='ADD_CONTEXT', active_skills='prove-data-work'), then make a fresh read_comparison(diff_hash=…, include=["license_audit"]) call before answering. Use each raw provenance label exactly as returned; do not translate it into a friendly name or infer a rule explanation from it. The Prover toolkit reference covers the audit projection and its bounded evidence contract. When no Prover-page comparison context was supplied, the chat can use its own proof record only when the thread identifies exactly one distinct, successfully completed comparison. If there is no such comparison, more than one, or the record cannot be validated, the chat does not guess which audit to read. Supply valid Prover context from the relevant comparison to identify it explicitly.

​

The flow

Read it as one sentence: measure both sides, compare them, grade the specification against that comparison, settle what can be settled mechanically, and put the remainder in front of a person.

​

One proof, with or without a specification

A Prover proof is one thing, whether or not a specification is attached. The comparison always runs — the two estates are measured against each other and every difference is enumerated, specification or no specification. When a sealed specification is attached, the same proof also grades it. And whatever the specification did not explain still goes to review. That is the important guarantee. A specification narrows what a person has to decide by hand. It never shrinks what was measured, and it never closes a difference nobody licensed. For how the prove report handles a comparison that matched no objects before presenting the grade, see the prove tool reference. The agent-facing prove operation now provides that one trigger: it takes both characterization snapshots and an optional sealed specification, returning one proof run that owns the comparison and, when attached, the grade. Grading remains separately repeatable for a repaired specification against an existing comparison; that path does not re-measure the databases. Before any comparison exists, an obligation-only grade is also possible with tiers=["derivational"]; see the grade tool reference. Use prove when the first run should compare the estates and grade structural items as well. A succeeded, sealed spec_conformance grade can also be cited as server-checked project evidence through project_note. For a sealed-connection refusal, follow the proposed retry described in the grade tool reference. Databricks characterization connections support Service Principal (OAuth M2M) credentials for headless Prover scans and validations; see Databricks connection behavior for token refresh behavior during long-running validations. How agents drive the Prover

​

When a grade names a comparison made without its spec

A sealed specification that declares a target_model is graded over a comparison made under that model. This is the same comparison that prove(spec_hash=...) makes: the model licenses the declared target mappings and scope that the structural grade reads. If a caller uses compare and then calls grade with that comparison’s diff_hash, Genesis compares the pair again under the sealed model and grades the replacement comparison. The grade provenance records comparison_recomputed_under_spec, including the replaced diff_hash, the target_model_hash, and the spec that declared it. If that recomputation creates a new comparison, its listing title comes first from the grade run’s recorded title. Otherwise, it inherits the replaced comparison’s title unless that title was explicitly recorded under a different kind. A title recorded without a spec is not carried onto a spec-measured comparison; a title minted before title kinds were recorded is carried forward, preserving the name shown for that older comparison. The new comparison records an inherited title under the graded spec, so later re-grades can match that kind. When no eligible title exists, the recomputation has no business title and the card keeps its technical label. Consent-triggered re-runs preserve the original comparison’s title and its recorded spec kind. This keeps a title attached to the kind of comparison it names across re-grade and consent re-evaluation. The recomputation carries forward the original comparison’s caller-declared column_map, so renamed columns remain paired instead of appearing as missing and surplus. It also carries the comparison’s recorded row_identity_declared key and resolves it under the model as prove(spec_hash=..., row_identity=...) would. For a derived target, that means the key is resolved against the derived target’s driving input. If the key no longer pairs rows one-to-one under the model — for example, its target column is unavailable or its values repeat — the recomputation withholds that pair as indeterminate rather than guessing or refusing the whole grade. If the original comparison never recorded target terms for a key that paired no rows, those terms are not invented; the pair is withheld. Mapping an input onto a model-declared DERIVED target is not treated as row correspondence: the model builds that target from its declared inputs. This keeps compare-then-grade aligned with prove(spec_hash=...) instead of presenting the input rows under the derived target’s name. The grade reports the key and failure at comparison_recomputed_under_spec.row_identity.<object>.reason. That fallback is real warehouse work: both estates are read again, plus the model’s hub keys where applicable. If a pinned comparison’s basis says it paired rows on a caller- declared key but its record does not contain that key, recomputation still returns a conflict rather than silently dropping the declaration; prove the pair with the spec and row_identity together. A comparison already made under the sealed model, and grades without a model, keep their previous cost and behavior. Specs in one grade set must agree on one target model; conflicting models are refused before grading.

​

Move a finished comparison

A finished comparison can be handed to another Genesis server without rerunning the measurement. An agent exports the comparison bundle, and an agent on the receiving server validates and imports it; the receiving server keeps the original diff_hash and review decision, including the original reviewer and timestamp. This is a transfer of the measured result, not a second opinion from newly scanned databases. The bundle carries the rows needed to render the card and connection references, not warehouse data or credentials. If the receiving server already has an estate for the same database boundary, it matches at most one imported estate to each existing row, preferring an existing row whose id is already carried by the bundle. If no target row is available for an imported estate, Genesis writes it under its own id instead of sharing a row already matched to another estate; the transfer reports that outcome as a warning. Use the validation step before import when the target may already contain part of the comparison, and choose an explicit conflict mode when it does. The agent-facing export_comparison and import_comparison tools and the REST endpoints are documented in the tool reference, which also lists import validation refusals, and API reference. covers what that one trigger means for the person reading the result. Grading stays separately repeatable, and that is deliberate rather than duplication. When a specification is repaired — a clause corrected, an ambiguity settled, a missing obligation added — it is re-graded against the comparison that already exists, without characterizing the databases again. Re-reading two real warehouses in full is the expensive part; re-reading a corrected specification against a comparison already on disk is not. A grade’s obligation checks do still query the two live databases at the moment you ask, so a grade covering both halves describes two moments and reports which — see How a run works.

​

The six components

​

1. Estates and characterization

An estate is a database you have registered with the Prover, under a name and a scope — which catalogs, schemas and objects are in bounds. Characterizing it is the measurement: the Prover connects and reads the estate first-hand, in one session, recording as it goes. For estate registration semantics, including archived-name reuse and legacy duplicate scope cleanup, see the estate registration API reference. Two properties make a characterization evidence rather than a report:

• It enumerates with witnesses. Alongside the object list, the Prover records the principal it connected as, the exact catalog mechanism it used, what that principal could and could not see, and whether the enumeration was provably complete. An estate you were not permitted to read fully says so, rather than looking small. If the visibility witness itself cannot be read, the characterization records that witness as unavailable and continues measuring the objects already in scope. The Prover withholds the completeness claim unless a separate dialect-specific probe establishes it; a refused or failed witness is not treated as proof that the estate is empty or complete.
• It measures from a closed, versioned library. A fixed set of statistics — row counts, per-column counts, minima, maxima, distinct counts and maximum lengths, bounded top-value samples, and checksums over stable key ranges. Because the library is versioned, a snapshot is only ever compared against another taken under the same definitions. The current measurement library is estatechar.measure.v14; this version removes a view’s line comments before it stores the view’s text, so a comment can no longer hide the rest of the view from the logic it is checked against. Since v13, a SQLite column of a class that renders as the warehouses do (integer, text, UUID, boolean and float) is folded into the same checksum family as Databricks and Snowflake, so those columns’ values are compared across engines. A float compares as equal only inside the canonical window [1e-8, 1e15); outside it each engine keeps its own spelling, which can read as a false difference but never as a false match. A pre-v13 snapshot must not be compared with a v13 snapshot, so re-characterize both estates before comparing them. Other dialects retain their existing measurement bytes. For a SQLite NUMERIC or DECIMAL(p,s) column, the Prover can also compare its content digest with an integer or scale-0 decimal counterpart: SQLite reads both with its integer expression. This exception also applies to whole-table checksums only when every digest-bearing column is paired comparably. For cross-family comparisons, the exception does not cover a SQLite decimal paired with a float or fractional-scale column; those digest recipes remain indeterminate rather than being treated as a value difference. A column digest can also be compared across the SQLite and MD5-window families when either column is all NULL or has no rows, regardless of its declared type. This exception does not hide values on the other side: the digests still differ if that side contains values.

Databricks characterizations record tags:not_captured:databricks as an object-level exclusion because they do not read Unity Catalog tags. This covers both object and column tags: the exclusion means tags were not captured, not that the object has none. Palantir Foundry scans do not receive this exclusion because they do not use Unity Catalog. When a catalog does not report a column’s declared nullability, the Prover records the column-level exclusion nullability:not_captured:<dialect>; the declaration was not captured, so the comparison does not treat it as nullable or non-nullable. The result is content-addressed over the measurements and the instant they were taken at, so a snapshot names one reading unambiguously and two people can confirm they are looking at the same one. It also means scanning an estate that has not moved produces a new snapshot rather than reproducing the previous one: a reading is a reading, and the Prover never quietly hands back an older one in its place. Comparing two such readings is how you learn the estate did not move. The exception is a scan that was interrupted and relaunched: it continues the reading it had started rather than beginning a fresh one, reusing what it already measured and keeping that reading’s original instant. Characterization is not only about the data. Alongside the data pass, the Prover can measure an estate’s access surface (who is granted what), its consumption surface (the views and registered consumer queries that read from it, and whether they still return what they returned), and its logic surface (the models and tests a dbt project declares). Scanning covers the whole source estate by default: a scan is never silently narrowed to a subset, and every schema it drops is recorded with the reason it was dropped. The Prover uses the same qualified-name scheme for objects as the Digital Twin and Context Graph, so an object in a characterization lines up with the same object in the graph. palantir_foundry is supported as a source dialect. Foundry exposes Spark SQL over datasets but does not expose an INFORMATION_SCHEMA, so Genesis obtains the object, column, and completeness-witness rows through the connection’s catalog provider instead of issuing SQL catalog queries; the measurement pass still runs through Foundry’s SQL surface. A Foundry dataset is addressed as one backtick-quoted dataset RID or path, not as a three-part catalog.schema.table name. Foundry has no SQL time-travel form, so the characterization is disclosed with pin mechanism none; the dataset transaction RIDs observed during the scan are retained as watermark evidence. For the route-fallback counts and refusal details in a Foundry run’s terminal summary, including error terminals, see the characterize tool reference. Foundry characterization uses the elapsed budget in connectors.palantir_foundry_measurement_budget_seconds (default 3600 seconds, enabled by default). It starts before the scope and catalog walks. If it expires, completed measurements remain in the snapshot and any unfinished or remaining datasets are recorded as named indeterminate results with the budget reason; a named estate scan reports partial if a member is truncated. The budget is checked between reads, so it does not interrupt a Foundry read already in progress; that read remains subject to connectors.palantir_foundry_scan_timeout_seconds. Backend-owned Foundry characterization runs stay heartbeated while the scan is active.

​

Foundry SQL result caps

Foundry’s foundry-sql-server:preview role can return the first 1,000 rows as an ordinary successful result, with no indication that rows were cut off. The Prover refuses an unbounded SQL result containing exactly 1,000 rows as foundry_result_may_be_capped, rather than letting a possibly truncated read count as a match or a passing comparison. An outermost literal LIMIT of 1,000 or fewer rows is considered bounded and is not refused for this reason. When such a result is ambiguous, the connection runs SELECT id FROM range(1001) once for that scan or comparison. A result over 1,000 establishes that the connection can return more than the preview cap. A probe that returns 1,000 or fewer rows leaves the ambiguous read refused. If Foundry rejects the probe, the Prover instead checks each ambiguous read by counting that read’s statement up to its 1,001st row: exactly 1,000 accepts the read, while any other count or an unsuccessful count refuses it. A statement that cannot be counted soundly is refused without that count. The probe costs one Spark job on the Foundry tenant, only when an ambiguous result first occurs; after a rejected probe, each countable ambiguous read costs one extra Spark query. Because the read and count are separate queries, a change to the dataset between them can affect the result. Granting foundry-sql-server:read on the project removes the cap. These checks establish whether returned rows are capped; Palantir has not confirmed whether the preview role also caps rows scanned, which they do not establish.

​

Foundry catalog and declared keys

Foundry catalog enumeration also reads keys the platform declares: the dataset schema’s primaryKey on master, and primaryKey expectation checks on dataset outputs in the published sandboxes of Pipeline Builder pipelines found in the walked space. A pipeline check contributes a key only when its columns are plain column references and every named column exists on the dataset’s master schema. Genesis does not measure uniqueness or infer keys from column names; a key not declared by the source must be established through a ratified correspondence rule. The catalog scan reads each distinct Pipeline Builder pipeline’s sandbox listing and, when it has a published sandbox, reads that sandbox’s definition: up to two additional Foundry REST requests per distinct pipeline. These reads are skipped when no dataset is in scope. Draft checks are not treated as declarations, and pipelines outside the walked space are not read. If a declaration cannot be read or resolved against the dataset schema, or a relevant schema or pipeline definition cannot be read, the scan records that limitation rather than treating the key as absent. For each in-scope dataset, the scan also makes one Foundry job-spec request to record whether Foundry builds it and, when it does, the producer: a Pipeline Builder pipeline RID or jobspec:<rid>. If Foundry does not serve the job spec, the build status is unknown; the Prover does not infer that the dataset is either a source or a built output. The request adds one REST round trip per in-scope dataset, and rejected Foundry credentials still fail the scan. The measured object exposes this producer as built_by when one is identified; other dialects and datasets without readable producer evidence omit the field.

​

Foundry nested-column digests

When Foundry declares the complete shape, the Prover can compute content digests for ARRAY and STRUCT columns, including nested arrays and structs. It sorts the outer array’s elements for the digest and uses the struct’s declared field order. A bare or incompletely declared nested type has no digest. A MAP at any depth also has no digest because Foundry does not guarantee map-key order; the Prover withholds that content comparison rather than treating it as a match.

​

Foundry datasets without a schema

When Foundry reports that an in-scope dataset has no schema, the Prover reads its raw files through the Foundry files API instead of trying to measure it with Spark SQL. It pins the listing and every file read only to the branch’s head transaction when that transaction is COMMITTED. Checking the head and its status takes two Foundry requests; each is a single attempt with no retry or wait on Retry-After. The listing adds one request per 100 files, and each file adds one full-file transfer. If the head is an OPEN transaction (a write in progress), has no transaction, or its status is not confirmed as committed, the files remain unmeasured for that scan rather than being read from an in-progress write. The measurement is bounded to 1,000 files and 128 MiB total; an unreadable file, a file whose read disagrees with Foundry’s listed size, an empty dataset, or a dataset over either limit also remains unmeasured rather than being treated as a match. A later characterization can measure the files after a committed head is available. The source record stores each file’s path, byte length, and SHA-256 over its original bytes. On a Databricks target, the Prover compares that record with a table containing exactly the two string columns document and file_path; one full table scan computes the UTF-8 byte length and SHA-256 of each document, returning only paths and digests. No newline, whitespace, encoding, or Unicode normalization is applied. Equal file paths and bytes produce a match; a missing, extra, or changed file produces one file_content finding. If the target shape cannot be read, or either side could not be measured, or the target dialect cannot hash the landed documents on-engine, the comparison remains indeterminate. Recharacterize both estates to create these file-level measurements; earlier snapshots do not contain them. Because a file-backed dataset is still held and measured by the source scan, a spec cannot declare it new with add_table when the locus identifies that dataset or the latest target scan identifies its matching landing. finalize_spec refuses the item; see the spec-author tool reference for how to revise the draft.

​

2. Comparison — the system diff

A comparison takes two characterizations — normally the source system and the target it was migrated into — and enumerates every difference between them. This is the migration scenario: objects that moved, objects that were renamed, objects that were relocated into a different schema, columns whose types changed, values that no longer agree.

​

Rewritten views and behavior proofs

When a view’s definition differs on the target, which_proof_applies explains what this comparison read for it. A view written the same on both sides needs no behavior proof, though data findings on it still need resolving. For rewritten views, resolve data findings first: data_differs means differences remain, while data_explained_by_rule means a person must decide whether the rule-explained differences are acceptable. A behavior proof explains a rewrite only after the data matches. For a rewritten view with no data finding, needs_behavior_proof means this comparison read no passing proof for it. Check designed cases’ coverage claims with design_stimulus_campaign using check_claims_only=true; this checks without storing the cases. Then pass the cases to prepare_migration_prover, which stores them unapproved. Have a person approve them with request_test_case_approval, then run them with validate_migration. Prove the pair again and read the new comparison so it can include the passed proof. The prove-data-work skill supplies prover_tools and migration_prover_tools for this workflow; see the tool group reference. A proof recorded as behavior_proof_failed or behavior_proof_did_not_run is not a pass; read its behavior_proof_run_id with get_run to explain the outcome. If the kind is behavior_proof_passed_data_not_compared, fix the value coverage (for example by re-characterizing or declaring row identity), then prove again. behavior_proof_passed means this comparison read a passing proof; a proof that passed after this comparison was computed is not included. The complete field shape is in the [read_comparison reference] (/docs/Genbot-Toolkit/Additional-Tool-Groups#read_comparison). If a view cannot be tested because its source cannot be copied, copy access is unavailable, or its logic depends on the run time or session, explain why its rewrite cannot be proven by test cases. Do not call it proven or failed. which_proof_applies is explanatory only; it does not change the comparison verdict. When a view’s entry names a behavior proof run, its test_case_coverage lists which logic situations of the two views that run’s approved test cases covered, and which none covered. This is what the agent stated when it designed the test cases; running the proof does not check it. A claim made against another version of the view’s text is listed as not credited and does not count as covered. Prover assigns a case by its output_relation (schema and name); when that matches no view in the comparison, it falls back to the case’s dbt target_node model name only if exactly one view pair matches. Check not_credited for claims that identify no single situation and not_matched for coverage claims from cases assigned to neither view. The API reference describes the response fields and list limits. For value columns compared by row key, string and uuid values must match exactly even when a numeric tolerance is configured. Digit-only text such as 0012 does not match 12 through numeric conversion; identical values still match. For paired FLOAT / DOUBLE columns, a difference in the measured value digest or categorical distribution can trigger a live re-read on both sides. The Prover checks that each read still reproduces its snapshot digest, then compares the sorted non-null value multisets when each side has at most 2,000,000 values. Values match when abs(source - target) <= max(1e-12 * max(abs(source), abs(target)), 1e-300); NaN and infinity compare exactly. A tolerance-only result is licensed, never a silent match, under platform:float_relative_tolerance, and its reading reports the largest relative difference (plus the number of near-zero pairs decided by the absolute floor). If the live read cannot be verified, the sides have different counts, the value limit is exceeded, or any pair is outside the tolerance, the existing difference remains. FLOAT / DOUBLE boundary values use the same tolerance. The float tolerance does not apply to integers, DECIMAL / NUMERIC, text, dates, or timestamps; those classes keep their existing comparison rules. These additional reads happen during the comparison: each candidate object gets an aggregate digest check and each candidate column gets a full value read on both sides. Each side’s column is capped at 2,000,000 non-null values, and all live float and TIME value reads together are capped at 10,000,000 values per comparison. An unread float column remains a difference, and its detail says the tolerance was not checked and why; the run’s float_tolerance_read records each requested column, whether both sides were read, and each unread side’s cause and reason. Reads are bracketed by digest checks before and after the values are fetched, so a table that changes during the read is not used. Before the key-ordered float walk, the Prover can also use a tolerance digest as a skip gate. It runs only when both sides’ key uniqueness was probed, every compared pair is FLOAT / DOUBLE, both dialects support the digest, and each column declares a relative tolerance of at least 2e-14. The digest folds values to 15 significant digits; this minimum tolerance ensures that equal digests cannot hide a difference the walk would report. The gate issues one full-scan aggregate query per side. If the row counts and digests agree and no row contains a NaN or a finite value outside the digest’s canonicalization range, the Prover skips the paged key-ordered walk. Any difference, unreadable result, ineligible contract, or such value leaves the walk in place; the gate never changes a verdict. This can replace 666 page queries with two aggregate queries for a 1.66-million-row comparison at the default 5,000-row page size. When the gate runs, the comparison result’s tolerance_digest records its status and columns; declined explains an ineligible gate, and a skipped_walk result also records float_significant_digits: 15. Statuses are not_eligible, differs, unreadable, unfoldable_values, and skipped_walk. The [comparison tool reference] (/docs/Genbot-Toolkit/Additional-Tool-Groups#read_comparison) describes where to read the comparison result. A source TIME column stored as text on the target can be licensed under the seeded assumption time_as_canonical_text (platform:time_as_canonical_text), but only for a BigQuery source, whose TIME text preserves fractions. Databricks has no TIME type, so this can cover a source TIME to target text (STRING) type change. The comparison reads both sides’ non-null values live and licenses the column_type reading only when null counts agree, every target value is canonical HH:mm:ss text, and the target values match the source TIME renderings as a multiset. A malformed or different value, a dropped fraction, or a source dialect whose TIME rendering is not proven lossless leaves the difference unlicensed. Each side is capped at 2,000,000 values, with the shared 10,000,000-value comparison budget above. Live row and non-null counts are checked on both sides, and the target’s exact value digest is checked before and after the value read; a text column with no exact snapshot digest cannot be licensed. If either side cannot be read, the finding says the TIME values were not checked and why; the run records the requested columns and unread reasons under time_text_read. This proves the value multiset, not row-key equality. The comparison tool reference describes where to read the run disclosure. For an append_only comparison, the Prover distinguishes a duplicated load from rows appended between the two reads. When an exhaustive, unsampled reading has a native distinct count and no NULLs for an eligible single-column declared key, the Prover checks that key on both sides. If the side with more rows repeats key values, it records relied_on.basis: "duplicated_key_surplus" with the row and distinct counts, duplicate_rows, row_surplus, and accounts_for_surplus instead of attributing the difference to observation skew. For a row_count comparison, measured repeated rows are sufficient; for other comparison kinds, they must account for the whole row surplus. When the comparison can read the grown side, relied_on.sample_keys and the finding detail can name up to five repeated key values as text, capped at 200 characters each. A bounded, key-ordered query runs only for planned duplicated-load candidates; these examples are illustrative and never decide the finding. Missing, sampled, or otherwise ineligible key evidence remains indeterminate, and a failed sample read leaves the counts as the evidence. The Prover also rules out append skew when both readings have the same row count and the same measured maximum on the same append-only anchor column. It records relied_on.basis: "append_only_same_extent" with the anchor column, row_count, anchor_max, and skew_seconds. A value permutation within that unchanged extent therefore remains visible as drift even when the reads are seconds apart. This evidence is unavailable if either side lacks the anchor, row count, or measured maximum, if the anchor columns differ, or if the counts or maxima disagree; in those cases it does not rule out skew. For a mutable object with no mutation-stamp or change-stamp evidence, the finding detail states that this is an absence of evidence, not proof that the object was quiet. Do not present the missing stamp as proof that no change occurred. When a persisted change stamp and the earlier read time differ in timezone awareness, the Prover does not assign a zone to the timezone-less value: it proves the stamp was at or before the read only when it is at least 14 hours earlier, a margin that covers every real UTC offset. A stamp within that margin does not prove quietness, so the comparison continues to abstain. If the proof uses this margin, the decided element’s relied_on records offset_margin_hours: 14 and offset_margin_sides, which names what needed the margin (see below). When both timestamps have the same timezone awareness, they are compared directly. The same margin applies when a stamp shows movement. If a caller declares both estates static but a change stamp follows the earlier read by more than 14 hours despite a timezone-awareness mismatch, the declaration is refused and the comparison continues to abstain. A stamp inside that margin does not prove movement, so the declaration still decides. The refusal’s relied_on records the same two margin fields. A declaration’s timezone-less quiet_since covers a timezone-aware read only when it is at least 14 hours earlier. In every case offset_margin_sides names what needed the margin: source or target for that side’s change stamp (both can appear), or quiet_since for the declaration’s own instant. When Foundry verification supplies the translator’s lineage record for columns fed by an unseeded random function, their value, content, and count readings that remain unlicensed are indeterminate with cause non_reproducible_by_construction: the values are drawn afresh on both sides, so the reading is neither a difference nor a match. A person’s licence still takes precedence, and structural readings such as type or presence remain comparable. The comparison records relied_on.basis: "declared_lineage_record" and excludes those columns from the whole-table digest, which is decided over the other columns. This lineage input is documented in the Foundry migration tool guide. When missing and surplus column names differ only by case and separators (for example, flight_id and flightId), the comparison may add one leading, unlicensed addressing_incoherence finding when each name has exactly one candidate on the other side. Case-only differences are excluded because identifier folding already handles them; ambiguous candidates are not grouped. The finding is a text-only rename suggestion: each column still remains missing or surplus, and its content is not compared until the caller declares the pair in column_map. The result’s unwitnessed_by_identity disclosure counts unlicensed findings with no witness rows because no row identity was declared for their objects. Relay its sentence and declare row_identity to localize those findings rather than treating the absent witness rows as an evidence gap. See the API reference for repeat identity. Keyed verifier phases that need reads from both estates issue those reads concurrently. During localization, page fetches overlap when both streams need a page and the query budget covers the pair, reducing elapsed time for comparisons whose key streams advance in lockstep. For keyed specification checks, the engine can also infer a key’s family from the projection itself. A bare quoted literal is string, a bare integer literal is int, and a CASE expression is accepted when every THEN branch and its ELSE are literals of the same family; a CASE without ELSE, mixed families, non-literal branches, and other numeric literals state no family. A checksum projection that contains only key columns returns indeterminate_reason: "checksum_key_only": it verifies key membership, not content, and is attributed to the specification as written rather than treated as a clean content proof. For a SQL obligation, a non-empty compare_columns declaration limits the grade to those non-key value columns. Other columns returned by the query are context, not compared values. A declared column missing from a result is not silently replaced by a context column; the comparison errors. With no declared columns, every returned non-key column is compared. For an all-zero COUNT(*) - COUNT([DISTINCT] expression) check, the degeneracy probe also checks that the filtered query population contains rows, replacing the count expression with COUNT(*) while retaining the filter. A zero duplicate count over rows can therefore confirm uniqueness; an empty population cannot. The comparison keeps the evidence attached to what was actually measured. When unpaired objects have matching row counts and boundary measurements on at least two columns, Human Review can link them as a rename hypothesis even when their names share no fragment; the review member records whether the link came from measured_agreement or only a shared_object_name. Ambiguous candidates remain unpaired rather than being guessed. Every recorded comparison also discloses object_presence and not_measured from that run. object_presence is the authoritative object-by-object answer: it names every source object the target lacks or whose presence is undetermined, then bounds the list of present and surplus objects at 200 while keeping exact counts and omitted totals. not_measured lists the run’s indeterminate and errored readings with their causes, up to 200, and points to read_comparison for the remainder. Both fields are null on a comparison saved before the disclosures existed; that is unknown, not proof of complete presence or complete measurement. On a withheld comparison, do not infer presence from the withheld one-to-one readings: the disclosure marks them as withheld and undetermined. object_presence.not_built separately names declared derived targets the build lacks; these are computed tables, not source objects, and are not included in the source-object counts. Addressing is still one-to-one unless the sealed specification declares a general target mapping: object_map renames only, so a null or empty target is refused rather than used to declare an input-only table. Declare that table through the sealed specification’s target model. An object_map value may use a one-element list as an alternative spelling for one target, but a list naming several targets is refused instead of choosing one. A row-identity declaration may likewise name renamed key columns per side, positionally, so row witnesses can be paired when the business key itself changed spelling. A version-2 target_model is the explicit mapping exception: it can declare one legacy object split across several images or several legacy objects merged into one non-hub image.

​

Declared target mappings and Data Vault shapes

A sealed specification may carry an optional target_model declaration. Its default schema_version: "1" describes a Data Vault target: it requires vault conventions and at least one hub, and names the hubs, links, satellites, their derived metadata columns, declared ghost keys, and each legacy object’s split. schema_version: "2" describes a general mapping instead. It may use plain target images with no vault role, or annotate the images it names as hubs, links, and satellites to enable the corresponding vault checks. The proof reads this block only after verifying the spec seal; it is not a caller-supplied comparison mode. The version-2 target_model is one object, not a list of descriptive rows. If an agent passes rows shaped like {target, derivation, sources, grain, rule}, put them under the object’s derived array: use object for the target, derivation for the rule, and columns for the complete delivered column list. See the [register_target_model tool] (/docs/Genbot-Toolkit/Additional-Tool-Groups#register_target_model) for the validation response and the tool contract. At seal time, target-side SQL is checked relation by relation against the mapping’s declared columns, including schema-specific declarations. See the [author_spec contract] (/docs/Genbot-Toolkit/Additional-Tool-Groups#author_spec) for the refusal and resolution rules. On Snowflake, the seal reads each relation’s stored column names, so a correctly quoted identifier is not refused as a missing column.

​

Engine-pair renderings

Target-model obligations stay engine-neutral when their identifiers render the same across the supported dialects. If a relation or column needs engine-specific quoting, the seat renders that mapping for the run’s placed source-to-target engine pair. A run without a placed target cannot seal that quoted rendering; place the target for the run or use plain identifiers. The rendering records its engine pair, and grading it on a different pair refuses the check rather than running SQL whose quoted names may mean something else. Re-seal from a run placed on the grading pair. In a version-2 mapping, several legacy objects may feed one non-hub image: that image is the declared merge. Each image column still receives exactly one legacy column, while the comparison accounts for the union of columns carried by all of its legacy feeders. The same mapping can declare a computed target with derived: each entry names the target object, its legacy sources, the columns it must hold, a human-readable derivation, and optional grain. In a layered build, layer_sources names the build’s layer directly below that target; use layer_sources: [] when the target is computed straight from its legacy sources. A target the build gives a placeholder row on purpose (a dimension’s unknown member) declares it as unknown_member: {"column": "<key column>", "values": ["<key value>"]}; the seal then refuses a target-side domain invariant over that target that the member breaks (invariant_over_declared_unknown_member). A derived target is checked for presence and declared columns, and each source is licensed into that target with provenance: "model:derived"; its row content is not compared to any one source table because the target is computed. The first item in sources is the target’s driving input: declare the target’s row key on that legacy input, using the per-side form when names differ, so the key pairs the input rows with the derived target for witness localization. Witnesses compare the key and the target columns the model carries under the input’s names; other target columns are computed and are not compared cell by cell. Column-presence findings are filed on the derived target itself: object_name and target_object name the target, not the legacy input that answered for it. When the key has several columns, witness rows are ordered and paged on the complete composite key rather than on any one position. If the target is absent, the missing finding names the derived target as both object_name and target_object; it is not counted as a missing source object. A legacy source used only by derived targets need not exist under its own name in the target when at least one declared derived target that consumes it is held. If none of those targets is held, the source is also reported missing under its own name. The exception is a declared target or a declared layer_sources object whose base name is the same: that layer object counts as the held target image. A version-2 mapping may contain only derived targets, so splits can be empty when every target is computed. For a legacy object carried by a split, a caller can declare a row key for one image using the per-side row_identity form with an image member; see the row_identity request field for its payload shape. The target terms name columns on that image. When the split has exactly one image, image may be omitted and the key pairs with that sole image. For a split with several images, name the image as it appears in the target inventory or by its uniquely resolving model name; an image not declared for the split, a missing image on a multi-image split, or an image on an object the model does not split is refused. The key applies only to findings for its named image. Its witnesses compare the key and the columns the split carries from the legacy input into that image, under the image’s column names; sibling images continue to be evaluated independently without that key. Every derived target must also have a membership or recompute obligation that reads the target on its target side and reconciles it to at least one of its legacy sources on the source side, end to end through any layer between. A check against layer_sources may be included, but cannot replace the legacy-source reconciliation: two layers can share the same defect. During authoring, a target already present in the source estate with no declared layer_sources is refused with layered_source_undeclared; a target with no legacy-source reconciliation is refused with unanchored_derived_target. Neither refusal seals the specification. For an additional obligation comparing two derived tables, keep the comparison on the target side: use source_sql for a constant expected row (for example, SELECT 1 AS grp, 0 AS mismatches) keyed on grp, and use target_sql to count rows where the derived tables disagree. This does not replace the required reconciliation to a legacy source. On a run whose target is separate from the source, a source_sql that reads a declared build output can be refused at sealing; see the [author_spec contract] (/docs/Genbot-Toolkit/Additional-Tool-Groups#author_spec). An image name must use one spelling throughout the mapping; a bare name and its schema-qualified form are refused as ambiguous. A merge declared by the mapping and a delta’s object_merge operation must agree on the image and sources. If the declarations disagree, the merge is refused and the run records addressing_incoherence; the involved object_missing and object_surplus readings remain indeterminate rather than being treated as absence or newly created data. Object-name matching treats a dot inside a double-quoted identifier as part of that name, not as a schema separator: main."a.b" and "a.b" can name the same object, while "a.b" and "x.b" do not. The Prover does not take a whole-table digest for a declared split image because its columns are compared individually against the legacy columns they carry. That not_compared_by_design reading is reported as a design disclosure, not an unresolved difference, and never blocks approval. A declared derived target is different: its rows are computed and nothing compares its contents cell by cell against the source. Its derived_target_not_compared reading remains a blocker unless the grade’s sealed-coverage rules confirm the table; when it stays unchecked, the grade explains why. See the grade response details. Each image in a declared split is evaluated as its own finding coordinate. If the same legacy object and column appear on two target images, the Prover keeps those readings in separate findings keyed by their target images, so one image’s deviation or review status does not settle its sibling. When a later comparison encounters a finding created before that image-specific key was available, reconciliation matches it to the image named in its stored evidence before applying the new verdict. Reconciliation only treats an absent row_count finding on a split object as re-observed when the current run actually counted rows for the finding’s image. A satellite, link, merged image, or any other image whose rows were not counted therefore remains not_exercised instead of closing as resolved merely because the finding is absent from the run. The same protection applies to every finding kind under a declared model mapping. The run records, per legacy object, which comparison kinds it decided and which image or derived target it read. An open finding remains not_exercised when that kind was not decided on the object, or when the run read a different target, so silence cannot close an unmeasured bronze image, silver target, or derived-target reading. When a version-2 split has exactly one image, that image has no vault role, and no other source object feeds it through a split, merge, derived target, or ordinary one-to-one pairing, the image is treated as the legacy object’s sole carried image. The Prover compares their row counts; equal counts match, while a difference is an unlicensed row_count finding. Where both tables were digested, it also compares their content over the columns paired by the declared mapping, and compares the values of each paired column individually. SQLite supports both the per-column value checks and the comparable whole-table content fold. Columns present on only one side are excluded from the digest comparison and reported separately as missing or surplus. If a digest cannot be compared, the content result is withheld rather than treated as a match. If either row-count measurement is indeterminate, the row-count result is indeterminate instead of clean. With a model, the comparison does not force a legacy table into one arbitrary target table. A hub image is compared on the declared business key, excluding only the ghost rows the model names. For each legacy object carried onto a hub, the model generates a current-state obligation: the legacy row is compared with the hub joined to the latest row of each declared satellite, keyed by the legacy business key. For each declared junction split onto a link, it generates a link-membership obligation: the source pairs are resolved through the declared legacy references to participating business keys and compared with the link’s pairs after joining its hubs. The comparison uses the link’s full business key, including dependent child columns carried from the junction, so a child filed under the wrong hub key differs on both sides. These obligations use business keys, not derived hash keys, so they prove the data rather than the hash rendering. For every other image with a usable declared key, the model also generates an M-<image> row-membership obligation: satellites are keyed on the business keys of the hub or link they describe, links loaded from a hub’s own legacy object are keyed on their participating business keys, plain images use the key declared by their history, and a merged image with no vault role uses the key declared by every feeder. These checks compare distinct key sets, so they catch a carried row that was skipped or invented without mistaking a satellite’s multiple historical rows for a membership failure. An image without a usable key is listed in unrendered with the reason it cannot be checked; a sole image carried one for one remains covered by the current-state row-count and carried-column content comparisons against its legacy object. An attributed row-count or content difference fails the image’s declared must_match structural item; without an item, the difference remains drift, while a must_differ item explains it. Declare must_match when the image must remain unchanged, or write a membership obligation for it. If a rendered membership check is INDETERMINATE solely because its target has rows with NULL keys and its source has none, the grade records a decided FAIL: the rendered model keeps those rows, so they are orphans no legacy key derives. Other causes of an indeterminate check remain undecided. Generated obligation ids normally use object names without their schemas, but retain a schema when the model declares the same base name in multiple schemas. If composed ids collide, the colliding checks are rerendered with schema-qualified object names; any collision that remains refuses the model because one id must name one check. In a split’s references map, each value names the referenced split and column as <split source>.<column>. Spell the split exactly as declared, including its schema: for a split named main.branch, its branch_id reference is main.branch.branch_id. A declared link that renders no membership check cannot be sealed; the spec-author seal also checks hand-written population checks against historized links. See the finalize_spec refusal guidance. For a link loaded from a split, its rendered membership check reads pairs from the current source rows and each history relation declared for a satellite image in that split. The history relation must carry the legacy columns used by the link check; otherwise mapping registration reports the missing columns. This lets an insert-only link retain relationships that changed in later source rows without treating those earlier pairs as target-only drift. Link business-key registration also requires each participating hub to receive one key part in participant order, and measures each readable link key on its junction. A key that repeats or contains NULL is returned to the proposer with source counts and guidance to add the dependent child that identifies one junction row, because the resulting LNK-* check could only be INDETERMINATE; see the register_target_model contract for the exact refusal behavior and measurement cost. During authoring, an unavailable or unsupported source is reported as unmeasured rather than treated as unique. A historized image can declare the relation that holds its source history under history: {"relation": "<source history relation>", "batch_column": "<batch or effective-from column>"}. The relation is expected to hold the legacy row for each key in each load batch (or each version of an SCD2 audit); a non-vault historized image also declares its legacy key columns under key. register_target_model renders one history obligation, named H-<image>, which counts the source’s consecutive states per key and compares that count with the rows the target image holds. This is the source of truth for history grading: the current state table alone cannot reveal how many states the load should have written. If an image has no readable history source, the grade lists it in history_not_testable rather than presenting its history as matched; add the upstream landing batches, change feed, or snapshots to the image declaration and re-register the mapping. The completed grade persists each such object and its reason in obligation_verdicts.history_not_testable. Its verdict headline also names the count and up to five affected objects, then points the reader to that list for the explanation, so an untested history is not read as a matched history. When a history relation is not otherwise named by a split or derived target, the comparison also treats it as a declared input: if it resolves in the source and no target object shares its base name, it is read as a no-image split; a same-named target remains an ordinary one-to-one comparison. Derived vault columns are disclosed as model metadata, and a legacy column carried into no image is an explicit split_column_unaccounted finding. A declared image that the generator cannot reach is named as an unreachable shape instead of being silently treated as matched. The run records target_model_hash and live split-key evidence so the result identifies the declaration and the read it used. The seal also checks that every authored obligation can run on the declared target shape. Before a spec is sealed, its target-side SQL is prepared against the empty catalog of objects and columns declared by target_model; an obligation that names a missing table or column is refused with unrunnable_on_target_model rather than producing a specification that can never grade successfully. The author must rewrite the target query to follow the declared mapping and re-register it; finalize_spec describes the refusal and repair guidance. Specs without a target_model are unchanged. The authoring seal also refuses invariants with no counted constraint, undecidable structural items on carried columns, and excluded scope entries for objects the mapping delivers; see that guidance for the findings and repairs. Comparison expectations that cannot cover the keys their target checks grade can also be refused at sealing; see author_spec seal checks. For cross-engine targets, see author_spec target connection preparation. When Readiness paired a target estate with the source, pass that estate’s id as target_estate_id on the authoring call; the author_spec reference covers target placement and the seal refusal when no target is placed. When a chat prove call includes spec_hash but omits target_connection_id, Prover uses the target connection recorded in the sealed spec’s commissioned placement. If the seat recorded a source or target catalog but no target connection, Prover uses the source connection for the target; otherwise, pass target_connection_id explicitly. For the author-seat setup corresponding to this shared-connection placement, see the author_spec reference. The model must also license the vault metadata that the load derives rather than carries from a legacy column. Put a satellite’s hash-diff column under that satellite’s hash_diff, and put other load-derived columns — such as a status satellite’s is_deleted, an effectivity satellite’s is_active, or a hub’s last-seen date — under the owning hub, link, or satellite’s metadata_columns. A Medallion layer table carried whole from a legacy table declares the load metadata it adds (a bronze table’s load id and load timestamp) under its own image’s metadata_columns, so it is still compared one to one on content. An undeclared derived column is reported as an unlicensed column_surplus reading. A hub’s placeholder or ghost rows are likewise non-data only when their hash-key values are declared in that hub’s ghost_keys; otherwise they remain data and increase the hub’s row and business-key readings. When one of these declarations is missing, the finding detail names the model key and entity to add before rerunning the comparison. String-valued ghost_keys use the engine-specific quoting described in the validate_migration reference. When an author-seat run uses a SQLite connection, its brief includes SQLite-specific instructions for hash_key and hash_diff rules. Genesis registers genesis_md5_sum60(text) on each SQLite connection it opens, so the seat can compute the rule input’s MD5 suffix per row and compare it with the stored hash’s final 15 hexadecimal digits in a sealed check. It does not have to leave an MD5 rule unchecked just because SQLite lacks a built-in md5() function. This guidance is included automatically for SQLite runs; no setting is required. Model usage for specification authoring is recorded as system work in Pulse Costs under usage_category=prover and usage_subcategory=spec_author. This recording is automatic; it does not depend on the retired features.cost_accounting setting. See the author_spec reference. A migration’s column rename is a separate caller declaration: include column_map on prove or compare to pair the exact source and target names. The comparison then reports column_renamed and compares their content; without the declaration, the names remain separate column_missing and column_surplus readings. See the comparison request field for its shape and validation rules. For non-reproducible lineage records, the Prover also matches a renamed column by either its own name or its paired name, so the record is recognized in both forward and backward comparisons. For this response shape, see the estate API reference. When a declared mapping leaves legacy tables out of account, the run adds an unaccounted_sources guidance block beside the comparison verdicts. It names the source-side tables from table-level object_missing readings that no split carries and no derived target uses; a source already named by a split or derived target is not listed. For a mapping made only of derived targets (a computed gold or silver layer), register_target_model also checks the live table listing for each source schema it reads and refuses the mapping until every legacy table is accounted for. This catches a table that a correct build would otherwise appear not to have loaded. For each named table, either declare it as an input-only split with no images when the target loads it nowhere, or name it among the sources of the derived target that uses it, then re-register the mapping. The block includes the source/images declarations to use for input-only tables and the mapping’s next-step text. SQLite engine-owned catalog tables are excluded from this inventory. A version-1 or version-2 mapping may instead list unrelated tables nobody assessed in unassessed: {"objects": ["..."], "basis": "<the owner's ruling>"}. Quote the owner’s ruling for basis. This says nothing about whether those tables were loaded or disposed of; unlike a split with "images": [], it does not claim someone checked that the target loads a table nowhere. A listed table cannot also be used by the mapping, named by the spec’s scope or a structural item, or read by an obligation. Qualification does not exempt a read: if bronze.t is unassessed, an obligation that reads cat.bronze.t or other.bronze.t still names that table. The spec must declare a scope; otherwise finalization refuses the model. For a mapping made only of derived targets, this is the way to account for source tables outside the feed without asserting their disposal. The comparison records these tables in unassessed_sources and leaves their table-level object_missing readings unlicensed but outside findings about the build; a same-named target table remains unpaired. Candidate mapping requests are not offered when either the source table or a table with the candidate target’s name is listed as unassessed; the candidate reports no_request_reason: "unassessed". To request that mapping, first revise the model to assess the table. If an already-sealed spec is registered from outside Genesis, the same contradictions are reported as advisory findings without blocking registration; see the compiled-spec registration API. See the tool contract for the seal refusals and the proof API for the summary record. If the target catalog looks like a Data Vault but the sealed spec has no target_model, the run adds an undeclared_target_shape guidance block. It identifies hubs named with the hub_ prefix, links named with lnk_, and satellites named with sat_, msat_, esat_, or csat_, along with load-date and record-source columns. It deliberately does not classify pit_ or brg_ tables because the target model has no role for those query-assist tables. The guidance provides a minimal model skeleton to complete from the mapping document and explains how to declare it. On this path the one-to-one unlicensed and indeterminate readings are withheld from published findings and named by class and verdict, because they are readings of an undeclared pairing rather than evidence about the build. The same guidance key is used for a non-vault pair whose objects are unpaired on both sides: it names the unpaired source and target objects, reports shared column names only as an observation, and supplies an empty mapping skeleton. Those readings are withheld only when nothing paired; if another object did pair, the guidance is shown beside the real findings. The persisted comparison remains intact, but its published unlicensed and indeterminate counts count only published readings; the run summary records the published unlicensed count explicitly as unlicensed_published. Summaries written before that key existed derive it from unlicensed and withheld_unlicensed. the withheld counts are exposed as summary.comparison_counts.withheld_unlicensed and summary.comparison_counts.withheld_indeterminate. The GET /api/estate/runs full and card projections also expose decoded headline counts; see the estate run API contract. When a verdict has withheld readings, surfaces render its published and withheld counts together, including 0 published · N withheld (undeclared target shape); when none of that verdict’s readings were withheld, the headline does not add a 0 withheld count. Withheld readings are not unexplained differences or undecided readings, and the result is not treated as a green comparison. Targets that are not vault-shaped retain the ordinary one-object-to-one-object behavior. A comparison whose readings were withheld because nothing paired sets nothing_compared: true in its review population and cannot be approved; declare the mapping, reseal the specification, and run the proof again. Under a declared mapping, each target object and declared column that the comparison finds is counted as a comparison, even when it finds no difference. A declared mapping that still records zero matched comparisons therefore needs investigation: check that the target snapshot is the build the mapping describes and that the mapping uses the target names as the build spells them, then re-prove. A grade’s own checks do not change that comparison-level result; see the [Prover approval guidance] (/docs/Genesis-Prover/Agents-And-The-API#comparison-cards-in-chat) for the cause-specific remedies. When a sealed specification grades a comparison with withheld readings, the grade keeps conformance.drift_count as the measured total but uses conformance.published_drift for the drift published as unexplained. conformance.withheld_drift reports the measured drift readings withheld because the target shape was undeclared, or null when none were withheld. Withheld drift is named in the not-verified headline with the same declaration guidance; it is not presented as unexplained drift to investigate. The grade summary also reports conformance.withheld_indeterminate for indeterminate readings withheld by the comparison, or null when none were withheld. The graded review sets these readings aside rather than counting them as undecided, matching the ungraded summary.comparison_counts.withheld_indeterminate count. Every measured element the Prover compares comes back as exactly one of four verdicts, and the fourth is the one that makes the other three trustworthy: For categorical value-count comparisons, a rendering recipe split, an unknown engine, or a known measurement-library version that this build does not reproduce can make the two hashed value domains impossible to line up. The Prover reports that limitation as indeterminate with cause="categorical_recipe_mismatch" instead of claiming a value change it did not measure. In the version case, relied_on.basis is recipe_version_foreign and identifies the version that measured both sides. Case-folded column pairings remain visible as licensed column_relocated elements, and licensed summaries identify which comparison and provenance accounted for each licensed element. The agent-facing comparison surface also exposes errored for a read that failed before it produced a measurement. It is UNMEASURED, never clean; see How agents drive the Prover for the handling and the complete read contract. Every completed comparison also publishes value_coverage, so verdict totals are not mistaken for proof that data values were compared. Its columns and objects blocks count, respectively, paired column value digests and paired whole-table checksums: readings is the measured denominator, compared includes match, licensed, and unlicensed, and not_compared includes indeterminate and errored, with not_compared_by_cause naming the reasons. A column with no value digest on one side is in neither count. statement is the sentence to relay, and basis defines the counting rule. When digest fold recipes differ between the two engines, digest_families names the source and target recipes and the statement says that values were not compared; a re-fold cannot repair that mismatch because each side must be read with its own recipe. The block is null for comparisons recorded before this disclosure, which means unknown—not “all values compared.” When recharacterize is present, follow its snapshot-specific re-scan guidance before treating the refused readings as permanently incomparable. For instrument_version_mismatch, the block names the snapshot ids to re-characterize; re-characterize every side named in recharacterize.estates before comparing again. If the block is null, the affected side’s measurement version was not recorded, so its value is not comparable yet. See the comparison response contract. When a run’s next recommends several scans, next.args gives the first characterize call and next.why lists the remaining calls to make before the follow-up proof. Every stored comparison also records the diff engine that computed it as diff_engine_version and diff_engine_digest. An unpinned comparison reuses only a comparison recorded by the current engine; a comparison from a retired engine, or one written before engine identity was recorded, is skipped and recomputed. A grade pinned to a retired-engine diff_hash recomputes that comparison on the same stored snapshots under the current engine — nothing is rescanned — and grades the result. The grade says so under provenance.comparison_recomputed_under_engine, naming the comparison it was given, the one it graded and both engines. The grade response contract defines when an approval carries or is superseded, including when a revised spec changes the result, and the returned disclosure. The retired comparison’s own review page and landing card then say the same — its approval was superseded by that run — and link to the comparison the run graded, where the review now lives. A carried approval is not a new decision: the new comparison’s review page says it was carried from the earlier comparison, names who approved it and when they did (never the moment the regrade finished), and links that comparison; the retired comparison’s page says where its approval was carried and links the new one. Three retired comparisons are refused with a 409 instead of recomputed: one over a snapshot measured under an older measurement library (the refusal names the snapshot to re-characterize, because only a rescan can bring it current); one made under a declared target model the graded spec does not declare; and one that paired rows on a declared row key its record does not hold. The last two cannot be reproduced by a recompute; run the comparison again (for a model, prove with the spec attached) and grade the new one. Grades expose the recorded engine as comparison_engine_version; null means the comparison predates engine recording and does not imply the current engine. A column content check whose digest was requested but could not be read is published as an indeterminate column_content_digest finding with cause="object_unmeasured". Its detail identifies the side whose column content checksum was unread, so an absent digest is not mistaken for equal values. Columns that were never asked to fold, and sampled scans already disclosed at object grain, remain silent. When a content-only re-fold cannot be tied to a stored whole-table fold, the indeterminate detail identifies which side was unanswered and why, such as a missing re-read or witness, a different set of columns, or a table that changed since measurement. The part worth understanding is how a difference becomes licensed, because that is where the Prover differs from a comparison tool. The Prover is default-deny. A difference is licensed only when something explicit covers it: Some licensed readings rest on an assumption rather than a person’s decision. The comparison discloses each one with a plain-English statement, its scope, basis, whether it was seeded by Prover or earned by an engine probe, and the covered readings by comparison. Typical examples are Snowflake’s upper-cased unquoted names, the proven bigquery->databricks type spellings and value renderings, the exact SQLite type spellings proven for Databricks and Snowflake, and an identical collation ordering measured from both engines. These assumptions do not change the comparison or its hash; they explain what the licensed count rests on. For a SQLite source, the seeded exact-spelling assumptions are INTEGER and INT → Databricks bigint, REAL → Databricks double, and TEXT and VARCHAR(n) → Databricks string; for Snowflake they are INTEGER and INT → NUMBER(38,0), REAL → FLOAT, TEXT → TEXT(16777216), and VARCHAR(n) → TEXT(16777216). Each mapping is its own assumption, based on the live SQLite, Databricks, and Snowflake golden run; the SQLite TEXT to Snowflake mapping also rests on Snowflake’s documented full length of 16,777,216, which is the size recorded for a VARCHAR declared without one. Narrowing types, representation changes, and cross-class landings remain findings: for example, Databricks int or float, Snowflake NUMBER(10,0) or scaled NUMBER, and text or numeric landings in the wrong class are not licensed. The Snowflake full-length target licenses a same-base declared-width difference only when the source column’s measured longest value, in characters, fits within 16,777,216; if that value was not measured, the difference remains a finding. SQLite does not enforce the declared length in VARCHAR(n), so its Snowflake mapping licenses only that full-length target; a shorter declared width such as TEXT(50) or TEXT(10) remains a finding. PostgreSQL sources also receive built-in platform-type assumptions for Snowflake and Databricks. These are applied automatically to declared-type readings; they are not proposed rules and do not require pack seeding or ratification. A mapping licenses only the same type: PostgreSQL VARCHAR(n) matches the same target length, PostgreSQL NUMERIC(p,s) matches the same precision and scale (NUMBER, NUMERIC, and DECIMAL are equivalent spellings on Snowflake), and unbounded PostgreSQL text matches Databricks STRING or Snowflake TEXT(16777216) only when its measured longest value fits. The target’s chosen longer or shorter bound, a constrained type for unbounded source text, unconstrained PostgreSQL NUMERIC, and cross-class or narrowing mappings remain findings. PostgreSQL integer types map to Snowflake’s sole integer spelling, NUMBER(38,0); PostgreSQL DOUBLE PRECISION and REAL map to Snowflake FLOAT (all are 64-bit there), while Databricks DOUBLE and FLOAT preserve their respective 64-bit and 32-bit source types. PostgreSQL timestamps and times map only when time-zone semantics and fractional precision are preserved; timestamp-without-time-zone does not map to the Databricks session-time-zone TIMESTAMP. These pair-specific assumptions use ids beginning platform_type:postgres->snowflake: or platform_type:postgres->databricks: and can be withdrawn for an estate pair like other rule-borne assumptions. When the comparison’s case-insensitive object-name policy is off, the Prover assumes the target platform’s own identifier fold by default: Snowflake folds unquoted identifiers to upper, and Databricks folds them to lower. It uses that assumption only when the source and target are the ASCII, single-case spellings of the same dotted identifier; mixed-case, non-ASCII, and ambiguous fold candidates remain findings rather than being silently paired. The broader case-insensitive policy remains an explicit comparison option, and takes precedence when enabled. The platform-fold license can be withdrawn for an estate pair when the comparison relied on it; the next comparison then reports the folded-name differences as missing and surplus rather than pairing them. For the target platform’s withdrawn fold, those findings name the platform license in would_be_licensed_by and contribute to that withdrawal’s findings_returned; withdrawing a source platform case does not tag forward findings. The same withdrawal applies to an engine-earned collation ordering when the comparison’s probes produced identical orderings. If that license is withdrawn, a measured text minimum or maximum that still depends on ordering returns as indeterminate, with detail naming the withdrawal and boundary. A minimum the empty-string rule can decide remains a finding because it does not rely on the ordering. Restoring the license allows the boundaries to be compared as content again. When the target reports declared primary and unique keys as informational rather than enforced, a missing target declaration can also be licensed by a seeded platform assumption — but only after the key’s uniqueness was checked. The Prover records basis: "unenforced_key_uniqueness_checked" and, for each covered key, whether it was declared_row_identity_probed_unique or measured_unique; the latter requires an exhaustive, unsampled target read with no nulls and a native distinct count equal to the row count. A composite key that was not declared as the row identity, or a target whose key-enforcement status is enforced or unknown, remains an unlicensed finding. A ratified correspondence rule still takes precedence over this platform assumption. The same platform limitation can explain a missing source unique index on a target that records unique declarations without enforcing them (Snowflake), or cannot declare them (Databricks). The comparison must verify each index key unique on the target rows it compared: either the key is the declared row identity and was probed unique on both sides, or it is a single column checked by an exhaustive, unsampled target read with no NULLs and a native distinct count equal to the row count. The evidence is recorded in the element’s relied_on with basis: "unique_verified_on_compared_rows"; it does not cover rows loaded later. Non-unique indexes, unverified or undeclared composite keys, and targets whose enforcement is enforced or unknown remain findings. A rewritten in-database view definition can also be licensed when the view’s data matched on this comparison and the newest-started finished validate_migration behavior proof that tested that view pair passed and proved an output read from the source view. A proof must identify the source relation it read and, when the target adapter records its own relation (currently snowflake_sql), that relation must be the compared target view. A proof of another rewrite between the same database sides does not license this view. Setup and validation refuse a Snowflake proof whose profiles resolve a tested view to the same live object; non-rehearsal campaigns enforce the same guard. See prepare_migration_prover for the profile correction. When the target relation is unavailable, the proof is not credited for views whose source and target are in the same database, where the sides alone cannot distinguish rewrites. Each side is the snapshot’s database on its connection; the run’s source and target profiles must identify those same respective sides. Matching connections alone is not enough: a proof against another database on either connection, or a profile that does not identify its database, cannot license the view. Profiles must record a database for an adapter that supports side matching: postgres_dbt and mssql_sql use database, snowflake_sql resolves its configured name to Snowflake’s stored name (unquoted names are upper-cased; quoted names are verbatim), bigquery_sql uses project, and databricks_sql, databricks_notebook_sql, databricks_repo_sql, and databricks_pipeline_sql use catalog without regard to case. The comparison records the proof run and the data readings in relied_on; if either half is missing, or the view has any non-matching, indeterminate, or errored data reading, its different body remains a finding. This forward-only assumption has id translated_view_behavior_proven. For a given view pair, the newest-started finished proof that tested it decides: a failing proof supersedes an earlier passing proof of that pair, while a proof of another pair neither replaces nor blocks it. Both this license and the unique-index limitation appear in the comparison’s assumptions disclosure and can be withdrawn for the estate pair. For a Databricks target produced by a declarative pipeline, the comparison can also disclose two pipeline-expectation assumptions. pipeline_width_expectation covers a source VARCHAR(n) read as target STRING only when the deployed pipeline’s own published dataset declares the matching width expectation with action FAIL UPDATE. pipeline_not_null_expectation covers a source NOT NULL read as nullable only when that dataset has the matching single-column IS NOT NULL expectation with action FAIL UPDATE. Evidence is tied to the behavior proof’s deployed update and exact repository revision; the update must still be the pipeline’s latest and must predate the target measurement. The comparison names the update, source file, and expectation in relied_on. WARN and DROP ROW do not license either difference. If the target is not Databricks, the update is no longer current, evidence cannot be matched to the measured target, or any source-file digest differs, these differences remain findings. When Foundry’s job-spec record says a source dataset is built, its absence from the target is licensed by the seeded source_built_output assumption: the translated pipeline is expected to produce that output, rather than the transport copying it. The reading’s relied_on identifies the producer and source platform. A Foundry dataset whose job spec could not be read, or whose record does not identify a producer, keeps an object_missing finding. The corresponding target-side object_surplus is licensed when the target Foundry record identifies its producer. A built dataset present on both sides is paired and compared normally. Other source dialects do not supply this build provenance. The same disclosure carries licensed_by_assumption, the number of licensed readings covered by at least one assumption, issues_not_covered_by_assumption, the remaining non-match readings, and assumptions_sentence, a one-line summary. Report the latter two counts after accounting for assumptions rather than presenting covered readings as findings. When a run predates assumption recording or its run record is unavailable, all four fields are null, which means unknown; an empty assumptions list means the comparison recorded that it relied on none. An operator can withdraw a rule-borne assumption, the platform-fold license, or the engine-earned collation license for one estate pair from the comparison review surface or a chat comparison card, or an agent can call withdraw_assumption. The withdrawal applies to later comparisons of that pair: a rule-borne assumption’s covered readings return as findings naming it in would_be_licensed_by, while the two licenses change the comparison behavior described above. The prior comparison remains historically unchanged, but a sign-off whose pass relied on that assumption reads reopened until the withdrawal is restored. Restoration is available to a person for any withdrawal; the agent tool can restore only an agent withdrawal. A later sealed specification cites the withdrawals in its provenance rather than changing the specification’s bytes. See the assumption withdrawal API and the withdraw_assumption and restore_assumption tools. The Prover takes the withdrawal ids and their attribution records from one snapshot when it keys a proof or comparison. That same snapshot controls the rules and the withdrawal bylines recorded for the run, so a restore or re-withdraw that lands while the run is being admitted cannot change either which withdrawals apply or who the run credits. On Snowflake, withdrawal and restoration use a guarded MERGE because the ledger has no advisory transition lock. If the pair’s standing changes between the check and the write, the operation is refused rather than appended; read the assumption’s current standing again before acting. Everything else is the unlicensed residual: an open finding, in front of a person. That residual can reach the Adjudicator even when the proof has no sealed specification. A no-spec compare has a system_diff subject of its own, so adjudication reads the comparison’s unlicensed, indeterminate, and errored elements instead of treating an empty grading envelope as a clean result. The comparison also reports its full five-way census — match, licensed, unlicensed, indeterminate, and errored — so no_findings with clean_comparison means the measured comparison contained only matches and licensed differences, not that the comparison had no elements. See the estate API reference for the subject resolution and response fields. A platform-only migration envelope is different from a failed or empty specification grade. With no specification and no caller declaration, it is labelled No specification attached yet, opens no findings and no Human Review worklist, and tells the reader to attach a specification and grade the comparison. A caller can instead pass change_expectation to declare the migration’s shape: must_match means a lift-and-shift, so a clean comparison is the answer to that premise and its next call is propose for a human decision; must_differ says that the target should change, but licenses nothing without a specification, so a clean comparison still points to author_spec. The proof summary preserves this declaration as declared_change_expectation, including the calling identity that made it. When a specification is attached, change_expectation must restate the shape every structural item declares; the sealed specification owns that shape and a disagreement is refused. Once specifications exist, only grades for the newest recorded specification are eligible to become the comparison’s displayed chapter. The newest specification is the one named by the most recently started grade that names a specification; older-spec grades are superseded for this display. If that newest spec’s grade measured nothing, the comparison opens with no chapter rather than falling back to an older grade. Within that spec, the newest authored grade is displayed whether it verified or not; verification does not keep an older grade above a newer one. If the displayed grade is not verified but an earlier grade of the same spec verified, the review identifies that earlier grade. For a derived target column with no source namesake, the structural check abstains, but the item is verified in scope when every sealed check for it passes. Opening the comparison card does not launch a grade; grading requires an explicit request. See POST /api/estate/migration-envelope/grade. The claim card says the item is where the spec puts it, with the shape it declares; its values are confirmed only by the checks the spec declares. It identifies those clauses and passing checks without claiming independent behavioral confirmation. An observed open finding is not necessarily outstanding: a person can approve or waive a difference without making it disappear. In the findings read, the settlement axis distinguishes an accounted-for difference from an unsettled one; use its settled value and basis when explaining what remains. The estate API reference defines the row and comparison summaries. An approval is therefore a state of the measured comparison, not merely a historical review event. API consumers should use ruling_rollup.review_decision as the revalidated approval state; its population-matching rules are defined in the estate API reference. Three rules hold on the licensing side and are worth knowing before you review anything:

• A proposal never binds by itself. A correspondence rule licenses variance only after a named person ratifies it for this transition. A rule that is qualified but not bound to your transition licenses nothing in it.
• A declaration has a human principal. The measurement tool records the signed-in person, names the acting agent when the declaration comes through a bot turn, and refuses scheduled or bot-only calls without a signed-in user; see the tool reference.
• A rule that is refuted is retired, not quietly downgraded. The history stays readable.
• A diagnosis never closes a finding. Deciding what a difference is — even licensing or waiving it — records your conclusion. The finding discharges only when a later comparison over the same pair no longer exhibits the difference. Closure is independent re-verification, never assertion.

At backend startup, Genesis checks shipped packs for pairs that still hold an older, unsuperseded copy. It seeds the currently pinned edition beside that copy and links the older definition to its successor. It edge-qualifies only unqualified rules from that pack; when an earlier startup already superseded the copy, a later startup only picks up pinned pack rules left unqualified. This keeps the shipped-rule worklist aligned with the pinned edition without ratifying rules or binding them to a transition. Renames and relocations get particular care, because “the object is fine, it just moved” is the easiest thing to wave through. A systematic relocation can be licensed by a reviewed map over object identities — but that map brings obligations of its own: it must be complete and unambiguous over what it licenses, and every reference to the moved objects must resolve under the same map. A view still pointing at the old name is a deviation even though the object it wants exists. Correct-though-relocated is a verdict the Prover can deliver; it just refuses to deliver it on faith.

​

3. Spec conformance — the spec agent and the grade

Everything above works with no specification at all. Attaching one is how you move from “here is what differs” to “here is whether we delivered what the ticket asked for”. The spec agent turns a ticket into a sealed specification. It works in one thread with read-only access to the estate, and it builds the artifact a piece at a time: structural items — what should have changed, at what locus — and derivational obligations, the value-level expectations expressed as checks. Three properties matter to whoever will trust the result:

• Its claims are checked as it writes them. An obligation’s query is validated against the live estate at the moment the agent registers it, so an invented table name is rejected while the agent is still authoring, rather than surfacing as a broken grade later. Where the agent settles an ambiguity by measuring the estate, the grounding query is re-run by the tool, so the number in the specification is a measurement rather than the model’s assertion. Comparison checks that restate a value instead of measuring their asserted object are also refused; see the register_obligation refusal guidance.
• It works under a pinned constitution. The doctrine the agent authors under is pinned by name, version and content hash, and the tools refuse to run when that pin is not in force. A specification authored under no doctrine would be indistinguishable afterwards from a constrained one, so the product does not allow it to exist.
• It repairs prior seals in place. A repair round seeds itself from the previous sealed specification and edits it, rather than starting empty and reconstructing it from a description — which is how details quietly go missing between rounds. The clause ledger is matched to the repair round’s document, with moved clauses following their wording; see the load_prior_spec reference for the returned entries and open-clause handling.
• It writes only what the diff cannot see. Its constitution states what the system diff already measures on every proof — object presence, column presence, types, row counts with row identity, value distributions, keys — and instructs the agent not to restate any of it. A hand-written restatement doubles a finding at best, and at worst contradicts the diff’s own measurement. What is left for the agent is what only judgment finds: business rules, semantic invariants, cross-table consistency and derived-value rules. The exception is an absolute: the diff compares the two estates, so it can say the row counts agree but never that either equals a figure the ticket names — a stated count, type or domain stays the specification’s to check. And a comparison the diff could not take is not one it passed: it skips wherever either side is unmeasurable, so where it abstained only an obligation in the specification delivers a verdict.

​

Rules beyond the diff in a fresh Registrar round

Fresh Registrar rounds add seal requirements for value agreement on derived outputs and for applicable platform-declared rules; classic tooling and repair rounds are unchanged. The Registrar tool reference explains how the author supplies those checks and handles catalog declarations the system cannot verify.

​

Target column type assertions

An author-seat caller can supply target_column_types as assertions tied to source clauses. The run summary retains those declarations, the commissioned target_engine, a target_type_screening status (declared_columns_only or engine_unknown), and any target_type_findings; the seat also receives the declarations with the engine context. Screening identifies the engine from registered connection metadata only: it does not read target DDL or data. The assertions are not evidence that the workspace supports a type. On Databricks, recognized zone-free TIME types produce native_time_support_unverified; time-zone-bearing TIME types produce time_zone_offset_unencodable, because the supported HH:mm:ss text encoding cannot preserve their offset. An unrecognized type whose base token is TIME or TIMETZ produces time_type_unrecognized. For the separate seal-time storage gate, see the author_spec contract. SQLite time-text checks also compare the value’s byte width with an eight-character time literal. This prevents text with trailing bytes hidden after a NUL from passing because SQLite’s LENGTH and GLOB stop at the NUL. A one-line ticket is a valid specification brief. “Migrate the SALES database to the target system as-is; the data values must match” pins no output relation, no column, no derivation and no domain, so the agent seals the smallest sealable specification — the row-set claim its constitution requires — and the diff carries the rest. The constitution states what that shape is; this page deliberately does not repeat the counts. That is the right answer for a lift-and-shift, where the only claim is that the data values survive the move. A ticket that states a business rule, a derivation, a domain, a reshape or a new mart gets a correspondingly larger specification, because each of those is something the diff cannot measure. For author-seat runs, the submitter can keep operator background (build history, reloads, or earlier findings) separate from requirements. Context is not graded: the seal refuses an obligation supported only by that background, and a written_by check requires the requirements to name its job, notebook, or pipeline mechanism. A repair carries forward each check only when the same obligation id retains the part that check grades; see the author_spec input contract. The same mechanism check applies when a spec is authored directly in chat or through the CLI’s seat verbs, without a commissioned seat-run row. In that path, a newly authored written_by obligation is refused because no recorded ticket or asset requirement names the mechanism. If the owner’s requirements specify a producer, commission the spec through author_spec with those requirements; otherwise remove the mechanism demand and record the build details as substrate with register_substrate. A carried obligation in a repair is evaluated under its prior commission. Finalizing runs the full artifact validation and seals the specification: it is content-addressed, so it is tamper-evident and can be named unambiguously afterwards. When a sealed specification is authored outside Genesis and registered for grading, the caller can hand over the uploaded file or its exact text instead of retyping the parsed object; the compiled-spec API reference describes the three forms and the byte measurement returned by registration. For the direct tool-call text limit, see the register_spec tool reference. Repairs are tracked as a chain rather than an overwrite: a repair round produces a new sealed specification that names the one it was repaired from, so the lineage of a specification across rounds stays readable. For a repair registration with a declared parent, omitting round_n makes the store allocate the next round after both the parent’s round and its existing children. Thus a repair of round 1 is round 2, and separate repairs of the same parent receive distinct round numbers. See the compiled-spec API reference for when to omit round_n and the explicit value limits. The author-seat contract explains how repairs retain prior owner questions, checks and still-standing rulings, and when changed facts allow them to be raised again. On Snowflake, registration claims a repair round in the write; see the compiled-spec API reference for how concurrent registrations of the same round are resolved. The grade runs a sealed specification against a comparison. Each item comes back as one of four readings: For a same scope object whose whole-table digest recipes cannot be compared across engines, passing row checks can verify the object instead. The checks must be full-table membership checks that pair the same rows on the same key on both sides, and they must compare every column whose digest cannot be compared on that key. Each remaining column must have a comparable digest that agrees or a moved digest accounted for by an accepted difference. When these conditions hold, the grade reports the object as implemented and names it in row_checked; otherwise its verdict remains indeterminate. The grade headline says this verification was by row checks, not by digest. For behavioral migration validations, the Prover starts only after every submitted stimulus case is stored for the exact boundary being prepared. If a case is already stored under another boundary, or the store contains fewer cases than were submitted, preparation refuses readiness rather than allowing validation to run against an empty or partial case set. The agent-facing details and response fields are documented in prepare_migration_prover.

​

Logic-path coverage for stimulus design

When designing a stimulus campaign, pass the optional manifest_path argument to design_stimulus_campaign to compare its cases with paths enumerated from the dbt manifest’s model SQL. The enumerator recognises paths such as IFF and DECODE arms, QUALIFY predicates, individual COALESCE/NVL arguments and outer-join arms. It reads metadata.adapter_type to choose the SQL dialect; a missing or unknown adapter falls back to PostgreSQL and is logged. The response’s logic_coverage summarizes the point count, claimed count and ratio, and names uncovered paths in named_exclusions and next_batch_targets. Targets carry the model, output column, SELECT scope, expression or arm, and source line numbers; the response includes up to 25 next-batch targets and 50 named exclusions. When a report is produced, it also includes models whose SQL could not be parsed in unparseable_models and claims that are unknown, ambiguous, stale or unrecognised. If no points are enumerated, logic_coverage is null. For the claim-tag format used by cases and mutation audits, see the source-contract tool guidance. For a rewritten view pair, the designer can also read both views’ stored text and logic outlines, then check that the cases claim the paths they exercise. Check claims with check_claims_only=true before preparation so the check stores nothing; pass the same view_pairs to prepare_migration_prover to record the claims report with the stored cases. The report is informational: claims do not block preparation or change a proof’s verdict. It uses the latest stored view snapshots, so claims need new tags if a view is changed and scanned again. See the tool reference for pair fields, size limits, and response details. Databricks stimulus adapters also reject an unresolvable workspace host before opening the SQL driver; see Databricks connection behavior. For a deployed Databricks Job target, call preflight_databricks_job_contract first to read the canonical hash, contract version, run identity, and parameter formats needed by the profile. The toolkit reference also explains the selective and monolithic Databricks Job modes and their different output isolation contracts, plus the recorded profile attribution returned by prepare_migration_prover. Databricks Job observation and failed-campaign evidence-retention rules—including read-back status for landing files and output relations, plus the per-run and per-task Databricks identifiers used to route a finding back to the job that produced it—are documented with validate_migration. Databricks Job and Run reads used by these checks follow paginated responses; an incomplete response is refused instead of being hashed, pinned, or treated as complete evidence. Each target can retain separate specs for different case sets; re-authoring the same target and case-id set replaces that spec’s effective version rather than dropping other case sets. See the tool reference for the submission and conflict rules. Only implemented satisfies completeness. An indeterminate item un-verifies the run rather than quietly passing it, which is the whole point of having a fourth reading at all. For a changed structural item, a declared column type change counts as implemented even when the source and target values produce the same content digest. A type difference that the comparison licensed as a rendering, or that the specification’s type_mapping rule accepts, does not count as the requested change; it is the engine’s spelling of the same logical type. A mapping that can lose fractional values on landing in a scale-zero numeric type is conditional: it accepts only source columns measured to contain no fractional values. A mapping into a type that holds fractions, such as NUMERIC -> DOUBLE, needs no condition: a type licence reaches only the column_type reading, never a value. Any loss of integer precision or exact fractional representation changes values, which remain subject to the value readings; an expectation that whole numbers land as integers belongs in the seal’s obligations, not in the type licence. The compiled-grade API reference describes the live-source measurement and its provenance. Grades run in two tiers. The structural tier grades the specification’s structural items against the comparison; it is the tier that resolves the comparison, so its findings get the durable numbers a person cites in a review. The derivational tier grades every obligation against the two live databases, and each obligation comes back pass, fail or unverified — a result the instrument cannot vouch for renders neutral, never green and never red. The conformance verdict carries requested_changes and confirmed_changes beside its headline. The run envelope and its cards use these grade-owned counts directly: requested_changes counts the sealed envelope’s items and scope entries, while confirmed_changes is the legacy count of confirmed grade items. For the current items_matched_in_scope and items_passing meanings, including why they differ from confirmed_changes, see the grade response reference. Do not rebuild the card’s denominator from the scope entries; the grade judges the items, and its own counts keep the headline and card aligned. A same scope entry is met when the object is unchanged or when at least one moved column-content digest is fully accounted for by an accepted-difference rule, all other content changes are also accounted for, and no column was added or removed. For a value substitution, the rule must account for the entire column-digest change; a partial explanation does not make the object the same. The digest’s null-count change must also agree with that substitution: replacing values with NULL must add exactly the number of substituted values, while any other substitution must leave the null count unchanged. Unexplained changes or undecided content also prevent this accepted-difference treatment. An unlicensed column_surplus on a same object remains drift when no spec item names that column; an object-level item does not explain a column the source never had. For same scope entries and structural must_match items, a content digest that moved only because paired FLOAT / DOUBLE values were licensed equal within the comparison’s platform float tolerance counts as unchanged. The comparison must license every moved column digest under the float tolerance alone; when the whole-object digest moved, its re-fold without those columns must also match. The grade names the tolerance licence and, when recorded, the largest relative difference. An unlicensed or non-float change still counts as a move. This tolerance does not change must_differ grading. See the comparison tolerance rules for how values are read and licensed. An object-level item on a split legacy object is decided by its matching new or changed scope entries, because the item applies to the object across its declared images. Removal items are not settled this way: an arriving image contradicts a claim that the object was removed. The item is settled only when every matching entry has the same decisive verdict (implemented or not_implemented); an abstaining or disagreeing entry, or no matching entry, leaves it indeterminate. For an implemented non-removal item other than add_table, presence alone is insufficient: the item must declare a change_expectation and have at least one passing sealed check attributed to its spec_id. Those check ids appear as its confirming checks, and the grade records that its content was confirmed by checks. A not_implemented entry settles the item as not implemented without that content confirmation. When a matching scope entry settles an implemented add_table, it is met by its scope entry and does not also appear as a prover_detection_gap: the split-object comparison grades the declared images, so it cannot detect the faithful carry itself as a difference. An implemented, undetected must_match item is also not a prover_detection_gap when it is not a removal. must_match claims that the locus arrived unchanged, so no difference in the blind comparison is consistent with the claim rather than a missed change. A changed scope entry can also be met when its content digest is unchanged or could not be compared, if a drop_constraint item confirms the declared key removal there. Every item on that entry that states a change must be a declaration-only change, and each item there must be confirmed as implemented; a content-changing item cannot be stood in for by a dropped key. A failed structural item or a sealed check that failed on the target table also prevents the declaration from meeting the scope. A missing or unmeasured check does not by itself block a key removal confirmed by the structural item; the grade still needs the declaration evidence from the check fold. See the register_structural guidance for how to name the key in the item. An item that may change content but whose locus resolves to neither estate can affect any scope entry. If declaration evidence would otherwise make that entry implemented or indeterminate, the grade leaves it indeterminate: the unplaced change may also belong to that object, so the declaration is not known to be the whole change. A failed sealed check is not hidden by structural abstention. When an obligation fails without a license, the finished grade names it in verdict.failed_checks, changes the headline to Not verified, and records its mismatch count, compared-row count, and up to three sample keys when the check localized mismatches. A key count stopped by the engine’s cap is shown as at least N, with mismatched_keys_overflow reporting additional keys found past that cap; neither value claims an exact full-population count. If the target lacks a column the check reads, no key was localized: mismatched_key_count is null, missing_target_columns names the column or columns, and unchecked_source_rows gives the source rows the check could not check. Its rendered sentence names the missing column and says how many source rows could not be checked, rather than presenting that population as a mismatch count. For localized failures, the sentence also says whether keys are one-sided or differing, names differing columns, and shows sampled source/target values. When keys occur only on each side and no paired row differs, it states the counts present only on the source and only on the target, then says every key present on both sides matches. If localization stopped at the engine’s cap, the sentence says “every localized key present on both sides matches” and presents each count as “at least N.” When the result names keys for both sides, examples identify up to two keys present only on each side; otherwise, each quoted key is described as “on one side only” without guessing which side. A one-row differing check reports the compared column and both values directly. The not-verified headline leads with failed checks instead of leaving them after the structural clauses. When failed items are attributed to those checks, their grouped failed-item clause leads, followed by the failed-check clause, checks with no verdict, and any remaining structural qualification. Each named check in the grouped failed-item clause is followed by its item count (for example, OBL-X (2 items)); with a total, a single-check clause reads N of M changes failed, caused by 1 check (OBL-X, 2 items). The failed-check clause names every check when there are five or fewer; above five, it names five and summarizes the rest as and N more, with every remaining check named and sized in verdict.failed_checks. A named check carries its mismatch and compared-row counts when available. If the engine refused a keyed comparison, its size comes from the key probe instead: observed duplicated keys and rows with NULL keys, by side. A duplicate-key count recorded as a lower bound is prefixed with at least. When some declared checks decided and others did not, the headline also gives the undecided count as N of M spec checks reached no verdict, alongside the failed checks. If the coverage counters are incoherent, it says coverage cannot be read instead of presenting an undecided count. Any requested change whose item verdict is fail or unverified keeps the grade Not verified, even when the grade’s own verdict status would otherwise read verified. The landing and review Overview use this same rule as the comparison card in chat. For how a keyed check with target-only duplicate keys is classified, see the grade tool reference. The same failure is added to the comparison’s Human Review population as a missing_requirement blocker under obligation_failed, so a reviewer can act on the check even when the structural tier has no item at that locus. Licensed failures are not included. For a must_match item whose table or column exists only in the target — including a Data Vault hub, link, satellite, or a whole derived table — the structural oracle abstains because there is no source namesake or content baseline; the sealed checks are the evidence that decides it, just as they are for a derived target column. When a derived table is listed in derived_checked, an implemented-but-undetected item at that table or one of its columns is covered by those checks rather than reported as a prover_detection_gap. The run’s headline is one of three, and the middle one exists deliberately: An unattributed difference is drift, and drift keeps the verdict open.

​

4. The adjudicator

The Adjudicator is a seat that settles findings against the rules and rulings already in force — reproducing what the finding claims before judging it, and citing what it judged under. It has no instruments of its own: it judges, and it never runs a measurement or builds anything. Provider failures are surfaced before seat startup; see the provider preflight setting and API response contract. Its behaviour is governed by one operator setting, estate_char.adjudicator.mode: For the verdict-by-verdict routing, returned send-back fields, and retry behavior, see the Adjudicator tool reference. Reading an unrecognised or unreadable configuration lands on silent, deliberately: the failure a wrong guess must never cause is a finding leaving the open count because of an unreviewed agent verdict. The Adjudicator is also structurally separated from the work it judges. It holds no licensing tools, no build tools and no way to hand work off — one write channel, for its own typed verdicts. And a verdict that a finding stands must cite an entry that actually exists in that proceeding’s register: a citation of something fictional is refused rather than accepted on the seat’s word. For a conformance run, the seat’s subject is both durable finding ledgers: the obligation ledger and the type_family ledger. Each open durable row is briefed as its own finding, retaining its durable_id and locus; a type-family finding also keeps the declared expected type alongside the observed type when both were recorded. This keeps the seat from ruling on one ledger while silently dropping the other. See the endpoint reference for no_findings_basis. The Adjudicator also uses the spec-author seat’s estate_char.spec_author.no_progress_seconds bound when reconciling a live proceeding; see In-product spec author settings for the lifecycle contract. The reconcile sweep judges only when the Adjudicator’s owning runtime can be read. It asks that runtime’s hard-stop to stop a stalled turn, retries a refused request under estate_char.spec_author.stall_stop_attempts and estate_char.spec_author.stall_stop_retry_seconds, and cancels the proceeding’s handoff before writing the proceeding failed; if the handoff still reads live, the proceeding stays running for a later sweep rather than leaving two lifecycles active.

​

5. The consult agents

Some disagreements are not about the measurement — they are about what the ticket meant. Prover Consult rules on exactly one of those at a time: a proposed explanation for a difference, a competing reading of the ticket, or a claim that the check itself is malformed. It measures the dispute with read-only queries against the two named databases and returns a verdict with its probes attached. Who asks matters. A ruling is requested by an estate-working agent — the side that disputes a finding — not by the Adjudicator, which holds no way to invoke Consult and no way to hand work off. Keeping the requester and the judge apart is what stops one seat both raising and settling the same dispute. A consult ruling never licenses a finding by itself. What it does to the board is an operator setting, estate_char.consult.apply_mode: A ruling an agent or a service asked for is approved or declined through its Action Review request, opened with Ask for approval on the finding, never directly on the finding. See Roles and approvals. An unreadable configuration reads as advisory rather than the shipped default, deliberately: the failure a wrong guess must never cause is a finding leaving the open count on an agent ruling nobody ratified. Two design choices make a consult ruling worth reading:

• The requester never describes the finding. The caller brings its position and which finding it disputes; everything else — the finding’s rationale, the computed values, the check itself, the databases, the ticket — is read from the ledger. A caller that could describe the finding could describe it favourably.
• Consult is never shown whether the build passes. No verifier outcome, no benchmark score, no prior review decision reaches it. Its ruling has to be grounded in the ticket and in measurable data.

Forked requirements remain explicit throughout this loop. A finding tied to one of several candidate readings is delivered to the builder as a fork leg, with its axis, bound reading, and the rival readings’ measured standing; it is not presented as a settled expected value. If that axis changes between graded sightings while the finding is open, Consult cannot license an acceptance from the current build because re-measuring it only reproduces the reading the build was moved onto. The acceptance is escalated for human review, and the ticket wording — or a specification flag when the ticket is silent — must settle the fork. See the tool reference for the docket and fix-brief details. Consult also escalates mechanically rather than arguing indefinitely: a dispute gets a bounded number of rulings, and when the disagreement still stands, the escalation is recorded with the implementer’s values standing and every ruling attached. Above Consult sits the Adjudication Court, for disputes that need a case rather than a ruling. The court runs on a deliberate spectrum — resolve automatically, let an agent-judge decide, or send it to the human court — and the boundary is an operator’s number: estate_char.court.agent_judge_ceiling (default 50.0) is the aggregate materiality below which an agent-judge may decide a docket on its own, emitting a provisional ruling that still queues for human ratification. At or above that materiality the docket is refused and left for the human court. Raise it to let agents clear more low-stakes disputes; lower it to route more to people. When a docket’s audit status is read, the docket itself supplies the class being audited; a docket with no attached class is reported as open rather than resolving another class from the query. The Prover Consult Agent and the Court-Attorney Agent pages describe those two agents individually.

​

6. The human review surface

This is where a person’s work actually happens, and it is the one place a signature is recorded. The Prover workspace in the Genesis sidebar carries:

• Needs you and My sign-offs — the personal worklists: what is waiting on this reader, across the whole estate. The landing reads open package and rule-review queues for its visible comparisons together. Rule-review items are pair-specific: a non-retired rule without a binding for that comparison’s pair can wait there even if it is bound to another pair; see the waiting sign-offs API for the full selection rule and batch contract.
• Featured comparison rows can also split out how many unexplained differences a person accepted by ruling or one-time exception, in difference elements rather than total resolved members; grade-licensed findings are not counted as person-settled. See person_accepted_differences for its readiness and nullability semantics.
• The featured comparison follows the most recently started run that answered with it, including a re-prove that reused an existing comparison; see the comparison-list contract.
• The landing’s hidden count is per withheld comparison card, not per withheld run, and is distinct from the paginated has_more count; see the comparison-list contract.
• A family parked with Leave for now remains marked in the worklist even when later notes are added; the API reference documents the optional deferral projection for integrations.
• A Human Review workspace per comparison, with tabs for Overview, Requirements, Findings, Correspondence, Licenses & references, Runs, Coverage and Audit.
• Comparison history lists recent runs, review actions and requirements registrations, who recorded each one, and links back to conversations when the reader may open them. See the comparison history API for entry details and truncation behavior.
• Ask buttons resolve which conversation to continue when clicked; see the latest-conversation API for the ownership and fallback rules.
• For comparison title presentation and legacy behavior, see Comparison cards in chat.
• A Prover agent can also start an evidence request on a finding; see the request_evidence tool reference for its requirements, response, and sign-in-dependent Action Review flow.
• Unlicensed failed sealed checks appear as named missing requirement blockers in the comparison review population, with the check id, its measured mismatch count, compared rows, and up to three sample keys. The review population also lists the graded-side tables each failed check read in relations_read, so their object count does not need to be inferred from the display location.
• Ratifications, Court, Conventions, Governance, Attestations and Migration validations for the estate as a whole.

Migration validations also open in Human Review by validation run id, using the ?view=review&validation=<run_id> address returned by the migration tools. This is distinct from a comparison’s ?view=review&diff=<hash> address; use the returned link so the review is pinned to the exact validation run. Findings created before durable finding keys were introduced remain readable, but cannot receive a recorded diagnosis. Deep links to a comparison load that comparison directly by its diff hash; opening one does not wait for or poll the whole comparison list. The detail response resolves the source and target estates and archive status for that comparison. See the comparison detail API. Proposal actions do not hand out review links that no one can open. A comparison outside the caller’s visible scope is answered as not found. For a caller with manage_all_connections, Genesis also checks that each endpoint is attributable to an estate connection or a scan-run connection; if an endpoint has neither, the proposal is refused before anything is staged and the response identifies the snapshot’s recorded connection, when available, so an administrator can register it and re-run the comparison. The same caller-specific visibility boundary applies to supporting reads, Prover submissions, and actions: attestations, finding history, reconciliation episodes, ruling questions, notes, remediation requests, comparison-scoped review operations, court and improvement-docket reads, transition details, dossiers, proofless-grade review, spec-author run status, and live progress streams are limited to subjects in that scope. Records that cannot be placed under a visible comparison have a limited administrator exception; see [Prover result visibility] (/docs/Genesis-API/API-Reference#prover-result-visibility) for the route-level rules. Not-found responses on episode write routes are covered with the [source-contract endpoints] (/docs/Genesis-API/API-Reference#estate-source-contract-endpoints). Prover tool calls also check referenced connections, snapshots, boundaries, comparisons, execution profiles, traces, deltas, findings, and episodes against the caller’s visibility before starting the affected workflow or write. A hidden reference is answered as unknown, like an absent one. Run-list and run-detail tools return only runs visible to the caller. For the profile and baseline-trace checks on validate_migration, see its tool reference. Working through the findings means giving each open difference a diagnosis — what it actually is. The vocabulary is deliberately small, and it separates “the migration is wrong” from “the instrument is wrong”: Every review write is appended to a log rather than overwriting one, which buys three things a reviewer can rely on: each decision names its author and its moment; two reviewers working the same comparison never silently lose each other’s writes; and the current state is a pure reading of the log, so a display bug is never a data-loss event. The end of the process is the review decision — the run-level verdict on one comparison: approved, approved with exceptions, or back to awaiting review. On a deployment with authentication enabled it requires a genuine human, all three values included, because resetting a verdict is as much a statement about the run as approving it. On a stack running with authentication off it is permitted and attributed to a self-describing local identity — Roles and approvals explains why, and which acts are refused outright instead. An approved comparison can be downloaded as a signed proof report. See the proof-report API for report eligibility, contents and signing setup.

​

Rerunning checks from a report

When Appendix A has both a source and target query for at least one check, the report explains how to rerun those checks. Run each query on its respective system, match the result sets using that check’s keys, then compare the listed columns. That comparison produces the check result shown in section 2; the two query results alone do not. A rerun shows current data, which may have changed since Prover read it, and does not cover anything the report’s first-page limits say was not checked. The report also gives the check-read time separately from the structural-measurement time when those measurements were taken at different times. The report distinguishes readings set aside because the source and target tables do not line up one to one from unexplained differences. Set-aside readings are still unsettled: Prover could not compare them. Roles and approvals covers what you are attesting to when you press each button.

​

What is not part of the product

Genesis develops the Prover against a benchmark harness — a corpus of frozen data-engineering tasks used to measure whether changes to the instrument make it better or worse. That harness is engineering instrumentation, not a product feature. It is not deployed with Genesis, it is not something you configure, and nothing on these pages depends on it.

​

Where to go next

For agents and integrators. The API and tool reference — the exact calls, the response shapes, and the refusals — lives with the code, in the Genesis repository under docs/prover/. That is what an external code agent or a Genesis agent reads before it acts; these pages are the product behind it and never duplicate the calls. For operational diagnosis, the HTTP API’s Prover listing responses also expose the read-service stages that produced them through the Server-Timing response header. This is automatic and requires no Prover setting; see the API reference’s timing contract for the covered endpoints, stage names, counts, and the boundary of what the timings measure.

​

Availability

The Prover workspace is off by default and is enabled per deployment by setting features.show_estate in Genesis settings. The ruling library that the Adjudication Court and the consult modes build on is a separate opt-in, estate_char.rulings.enabled, also off by default. Everything the Prover itself needs is configuration and connections: every Prover setting is a Genesis setting, changed on the settings page or through the config API and carrying a schema default, and every database the Prover reads is a registered connection. The Prover requires nothing to be set in the deployment’s environment, and a value it needs but does not have is a stated refusal rather than a silent default. (Genesis-wide settings such as the sidebar flag above are part of the platform’s general configuration layer, which is documented with the rest of Genesis setup.)