How a Run Works

Measuring a database estate, comparing two of them, authoring a specification and grading one all take minutes, not milliseconds. The Prover’s model for all of them is the same: the work is asked for, a handle comes back at once, and the handle is what everyone watches. Two operations do not work that way yet — grading an already-sealed specification, and contract verification — and they are named where that matters below. Everything else returns a handle. You will not normally start a run yourself — an agent does that. What this page covers is what you see once one is running, and what a finished run is telling you.

​

A run is the unit of work

A run is one long operation, recorded as a durable row with an id you can come back to tomorrow. Characterizations, comparisons, specification authoring, grades and adjudications all create one. The consequence that matters to an operator: a run outlives the request that started it — the browser tab that watched it, and the agent session that asked for it. Closing a tab does not stop work, and reopening finds it where it got to. Every run is readable at one address, whatever kind of work it is, so nobody needs to know which workflow produced a run in order to ask how it is doing.

​

Run ownership and connection stamps

When a run workflow names the snapshots, contracts, or execution profiles it reads, Genesis stamps the run with their connection when every input resolves to the same connection. The stamp is fixed when the run is created; later changes to an estate’s members do not move the run to a different connection. People who can see that connection can therefore find the run while it is running and after it finishes. If the inputs are absent, unknown, or resolve to more than one connection, the run has no single connection stamp. A run with no other visible subject is then available to its recorded operator or user principal and to principals with manage_all_connections. Calls that pass the authenticated submitter record that person as the run’s operator, separately from the connection used to scope the run. The run is stamped at creation, so its returned run_id can be followed immediately; no later refresh or job is needed to establish ownership.

​

Shutdown and scheduling refusals

When Genesis begins draining, it stops accepting new work and waits for every in-flight flow owned by the estate-characterization service: scans, grading, stimulus, preflight, estate re-characterization, system diffs, hardening, and fault/spec drills. The shutdown registry also drains the standalone grade_spec_conformance tool’s grading lane, which runs on a bot turn rather than through a service instance. A flow that outlives the drain timeout remains identified by its run_id in the shutdown disposition rather than being silently cancelled. Behavioral stimulus runs use the pair contract as their addressing and cleanup authority: declared physical relations and per-table island locators travel with the mission, while the legacy default is disclosed when no contract exists. Preflight exposes the contract resolution and hard-blocks stale or displaced contracts; see the stimulus API reference for the response fields and refusal codes. The same contract governs machine-checkable stimulus loci: the report keeps the logical raw.<name> or marts.<name> identity for coverage and spec silence, but reads each clone through its own declared physical relation, column spelling, and key predicate. Sealed-spec loci written in a side’s physical spelling are translated through that contract before coverage and silence are evaluated, so an off-topology pair does not silently deactivate the coverage floor; an unresolved locus remains uncheckable. Agent-driven ETL provenance is likewise per side, not a pooled statement list: contract mode records separate source and target statements and verifies the pair only when both sides pass. The run discloses each side’s attestation grade; invocation_attested is refused until its server-recorded invocation evidence is available. If a request has already allocated a run row but the service cannot schedule its flow, Genesis closes that row before propagating the scheduling error. This prevents a row from remaining running until stale-run reconciliation; callers should treat the request error as the admission failure and inspect the run row for its terminal state.

​

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 guarantee worth holding on to. 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. The agent-facing prove operation is the single trigger for this flow. It returns one proof handle and names the comparison child and, when a specification is attached, the grade child in the proof envelope. The REST and tool reference pages describe its request fields and response shape; this page focuses on how to follow the resulting run, and How agents drive the Prover explains what that trigger means for the person reading the result. Repeating the same proof is safe to retry: a finished result is reused only while the pair’s licensing remains unchanged. If a correspondence-rule binding changes after the held proof starts, the repeat recomputes the proof instead of presenting a stale answer. The proof API reference describes which pair changes invalidate reuse and the response states.

​

Pipeline migration proofs

