> ## Documentation Index
> Fetch the complete documentation index at: https://docs.genesiscomputing.com/llms.txt
> Use this file to discover all available pages before exploring further.
# How a Run Works
> Every long Prover operation is a run you can watch: what the statuses mean, what provenance a result carries, and where to follow one.
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.
Anything labelled **Planned** on these pages is designed but not in the product
today. Everything else describes Genesis as it currently ships.
## 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](/docs/Genesis-API/API-Reference#get-api-estate-stimulus-preflight)
for the response fields and refusal codes.
The same contract governs machine-checkable stimulus loci: the report keeps the logical
`raw.` or `marts.` 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](/docs/Genesis-Prover/Agents-And-The-API#one-trigger-the-proof)
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](/docs/Genesis-API/API-Reference#post-api-estate-proofs) 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](/docs/Genbot-Toolkit/Additional-Tool-Groups#feed-metadata-review-tools)
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](/docs/Genbot-Toolkit/Additional-Tool-Groups#register_execution_profile).
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](/docs/Genbot-Toolkit/Additional-Tool-Groups#register_execution_profile).
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](/docs/Setup/Advanced-Settings#dbt-cloud-to-bigquery-runtime).
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](/docs/Genesis-API/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](/docs/Genesis-API/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](/docs/Genesis-API/API-Reference#post-api-estate-proofs)
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:**
| Status | It means |
| - | - |
| `running` | In progress. The run reports a heartbeat while it works. |
| `succeeded` | The work finished. **This says nothing about the verdict** — see below. |
| `refused` | **A gate declined the artifact — nothing crashed.** Produced by a proof. |
| `superseded` | An identical **grade** is already in flight under another request, which owns the answer. Produced by a proof. |
| `failed` | The work did not finish: a crash, a lost connection, a timeout. |
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](/docs/Genesis-API/API-Reference#post-api-estate-runs-run_id-cancel) and
[Databricks SQL cancellation](/docs/Genbot-Toolkit/Databricks-Action-Tools#stopping-remote-databricks-work).
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](/docs/Genesis-API/API-Reference#post-api-estate-characterize)
and [system-diff](/docs/Genesis-API/API-Reference#post-api-estate-system-diffs)
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](/docs/Genesis-API/API-Reference#estate-source-contract-endpoints) 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:
| Outcome | It means |
| - | - |
| `PASS` | A grade measured its obligations and they held. |
| `FAIL` | A grade measured the migration and the result was against it. |
| `INDETERMINATE` | A grade verified what it could but excluded a region it could not decide; it is not a plain pass. |
| `not_verified` | The run made no conformance claim, including a refusal, failure, cancellation, supersession, scan, or bare comparison. |
| `no_findings` | The run's decision was an empty finding set. |
| `sealed` | The run sealed an artifact. |
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](/docs/Genesis-API/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:
| It records | So you can answer |
| - | - |
| The commit the server was serving, and how that was determined | "Which build produced this result?" |
| A reason, when the commit genuinely cannot be determined | "Is the build identity unknown, or just unreported?" |
| The package version | "Which release is this?" |
| How the process was launched | "Was this the authenticated API, or a standalone script?" |
| When the block was stamped | "When did this run begin its life?" |
**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:` or
`user:`), `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.
A version that begins `dev.` followed by a short commit means a development build
at that commit, not a released version.
## 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](/docs/Genesis-API/API-Reference#post-api-estate-verifications).
Use the [compiled-spec qualification endpoint](/docs/Genesis-API/API-Reference#post-api-estate-spec-conformance-compiled-spec_hash-qualify)
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](/docs/Genesis-API/API-Reference#post-api-estate-spec-conformance-grade-compiled)
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 in the Genesis sidebar is the human surface: it monitors
runs and it carries the approve buttons. Its **Activity** feed and its run views
stream live progress while work is in flight, and a run can be replayed
afterwards. Runs commissioned from a mission can also be watched or replayed
from that mission's **Overview → Prover** tab; see [Prover progress in
missions](/docs/Missions/Missions-And-Tasks#prover-progress-in-missions).
Agents drive the Prover through its API and tools — registering, characterizing,
comparing, authoring, grading, proposing. People are not asked to push
micro-buttons that do micro-things; that altitude belongs to agents.
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](/docs/Genesis-Prover/Overview) — what the Prover measures and how its six
components fit together.
* [Roles and approvals](/docs/Genesis-Prover/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.