The pipeline branch of the migration journey uses the same Prover evidence model but binds an additional execution identity: the selected source files and pipeline_checksum, the converted-code checksum, the reviewed output models, and the target runtime receipt. A successful target run is not enough by itself; the published code, deployed assets, task graph, and run evidence must also match the approved contract. Feed-rule artifacts preserve SAP identifiers as verbatim STRING fields on both sides; see the feed metadata review contract for the identifier list and related mapping checks. The journey can explicitly request two state checks. An incremental check needs successive changed-input builds for every reviewed output. A replay check runs the transform again without adding input and compares same-engine row counts, content digests, stimulus counts, and output types. These checks are opt-in. If a requested check cannot be observed, the pipeline verdict is NOT_RUN, not PASS, even when the cross-engine outputs are otherwise equivalent. For a Databricks declarative-pipeline target, the behavior replay records the deployed pipeline update, then replays its published streaming-table and materialized-view SQL in an isolated sandbox. File-reading datasets are copied from the deployed pipeline and receive the designed stimulus rows; Lakeflow’s file parsing and orchestration are not replayed. Replay queries are limited to the pipeline’s own sandbox datasets and an allowlist of pure SQL functions. Unsupported relations or functions refuse the replay before statements run. Recorded row-ingest refusals retain the originating case’s case_id, so the run can match a refusal to the same designed case on both sides. If one side refuses that case while the other accepts it, the run uses NOT_COMPARABLE, never PASS. Outputs first diverging at or after that refusal are listed as not comparable rather than as migration findings; divergences before it remain findings. Redesign the case so both sides receive the same rows before treating the output as evidence either way. Pipeline deployment, replay limitations, and state checks are included in the validation evidence. The SQL Server mssql_sql sandbox adapter requires ODBC and is unavailable for SQL Server connections made inside a Databricks App; see the mssql_sql execution-profile requirements. Repository-backed Snowflake profiles also resolve mapped relations and target-grain columns by exact spelling or a unique ASCII-case match; see the snowflake_sql execution-profile contract. Snowflake view targets can also map a rewritten view to a different relation and declare base-table inputs from other databases; see that same profile contract for the required payload fields and sandbox limits.

​

Isolated dbt Cloud-to-BigQuery runtime

When enabled, a pipeline proof can run its dbt Cloud migration against isolated, run-owned BigQuery datasets and a GCS landing resource. Genesis first records a bounded runtime lease, provisions the exact resources, and qualifies the separate lifecycle, runner, and grader identities before binding the dbt Cloud run. The grader observes the target outputs while the runner is denied access to the standing grader-control and comparison-arm datasets. A lease is not authority after it expires, and a terminal run must be proven before cleanup proceeds. The runtime is opt-in: set estate_char.behavioral.dbt_cloud_runtime_enabled to true only after configuring the dedicated Genesis Connections and identity pins described in dbt Cloud runtime settings. Cleanup recovery is independent and enabled by default, so leave estate_char.behavioral.dbt_cloud_runtime_cleanup_enabled enabled while runtime execution is in use. The cleanup owner runs once when the backend scheduler starts and then at the configured interval; it reconciles durable allocations after an interrupted provisioning, run, or shutdown and removes only resources that still match their recorded ownership and provider incarnation.

​

Grading is separately repeatable

Grading stays its own operation, 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 whole warehouses is the expensive part of the loop; re-reading a corrected specification against a comparison already on disk is not. That shortcut applies only when the characterized estate and comparison are unchanged. If a repair changes the target configuration, characterize the target again, then use prove(spec_hash=...) to create a fresh comparison and grade it; re-grading the old comparison would measure the old target structure. The structural half of a grade is exactly that re-read. The obligation half is not: each obligation is a query run against the two live databases at the moment you ask. So a grade covering both halves can describe two different moments — a photograph taken earlier, and a reading taken now — and a repair round is where those two most often disagree, because the target was changed in between. Whether they actually differ is something the grade measures rather than assumes: it reports when the photograph was taken, when the live reading was taken, and whether the two are the same moment, different moments, or something it could not establish. The finished grade exposes those intervals in structural_observed_at, structural_observed_through, obligations_read_at, and obligations_read_through. vintage_basis is same_vintage only when all four ends coincide, blended when the two tiers span different moments, single_tier when only one tier read, and vintage_unknown when the run cannot establish the comparison. A zero-obligation derivational pass does not count as a live obligation reading merely because the tier was selected. blended describes the instants, not the estates. Two reads at two moments still describe one estate when nothing wrote to it in between, so a blended grade also reads each estate’s write history again after its checks and records vintage_between_reads:

• observed_changed: a table was written between its snapshot and the checks. The caveat is a warning that names the table, because a difference reported on it may be that change rather than a defect. On Databricks Delta, the history check treats statistics and recognized maintenance operations as non-writes. It also excludes a MERGE, UPDATE, or DELETE when Delta’s operation metrics show that no rows changed, and a blind append that added zero rows. Missing or unparseable metrics do not establish that nothing changed, so the commit remains a possible write.
• confirmed_unchanged: no table on either side was written in between. There is no caveat.
• not_confirmable: an estate keeps no write history Prover can read (a SQLite file, Snowflake), or its history could not be read again. The caveat names the unconfirmed side or sides and the reason; it may also state what was confirmed on the other side. It says the result is not wrong just because the history could not confirm a change. It says nothing was seen to change only when at least one side’s history was actually read; when neither side’s history was read, it does not imply that a check took place.

When a caveat includes timestamps, it dates each side from that side’s own snapshot, alongside the obligations read time; it does not use the earlier snapshot of the pair as the start of both sides’ windows. If a side’s snapshot instant is unavailable, the caveat uses the structural observation interval instead. Reading the history again costs one write-history query per table, on blended grades only and only on an engine that keeps a history. Every run envelope also promotes the grade reading to vintage_basis, vintage_caveat and vintage_between_reads, including proof runs whose grade summary is nested under summary.summary. vintage_caveat is the sentence to place beside the verdict; on a blended grade it follows vintage_between_reads, and it also covers vintage_unknown or a basis this build does not recognize. It is null when there is nothing to qualify. An unrecognized stored basis is exposed as vintage_basis: null rather than copied through raw, so read the caveat before treating that null as “no grade reading.” Repeat grades are organised into rounds, and a round is claimed before the work starts, so asking the same question twice gets an honest answer rather than a second verdict:

• A finished round returns the result it already produced, marked as reused.
• A round still running refuses, naming the run to follow — rather than inventing a verdict nothing has decided.
• A round that errored releases, so the repeat genuinely re-grades it.

A grade is refused when its sealed specification, or any member of a sealed-spec set, relies on a clarification that a person has overturned or the recording agent has withdrawn on the owner’s word. The earlier grade is reopened, so the Prover does not answer from that run, and a new grade would rely on the retired decision again. Author the specification again without that clarification, seal the new artifact, and grade the new seal. A round’s identity can also carry the caller’s estate_coordinate: what the caller measured the estate to be at grade time. It reaches no query, but the same coordinate is the same estate and can reuse the run; a different one is measured again. Omit it when no measurement exists, and do not invent one from the round number. The grading-code version is part of every grade round’s identity as well. If the grader changes, repeating the same request starts a fresh grade rather than reusing a verdict produced by retired grading code. When a response is reused, reused_from_grade_version reports the version recorded by the reused run; it is null on a fresh grade or when the older run has no recorded version. The run envelope also exposes grade_engine_version, which identifies the grader version on the verdict carried by that envelope; see the run API reference for how both grade-version fields appear on the common envelope and their null cases.

​

When a re-grade changes approval truth

An approval binds the review population of the run it was recorded against. When a later grade becomes the comparison’s review, that binding no longer holds: the comparison is awaiting review again. The grade that caused the change reports approval_superseded with the prior decision, approver, approval timestamp, approved run, superseding run, and a sentence explaining the un-approval. The same object is promoted to the run envelope and the comparison review read, so a signed-off comparison does not look approved merely because its earlier decision remains in the event history. null means the grade superseded no approval. The read-side contract is documented in the API reference.

​

Relocation proofs bind once

When a migration moves relations between schemas, a proof can declare the relations that must end up on the target with declared_relations. These are schema-qualified target coordinates, and the request must name an explicit round_n plus exact source and target snapshot ids. The first round whose target produces every declared relation binds the proof to that target snapshot. Later rounds reuse the binding rather than re-snapshotting the target, so the same repair is always graded against the same estate. If the target does not hold all declared relations yet, that round fails and records the missing names; it is not held for a later retry. Fact 1 is satisfied when the source snapshot holds each declared relation or, for a greenfield build whose read-only source does not hold the mart, the attached sealed spec declares it in a structural item’s locus. A relation-level locus and a column-level locus both declare the owning relation. The binding records premise_basis as source_snapshot or spec, so the evidence used to bind remains visible on later reused rounds. Relations covered by neither the source snapshot nor the sealed spec refuse with stop_reason: "source_absent"; a spec-backed refusal identifies the undeclared names. The declared relations must still be absent from the pre-build target baseline, otherwise the relocation premise is refused. See the prove request contract for the request fields, response details, and premise lookup window.

​

Reading a run’s status

Genesis normalizes run status into one vocabulary, so a run recorded under an older spelling still reads in today’s words. A handle returned without a run row has no envelope to supply its status. In that case the stored spelling is normalized directly: error reads as failed, while a spelling the status map does not recognize is returned unchanged. What you will see on a run today: The vocabulary also includes queued (accepted, not started) and cancelled (stopped deliberately). The estate run cancel endpoint can produce cancelled for a non-terminal run. For a spec-author seat, cancellation also asks the runtime to stop the seat’s turn; if a tool call is polling a Databricks SQL statement, it requests statement cancellation on a best-effort basis. Characterization, scan, system-diff, and stimulus work are cancelled on the run row only and may finish afterward; late results do not replace the cancellation. See the cancel endpoint and Databricks SQL cancellation. A proof can finish as refused when a gate declines what it was given — a seal that does not verify, a grading tier nothing defines, a connection the deployment does not hold — or as superseded when the grade it needs is already in flight under another request; both are terminal answers to interpret, not crashes to retry blindly. Re-submitting a proof produces neither — it is answered by the proof that already holds the answer, marked as reused.

​

Terminal error attribution

Runs ending failed, refused, or cancelled carry summary.error_basis beside summary.error. writer_reported means the terminal write supplied a non-empty error, or stated why it stopped in stop_reason_detail or stop_reason; when the writer supplied only that stop reason, Genesis copies it into summary.error. sweep_reported means reconciliation closed the row and reported the measured silence; no_reason_supplied means neither an error nor a stated stop reason was supplied. The last case is explicit rather than guessed. Successful and superseded runs do not carry this failure-only field. Terminal attribution is retained when work that outlives the terminal write publishes a later progress summary. The terminal status, error, error_type, next, and any cancel identity or reason remain readable; a later progress write does not make a terminal run look like an unexplained crash. A late completion is recorded beside that attribution rather than replacing it. The same one-submission rule applies before a proof is involved. A duplicate characterization while the first scan is queued or running follows that scan’s run_id instead of sealing a second snapshot; after it finishes, a new characterization is correct because it measures a later instant. A duplicate system diff follows the existing comparison even while it is still running, but a distinct comparison question on the same pair remains a resource conflict. After a comparison finishes, Genesis reuses it only while the pair’s correspondence-rule bindings have not moved since that run started. A ratification, pair-scoped review, or revocation after the run starts makes a repeat submit create a fresh comparison, so the older result cannot conceal a newly licensed rename. The API describes the request headers and reused_basis response field in the characterization and system-diff contracts. Long-running work can outlive the liveness window. The shared estate_char.reconcile.stale_after_seconds setting defaults to 2400 seconds, and a heartbeat keeps a running row alive while the driver is active. If reconciliation closes the row first, a later proof completion does not turn that terminal row into succeeded; the completion is retained in the run summary as a late completion. See the run API reference for the fields to read. Reaping does not erase the proof’s last measured state. The reconcile record is added under summary.reaper, including when the row was reaped and which liveness threshold was applied, while the existing summary keys remain available to the reader. The reaper closes only a row that is still running, so a proof that finishes during the sweep keeps its own terminal result.

​

The status is never the verdict

succeeded means the run finished. Whether the migration passed, whether the specification was met, whether the finding was upheld — those are separate, and they live in the run’s decision axis rather than in its status. Every terminal run now publishes that decision as top-level outcome, beside status, from this closed vocabulary: For a grade, not_verified is also the grade’s fail-closed word when it could not decide its obligations. When the grade’s verdict block instead lists one or more definite blocking findings, the grade did measure the migration and the run’s outcome is FAIL; an empty blocking list remains not_verified. This keeps a measured negative result distinct from a grade that could not evaluate its obligations. The field is null while the run is still live. Terminal records that predate the field are served with the same derived outcome from their stored status and summary, so callers can use the same vocabulary while the store backfill catches up. A grade that ran cleanly and concluded that the delivered change does not meet its specification is a succeeded run with a failing verdict, not a failed run. Read the status to know whether to keep waiting; read outcome to know what was decided.

​

Listing runs without the evidence payload

Use GET /api/estate/runs?shape=slim when a status surface needs recent run identity, liveness, and summary scalars without each run’s evidence document. The service reads those five slim scalars from dedicated run columns, so a page stays bounded even when the stored summaries are large. During startup backfill, or on a database dialect that cannot read JSON scalars directly, a row may instead report summary_shape: "slim_json_fallback"; it has the same values but the service had to read its summary document. The API reference defines the complete list and paging contract; use GET /api/estate/runs/{run_id} when the evidence itself is needed. The dashboard shell uses GET /api/estate/runs?shape=card for its initial run list. This keeps the listing’s identity, status, progress, and small summary values while leaving report documents such as items, canvas, drift, and the stimulus ledger for the single-run request. The card is normally served from its persisted projection; during startup backfill, a row that still comes from its evidence document is marked summary_shape: "card_from_document". The card also omits platform_attribution; its platform accounting remains in classification.platform_licensed and classification.platform_rule_ids; classification.model_licensed distinguishes the subset accounted for by a declared target model. The API reference defines these classification fields. When a reader opens a run, the dashboard can request the detail row separately; shape=report returns the report documents without the raw per-object measurement payloads. card also caps a top-level summary string at 2,000 characters and marks the value as truncated, so a malformed or unusually large error message cannot expand the whole listing. The notice points to GET /api/estate/runs/{run_id} for the complete value; the API reference defines the exact dropped fields and the summary_shape: "card" marker. For grades that measured waiting-rule coverage, classification.drift_would_be_licensed counts only the drift findings that an unratified correspondence rule could license if approved; it is not a count of all drift or of every pending ruling. The accompanying classification.drift_would_be_licensed_by groups that count by rule_ids and count, largest groups first, and lists at most 100 groups while keeping the total exact. Its rule ids come from pi: tags; platform: tags do not create a group. The same fields appear under reclassification.after. They are absent on older grades and during backfill, which means unknown rather than zero. Startup backfills for run cards, terminal outcomes, finding-family signatures, and snapshot content fingerprints write each batch with set-based UPDATE statements, rather than one update per row or executemany (which the Snowflake connector runs row-by-row for non-inserts). Statements are split to stay within parameter and bound-value size limits. This reduces startup wait on large stores without changing what reads return; rows not yet backfilled continue to use their document or object-derived fallback. In SQLAlchemy metadata mode, Prover store tables are created automatically on the first session for each platform engine, so the run list needs no separate table setup. When the request includes estate_id, the listing includes a proof if that estate is either the estate under which the proof was submitted or the estate it compared as its target. The filter is applied before pagination, so older proofs still appear on the target estate’s page. runs_without_estate counts only runs with neither a submitting estate nor a resolved target estate; those runs cannot appear on any estate-filtered page. A target that cannot be resolved to one estate is not assigned to an estate page.

​

Provenance: which build, which rules, which database

A Prover result is evidence, and evidence that cannot say where it came from is worth very little. Every run carries a provenance block, stamped once when the run is created, in its own field — not folded into the summary, where later progress writes would erase it. On every run, provenance records the environment the result was produced in: On specification-authoring runs, provenance additionally records the surface that drove the run, the principal it acted as, the authenticated operator, the escalation mode, and — importantly — the constitution the authoring was pinned to, by name, version and content hash. That is what lets a reviewer say which doctrine a specification was written under, months later. seat_settings_defaulted lists which of interpretation_policy and authoring_tooling the deployment default decided; an empty list means the recorded settings were not defaulted, while an absent field means no seat setting was recorded. It appears in both the seat run’s and the sealed specification’s provenance. When a run summary carries seat_settings_inherited, run reads project those settings onto the run’s provenance and omit inherited keys from seat_settings_defaulted in both the provenance and summary: the default did not decide them. This read-time view does not rewrite the stored run row. Proof, comparison, and characterization runs retain the caller-side provenance needed to distinguish an agent submission from a human REST submission. When present, the block records surface ("tool" or "rest"), principal (agent:<bot_id> or user:<user_id>), submitted_by, and thread_id; blank values are omitted rather than stored as empty strings. The principal identifies who the run acts as, while submitted_by identifies the authenticated user who submitted it. An agent therefore does not gain the user’s connection reach by being recorded as a separate principal; its result visibility is still imputed from the submitting user’s connections. Frozen measurement records use the same distinction: attested_by records the claim about who asserted that a non-PostgreSQL estate was quiet, while the frozen record’s created_by records the signed-in user who created the record. A turn without a signed-in user is recorded as unattributed; do not report the attester as the record author. A proof that carries a specification records the constitution used by the grading build on both the proof and its child grade; a comparison-only proof records an explicit constitution basis saying it was not bound to one. On a compiled-spec grade, that constitution is the doctrine the grading process ran under, not the constitution under which the persisted artifact was authored. Two choices you will notice when reading provenance:

• A field nobody measured is omitted, not filled in. A stated absence is information; an invented value is not.
• Runs created before provenance stamping existed are not back-filled. They carry an explicit reason saying so. A back-filled block would be indistinguishable from a measured one, which would make every block less trustworthy — so the older rows admit the gap instead.

The build identity is also directly readable from the deployment’s version endpoint, which reports the commit the server is serving, where that came from, and — when it genuinely cannot be determined — a reason rather than a placeholder that reads like an answer.

​

Waiting instead of watching

Polling a handle is the normal way to follow a run, and it is always available. Inside a Genesis thread, the agent-facing Prover tools characterize, compare, prove, and grade default to notify=true: the thread that started the work is told when the run reaches a terminal status. The wake arrives on the next tool result if the agent is still in a turn, or as a new turn once the thread is idle, and carries the same run handle a poll would return. adjudicate uses the same default and sends the proceeding readback that repeating adjudicate would return. This removes the need for a model-turn poll while preserving the existing handle and status contract. Set notify=false when an agent should check the run itself. Calls made without a Genesis thread, including REST API calls, are not armed and continue to use the returned poll link. notify is independent of wait_seconds: an inline wait may expire while the run continues, and an armed thread is still told when the run ends. A caller that would rather block than poll can ask for a bounded wait when it starts the work. Two properties of that wait concern an operator:

• The ceiling is yours, not the caller’s. estate_char.api.max_wait_seconds (default 300, bounded 1–3600) caps what any caller may ask for. A larger request is clamped rather than refused, and the clamp is disclosed on the response, so a caller can tell “the operator’s bound stopped me” from “my own wait ran out”.
• A wait running out never stops the work. The run continues; only the caller stopped waiting. The ceiling bounds how long a request holds a connection, never how long a run may take.

Three operations accept such a wait on the current build — proving a pair, the spec-author seat, and specification compilation. The agent-facing prover_tools.grade operation also returns a handle immediately and accepts wait_seconds; the REST POST /api/estate/spec-conformance/grade-compiled endpoint remains synchronous for callers that want the verdict in its response. Qualification of an already-sealed specification is synchronous and has no run to poll: it derives relation names from the sealed artifact and a named connection without invoking an author. Contract verification also remains synchronous. If the connection store cannot be read while verification checks its registered bindings, the request returns 503 rather than treating the registry as empty; see the verification API reference. Use the compiled-spec qualification endpoint when a sealed artifact only needs deterministic relation-name qualification. It returns a new child spec_hash and a receipt of the changed fields; it refuses rather than reseals if anything outside relation fields would move. Use a repair round when new instrument facts need model-backed re-compilation instead. Declaring a specification’s migration shape works the same way and is likewise synchronous with no author invoked: POST /api/estate/spec-conformance/compiled/{spec_hash}/declare-shape. The structural tier asks whether the target came out different from the source (must_differ — a change specification) or identical to it (must_match — a lift-and-shift, or the landing hop of a layered move). Those score the same estate as opposite verdicts, so a specification declaring neither has its structural items graded indeterminate with a basis naming the missing declaration rather than guessing. Every specification sealed before the declaration existed is in that state; this endpoint writes it onto every structural item and returns a new child spec_hash to grade with. When a grade fails an obligation, the Adjudicator receives the attributed and eligible unattributed failures in the persisted finding population. The grade response details explain the foreign-catalog exception and how to distinguish those populations before opening adjudication. A proof continues after the caller’s wait expires; its poll link is how to follow it to a terminal status.

​

Where to watch

The Prover workspace is off by default and opts in per deployment by setting features.show_estate in Genesis settings. When it is off, the Prover itself is unaffected — only the sidebar entry is hidden. Live progress is streamed over a dedicated channel that can follow one run or every run of a migration pair. It sends a catch-up snapshot on connect and then forward-only progress, so a tab that reconnects mid-run does not lose its place.

​

Next

• Overview — what the Prover measures and how its six components fit together.
• Roles and approvals — what lands in front of you and what each button attests to.

For agents and integrators. The exact calls, response shapes and refusals live with the code, in the Genesis repository under docs/prover/ — the API reference for agents. This page is the concept behind it and deliberately does not restate the calls.