How Agents Drive the Prover

Almost nothing in the Prover is started by a person. An agent registers the estates, measures them, authors the specification, submits the proof and follows it to the end. What a person does is read what came back, and sign — or not. This page is the human side of that arrangement: what an agent will already have done by the time something appears in front of you, and what the words on a run mean when you read them. It explains the vocabulary, not the wire. The calls themselves, and the exact shapes they answer with, live in the Genesis repository under docs/prover/, which this page links down to rather than repeating. On hosted deployments, the Prover’s estate live-progress WebSocket follows the deployment’s hosted identity boundary. A signed hosted assertion must resolve to an active explicit identity link for the configured tenant and installation before the channel is admitted; a later expiry or revocation closes the channel. The API Reference documents the connection parameters and close behavior.

​

The division of labour

An unattended agent turn can run the proof loop, recover from it, and call a bounded set of read-only Prover verbs under its view_connections allowlist. For a user-started mission, Prover reads use the mission originator’s visibility where that originator can be verified; cancel_run remains scoped to the originating conversation. The exact read verbs, caller-scoped visibility, authority limits, exclusions, and refusal behavior are documented in the Prover toolkit reference. Estate setup is agent-driven as well as estate monitoring. An agent can register an estate, edit its definition, attach git code assets, clone those repositories, and derive their transform lineage before it characterizes the estate. The exact parameters, replacement rules, and force behavior are in the Prover toolkit reference. A run an agent started is an ordinary run: same address, same words, nothing marked differently because a machine asked for it. What can tell you an agent was involved is its provenance — which surface the work arrived on, which identity it acted as, and which authenticated person was behind it. How much of that a given run carries depends on the surface that started it. A specification-authoring run records all of it today, along with the doctrine it was pinned to; How a run works sets out provenance in full, including which run types carry which part of it on the current build. A grade started through the prover_tools group records surface: "tool" in its provenance. That is the audit distinction for a direct agent tool call; it is not a different grading path or a different verdict.

​

A clean table is not yet a proven pipeline

The Prover now separates what is in the target from what produced it. A clean comparison still answers whether the measured rows and structure agree; its additive writer_attribution summary answers whether every target relation was attributed to a re-runnable mechanism. Read the per-relation writer_readings when the summary is not fully attributed. An unmeasured writer reading is not a failure of the table comparison, but it does mean the result cannot be read as evidence that a pipeline produced that relation. The reading comes from the target engine’s own write history, and Databricks is the only one of the fourteen supported dialects that exposes one. For a Databricks reading of unattributable, the Prover can also use Genesis’s own completed Flow-step record: when the step wrote the same relation on a connection bound to the target snapshot, and the engine’s last-write time falls within the step’s run (with two minutes of clock skew), the reading becomes attributed with mechanism: pipeline and includes flow_run. On every other engine each relation reads unmeasured carrying that engine’s own reason, and the summary’s basis then says so rather than describing a hand patch nothing measured — so read basis, not the qualifier alone, before reporting what produced a customer’s tables. For a specification that requires a particular producer, use a written_by obligation; it grades the target relation’s write history and accepts only the declared job, notebook, or pipeline mechanisms. For a pipeline demand, it uses the same completed Flow-step attribution described above: where the target engine exposes per-relation write history, a matching flow_run can attribute a write that history names even when it does not name the pipeline. A Flow-run record cannot substitute for an engine with no write history; finalization refuses such a written_by obligation (refusal details). Writer history is necessary evidence, not sufficient proof: a patched table can still be followed by a successful rerun. The reproduce_artifact tool is the sufficient check; it runs the declared SQL artifact in a utility estate and reports whether its output reproduces the live relation. Its REST contract is POST /api/estate/estates/{estate_id}/artifact-reproduction.

​

Discover before you trigger

When an agent starts with identifiers from the estate surface rather than snapshot or run ids, it can discover the existing work before launching anything new. The find_proofs tool should come first when the question is whether a migration has already been checked: it accepts the names, connection references, or database names a person uses and returns the proof of record with its current review decision; for the exact stands values, including the unmeasured null case and the rule to treat only true as signed off, see the Prover toolkit reference. If a new proof is needed, list_snapshots resolves an estate id to its scan timeline and exposes the snapshot ids that prove and compare require. Its rows distinguish scans bound by a scan event from snapshots matched by the estate’s registered scope; the latter are inferences, not asserted bindings. If a recorded decision no longer binds to the comparison’s current population, the proof still reports that decision with a measured non-standing basis rather than making it look as though nobody ever decided. Exception standing is based on the final state in the review log, so an exception that was retracted and then re-approved does not leave the approval withdrawn. A re-diagnosis is different: it withdraws the run decision and the basis names the finding and time that caused the comparison to await review again. See the Prover toolkit reference for the exact review_decision fields, boundary-group resolution, non-asserting resolution contract, and the unattributed_snapshots disclosure for snapshots withheld from proof pairs. If data.resolution.asserted is false, choose one candidate with active: true and ask again; do not relay the empty pairs list as proof that no migration was proved. The proof rows also hand over the Human Review page that records the decision; use review_url and review_url_basis as documented in the toolkit reference rather than constructing the address yourself. Relay review_url exactly as returned, including the whole hash; use review_path exactly as returned only when review_url is null. Without a public base URL, a link may use the Genesis address the conversation came from or this server’s local dashboard address; use it only in the context named by its basis. When no usable address is available, review_path carries the page’s address relative to the Genesis dashboard. Do not relay the deployment setting named by review_url_basis to the person signing off. A standing run decision is not the same as whether a comparison is Verified or needs a sign-off; use read_comparison and its data.review.nothing_to_decide field for that question, as described in the tool reference. The list_runs tool shows recent work newest first, so an agent can check whether a characterization, comparison, or other run is already in progress or complete after a bounded wait expires. The same cross-conversation visibility boundary applies to get_run and runs submitted with notify=false; see the tool reference. Run listings and run-backed reads follow the caller-specific estate and comparison visibility in Prover result visibility. The same visibility governs other Prover reads and actions, including rulings on proofless-grade reviews. See the tool-specific episode and court behavior. Pass estate_id when the question is about one named estate; it matches proofs submitted under that estate or compared against it as the target, before pagination. The response’s runs_without_estate count discloses runs with neither a submitting estate nor a resolved target estate. See how runs are listed for the estate-filtering edge cases. That feed is a page, not the whole ledger: inspect has_more and pass its opaque next_cursor to continue through older runs. These are read-only discovery steps; they do not start a scan or another proof. For scan-time row counts, use read_snapshot rather than counting against the live connection; its full response contract is in the toolkit reference. A scan summary’s schemas_scanned_count and schemas_discovered_count count schemas, not tables. schemas_discovered_count is null when a pinned scope remains explicit_subset. With estate_char.characterization.full_source_default enabled (default true), a pin naming exactly the schemas included by the full-source scope is recorded as full-source instead. That whole-estate pin keeps the same boundary as an unpinned full-source scan, so it does not re-key findings. If full-source scanning is disabled or schema discovery fails, the pin remains an explicit_subset. The earlier scanned_count and discovered_count spellings remain for one release; they also count schemas, but discovered_count counts a pinned list as discovered. For completed comparison history, list_comparison_events provides a bounded, newest-first discovery feed; inspect its truncated result before assuming all comparisons are present. Its response shape and drill-down route are defined in the Prover toolkit reference and estate API reference. See the estate API reference for the rule that keeps customer proofs out of curated Estate workspace labels. The proof also discloses estate movement separately from population standing: read source_moved_since_approval and target_moved_since_approval to see whether either estate has CHANGED since the snapshot the approval was recorded against. A change does not withdraw the approval; it tells the reader that the approval concerns an older estate reading. count counts later readings whose measured content differs from the bound one, or could not be compared with it — not later readings, because a re-scan of an untouched estate still writes a new snapshot row; readings_since carries that raw number for an audit answer. The movement blocks are always present and carry a basis, so no_standing_approval, no_snapshot_bound, and approved_snapshot_absent are not silently presented as a clean count of zero, and no_content_change names an estate that was re-read and measured the same. See the toolkit reference for the exact block fields and basis vocabulary. For a new scan, characterize(estate_id=...) binds the work to the registered estate; the complete parameter and refusal contract is documented in the Prover toolkit reference. Direct scans accept every dialect registered by the Prover, including SQLite and the other engines listed in that toolkit reference. When the schema picker is populated for a SQLite estate, it lists the databases attached to that connection; the temp database is excluded. See the estate API reference for the discovery contract.

​

One trigger: the proof

A proof is a comparison, optionally graded against a sealed specification — and it is one call either way. The agent brings the two sides; if it also holds a sealed specification, it names it, and the same proof grades that specification against the comparison it just produced. When a table is specified in parts, compiled-spec grading also accepts a set of two or more sealed specification hashes. The parts are graded as one result: each column is owned by the member that covers it, overlaps and conflicting claims are reported in spec_set, and only columns no member covers remain drift. The exact request, response, conflict rules, and warehouse-work implications are in the compiled-spec grade API reference. When the structural tier finishes, read summary.spec_set_reading to relay the same members, seals, overlaps, conflicts, and uncovered differences the review card shows. That single trigger is the point. The proof owns its children and names them, so nothing is hidden and no identifier has to be threaded between calls by hand — and the grade is bound to the comparison this proof produced, because a verdict attributed to the wrong comparison is worse than no verdict. The proof is also the notification owner: a comparison or grade child that finishes while its proof is still running is reported through the proof’s terminal wake, not as a second thread notice. The Prover toolkit reference covers the bounded form used when that wake enters a mailbox. The trigger also accepts row_identity when the engines do not declare a business key; a key position may be a coalesce expression when the key is carried across more than one source column. See the proof request contract for concat positions. On a spec_hash proof that is not using a relocation premise, omission of case_insensitive_object_names or row_identity inherits that value from the estate pair’s latest successful proof of the same spec. The pair is the resolved source and target, not the caller identity; an explicit request value always wins. The proof records the requested and effective values in summary.proof_addressing, with a source of request, inherited, or default for each value. When case policy was left to the deployment default, the completed comparison records the resolved value with source config, so a later proof keeps the policy actually used rather than following a changed configuration. The record also keeps case_insensitive_object_names_origin: "config". When a re-prove omits that policy and the inherited value differs from the deployment’s current setting, proof_addressing.differs_from_config records compared_under and configured_now; the pair keeps its prior policy, and basis explains that the caller must pass a value to change it. There are two exceptions to straightforward inheritance. A proof retried with the same client_request_id and the same requested values reuses that submission’s addressing, even if the pair has since had another successful proof. Also, if a later proof was refused with row_identity_unusable when comparing under the prior proof’s row identity, that row identity is not inherited again; omit it to use the engine-declared basis. The case policy still inherits in this case. proof_addressing records prior_proof_run_id, differs_from_prior, row_identity_refused_since_prior, and a basis sentence explaining the decision. When a declared key repeats, the refusal’s remedial call can suggest a more useful identity instead of only telling the caller to remove it: add columns that distinguish the repeated rows, use a first-non-NULL coalesce key, or provide separate source and target key terms when the two sides identify the object differently. The exact tool argument examples are in the Prover toolkit reference. When a declared key cannot be read on one side, that is different from a key the estate read and rejected as unusable. A terminal proof refusal reports the distinction in summary.unverifiable_objects, with the object, side, and probe cause; its next keeps that declaration and tells the caller to make the estate readable as the submitting identity or omit the declaration if it cannot be fixed. A key verified as unusable is listed in summary.unusable_objects and removed from the remedial call. The synchronous comparison endpoint returns the same decision in its 400 payload. During grading, invariant reads and grain probes use the registered query transport for the bound connection. An estate exposed through a Connections API transport can therefore be graded even when the legacy DatabaseConnector does not own that connection; the API reference defines the binding fields and validation. For the shared-connection catalog rule for target-side invariants, including the one-database-per-connection exception, see the API reference. That reference also documents the admission-time 400 for a one-database engine given a catalog other than the side’s recorded snapshot database. Attaching a sealed specification is an authority act: it takes the same authority a person needs to ratify, and an agent without it is refused before anything runs — not even the comparison, so nobody pays for the expensive half of a proof that could never have been finished. Roles and approvals covers that permission. The proof’s tier-selection admission rule and its terminal-run remedy are defined in the API reference.

​

Comparison cards in chat

prove, compare, get_run for a proof or comparison, and read_comparison carry a top-level presented block for the chat surface. The dashboard renders it as one comparison card rather than asking the agent’s prose to reproduce the result. Other answers carry presented: null; it is not part of data. When a comparison was created with a business title, the Prover landing and Human Review use it as the headline and retain the technical source → target label beneath; legacy comparisons without one keep their existing technical headline. The API’s comparison-list field is documented in the API reference. When Judge now starts a new no-spec comparison from a spec-titled card, see the API title rule for how the submitted title is stamped. See also API title handling for no-spec reuse. Separately, read_comparison may return data.timing_rescan_evidence when the comparison has timing-cause abstentions. Treat it as evidence, not a revised verdict; see the read_comparison guidance for its interpretation and limits, including how it places re-scans across changed observation boundaries. For a large reply, check the preview for this evidence before reading spilled output; the tool guidance describes the serialization order and its truncation limit. For a comparison-only compare response, data.with_a_sealed_spec is present when the caller should use a sealed spec for grading. It tells the agent to call prove(spec_hash=...) with the same pair for one comparison-and-grade, or to call grade(spec_hash=..., diff_hash=...) when a separate grade is needed; relay that guidance rather than treating the comparison as already graded. The target-model recompute and its cost are described in when a grade names a comparison made without its spec. The card starts as Comparison running and is updated in place when a poll or wake reports the same run. A completed card carries the explained (licensed), unexplained (unlicensed), and could-not-be-measured (indeterminate) counts, plus the count of reads that could not be read (errored) when that value is not zero. When the run withheld readings because the target was Data Vault-shaped, or because no objects paired on either side without a declared model, the card carries the guidance needed to declare the mapping and may carry withheldUnlicensed and withheldIndeterminate; each zero published count uses the headline format in the comparison guidance. That guidance also explains how withheld readings differ from unexplained and undecided readings. A read_comparison card can be the newest measured payoff verdict in any shape, including scope, when its errored count is measured; an unknown count does not qualify. See the read_comparison tool guidance for how that count is supplied for scope. When the review population also carries nothing_compared: true and no spec_grade, the approval action is unavailable even if its members are all accounted for. Follow nothing_compared_cause: declare the mapping for undeclared_target_shape, check that the target snapshot matches the declared mapping and re-prove for declared_mapping_matched_zero, rerun when the matched count is unavailable, or re-prove with a schema_map for matched_zero. The approval refusal and review-card readiness use the same cause, so the remedy shown to the person is consistent. A reshaped build — one whose spec derives the target from the source, so no table pairs — is judged by its spec grade instead: when the population carries spec_grade, a verified grade makes the comparison approvable once nothing is open, and an unverified one is refused with spec_grade_not_verified, naming the grade’s blockers. See the review-population API fields. When a verified person’s standing approvals cover every item that kept the comparison off Verified, the card reads Verified, names the approved-item count, and identifies approvers using their user display names when the server provides them. If a name is unavailable, it uses the part of the recorded address before @ (or the recorded label when it is not an address); the full address appears on hover rather than on the card face. No separate run decision is required; the comparison can read Verified without a run-level sign-off. A person’s explicit reset to awaiting_review remains a “not approved” and keeps the card off Verified until a verified approval replaces it. This reviewed outcome does not change the spec grade shown beside it; a grade still running cannot be lifted to green. The outcome is withheld while an open behavioral catch remains. The API’s person_acceptance conditions and item details are in the comparison review response. A partial seal keeps its grade below Verified: the card reads Partially specified · N clauses open (singular clause at 1), not Verified or “verified with unresolved scope.” A grade whose seal kind cannot be read instead says Seal state unknown — details on the review page; neither state is green. envelope.report_this includes the partial label and names the open clause ids. The Prover review view lists each open clause’s reason and remedy, including who must act; the grade run’s summary.open_clauses carries the full clause, evidence and remedy. When the remedy belongs to the owner or operator, it also carries the seat’s recommended_answer; that recommendation does not itself close the clause. Legacy run rows may have no stored seal field; the compiled-grade API reference documents how Genesis assigns their reading. A clause accounted for by the comparison of its objects (accounted_by: "scope") is decided by each grade, not by registration. The grade proves it only when every named object was measured on both sides and the comparison found it clean (match or licensed); a file-measured dataset must match its landing file by file. Otherwise the clause is held open for that grade, including when a side was not measured or the comparison errored. A grade that compared no objects holds every such clause open. The grade view’s clauses_proven_by_comparison lists the per-object result. An unproven clause appears in the review as not proven by this comparison, with a remeasure remedy; a person may accept it only if it is out of scope. See register_clause_accounting for how to record this disposition. Each clause is a separate open evidence-gap member. A person may accept a clause as out of scope in review; that acceptance can let the comparison read Verified once every blocker is accounted for, but it does not change the amber grade. An agent must not accept a clause or ask a person to accept one whose remedy names the proposer. For proposer-owned clauses, follow the remedy and commission a follow-up seal with repair_of=<partial spec hash>; for remedies naming the owner or operator, ask that person once using the seat’s evidence and recommended answer. See the tool reference for the recommendation requirement. For selected-check requests, see the grade tool reference. A grade of only selected checks is distinct from a partial seal: its result reads Partial grade · N of M checks and carries graded_check_ids and spec_check_count to identify what was graded. In chat, the card reads Partial grade, never Verified or green; the card does not show those counts. See the grade tool reference for selecting checks. For a running proof, the card also names the estate pair recorded on its run row, so the chat can open the live comparison before a diff exists. When read_comparison presents the completed comparison from that proof, its presented.proof_run_id names the proof run; chat uses it to update the original running card rather than leave a second card beside the verdict. The read_comparison read cost for that bridge is described in the read_comparison tool guidance. See the Foundry verification guide for how an asynchronous migration proof is returned and followed. In the chat card, the newest comparison with a view opens the embedded Prover theater while its run is active. It follows the proof into the comparison and stays mounted as the result arrives; once settled, the same card shows its source-and-target Venn and, when green, a migration pass score above the picture. The score reports object matches and behavior checks available in the conversation; Certified requires the comparison to be green, all counted objects to match, and every behavior check that ran to pass. If the theater is unavailable, a static Venn is used when comparison evidence is available. Readers who request reduced motion see the static Venn rather than the live theater. The score’s Open in Prover link opens the detailed stage, so the card does not repeat its Detailed view link. The theater’s snapshot picture uses the inventory shape of the snapshot detail API, so it loads object and column names without loading the full characterization document; see the snapshot endpoint reference. When object_presence.not_built names a declared derived target the build lacks, the Venn shows it separately as Derived table(s) not built; the list is outside the source-object counts, and any entry prevents the payoff from showing green. While the live theater is shown, its caption names the pair and its picture gives the count after assumptions, so the card omits those duplicate lines. On a green comparison, the theater’s verdict sentence also replaces the card’s verdict bar and count list; a comparison that needs attention keeps those counts on the card. When the theater falls back to the static Venn, the card returns to its own pair and verdict display, with the assumptions count and disclosure when available. When the completed comparison records assumptions, its headline uses issues_not_covered_by_assumption, the count after those assumptions. If the assumptions list is non-empty, the count carries an asterisk; select it to open the assumption list and inspect each assumption’s statement, scope, basis, source, and covered readings. From that list, a person can choose Withdraw for this pair and confirm to stop the Prover relying on that assumption for the comparison card’s estate pair; the withdrawal affects later comparisons, while this stored comparison keeps its verdict. An empty list leaves the count unstarred, while a missing list leaves the after-assumptions count undisclosed rather than treating it as zero. The same disclosure is available from the comparison’s review and detail views. When a comparison card would exceed the presentation size limit, Genesis keeps the card by trying smaller assumption disclosures: it first omits assumption evidence and source, then clips long statements to one line, and finally omits the card’s assumption list while retaining the after-assumptions count. The comparison review page continues to show the complete assumption records. It also reports what changed since the previous comparison of the pair. A first comparison says so; when unexplained findings decrease, the change line counts the ratified rules that account for that decrease rather than printing their ids. When it attributes a decrease to behavior proofs, it gives the proof count rather than printing run ids. If the indeterminate count rises during that shrink, the card does not claim that portion was explained: it says N unexplained not measured this time and shows undetermined before → now. A partly measured shrink reports the measured decrease and its rule attribution separately, then adds N more not measured this time. When the recorded withholding differs between the comparisons, their unexplained counts cover different populations: the line describes the withholding change and shows both counts without claiming a shrink or growth. If one side has no recorded withholding count, it says so rather than treating the count as zero. Comparison history follows what the scans compare, not just their connections. Bound scans remain grouped by their estate; an unbound scan joins a database’s sole boundary group only when that estate’s scope admits the scan. If no estate or boundary group identifies a scan of a known database, its requested schema pin distinguishes its history: different explicit schema subsets on one database have separate histories, repeated scans of the same subset stay together, and full-source scans remain grouped by database. Within a history, changing the object or schema map does not start a new pair. The previous comparison can come from another conversation. When it is from another conversation, the card says so and includes the conversation id when available. If the prior conversation was not recorded, the card says so; if its relation to the current conversation is unknown, the card names it when possible and says its relation is unknown. It omits the line when the prior comparison is from this conversation or the server sends no conversation metadata. When two comparisons differ only in declared scope and otherwise observe the same databases in the same way, they share finding identity. Changing scope alone therefore does not re-key findings for objects that remain covered. If a later scope does not cover an open finding’s object, that comparison did not measure it and does not resolve it. Comparison-linked writes from grading, stimulus rounds, source-drift reconciliation, and dossier capture use the pair identity recorded on the diff when available, so findings remain on that key after a scope change. Older diff records without a recorded pair identity use their observed boundary pair. The identity class includes each comparison’s observed boundary pair and its recorded identity pair when those differ. If the class later files under another pair, findings left open under the former pair remain there; they are not moved or closed. The findings API labels these rows with superseded_by_pair to identify the pair now receiving new filings; see the estate API reference. Earlier rulings recorded under another scope can reappear in the current proceeding’s prior_verdicts; the fetch_adjudication_materials contract defines the aliased_from field that identifies the key holding such a ruling. When a completed run is measured against a named specification, its finished notice also states what clarification records that specification relies on and who recorded them. That sentence comes from the sealed provenance, not from the ticket’s wording; a seal created before clarification records existed reports that clarification provenance is unknown. A finished proof or comparison notice also names its review page when one is available. When the notice gives both a markdown link and a plain dashboard path, relay both exactly as given and do not shorten the hash: the link opens in the Genesis dashboard, while the plain path is available to people receiving the message in Slack or Teams. The fields and fallback rules are in the toolkit review-link reference. A grade can be not verified even when every structural item is confirmed. The conformance scope is part of completeness. An unmet scope expectation always blocks; an unnamed target object blocks when the scope claims the whole target by carrying same or changed objects across. When the scope names only objects built by this change (for example, new tables), unnamed objects already present on the target are reported in scope_unclaimed but do not block: the spec makes no claim about sibling tables. Unnamed source objects absent from the target are likewise reported in scope_unclaimed_absent, not as missing-target blockers and not as licensed absences: the scope says nothing about whether these source objects should be carried over. This report applies only to object-grain absences under the comparison’s own pairing; named source objects and column-grain differences remain subject to attribution. In that build-only scope, object-grain comparison abstentions do not add an indeterminate blocker for a new or input object (or an object the scope does not name): the scope’s own presence verdict decides named objects, and unnamed target objects remain scope_unclaimed. An undeclared schema map likewise does not add an indeterminate finding when the scope claims only a build, because the spec declares no source-to-target pairing. When a same or changed entry carries an object from a source schema the target does not hold and no schema_map or object_map addresses it, that entry is instead indeterminate with cause: "schema_map_undeclared"; the comparison cannot establish where it went, so it is not graded as not_implemented. The schema_map_unpaired summary groups those scope expectations with the unnamed target objects and missing/surplus readings attributable to the same absent map. Its target objects are excluded from scope_surplus, and the review population represents the missing map once rather than once per affected scope entry. A map must name the target schema each source schema became; use an object_map when the object names also differ. Column-grain abstentions remain indeterminate because scope states presence, not content; abstentions also remain when the scope carries objects across. Missing target objects named by the declared scope remain measured and can still block. The headline names both kinds of unclaimed objects without treating them as blockers. Integrations can use the structured scope status, expected treatment, and target presence on each scope blocker in the review population rather than parsing its basis text; see the comparison review population response. When a full-seal grade is verified_with_indeterminate and unconfirmed changes remain without a failed item or recorded failure, every surface labels it Not enough evidence and says the remaining items need a person. This is an amber result, not a verified one. A verified grade with unconfirmed changes remains Not verified; partial or unreadable seals use their separate wording. The grade also asks for a person’s decision on a target column that is new and nobody accounts for. scope_unaccounted_columns lists object.column coordinates on tables the scope builds or carries when the column is absent from the relevant source and is named by no spec item, sealed check, declared mapping, or target model. For a carried table, the paired source table supplies the comparison. For a split image, the target model’s declared columns on that image supply it; if the model declares no columns for the image, the split’s source table supplies the fallback. A column the split drops, sends to another image, or whose source never held it is therefore new on this image unless another surface accounts for it. For a new table with a target model, the model’s declared columns are the complete answer. Without a model, a new table is read against the scope’s named input tables; if there are none, the grade reads against every source table and reports that limit in scope_unaccounted_limits, and if none of the named inputs are on the source, the limit says no source columns were available to carry. An unlicensed target-only column_surplus on a changed or new table leaves drift and appears in this list; on a same table it remains drift. These columns are not reported as failures: the grade can read verified_with_indeterminate while the card names the pending decision, and the Prover flow marks them unaccounted in its pending tone. In Human Review, each column is an evidence_gap with cause target_column_unaccounted; approving its exception package records that a person accepts the columns as expected, while a spurious column must be sent back as a defect. scope_unaccounted_readings lists the exact unlicensed column readings withdrawn from drift for that decision. The blind findings and canvas keep each in the unlicensed population with unaccounted: true; no item detection or licence claims it as explained. For a palantir_foundry estate, a scope entry may name a dataset by its bare RID, such as ri.foundry.main.dataset.<uuid>, even though the scanned catalog name includes its folder path. Genesis resolves that RID to a catalog name ending in the RID, case-insensitively, only when the supplied spelling is absent from both inventories and exactly one candidate exists across them. It uses the resolved name consistently for scope verdicts, surplus-object accounting, and finding attribution. If there is no unique candidate, or resolving entries would make two scope entries claim the same object, the entry keeps its supplied spelling. Conversely, a confirmed structural removal with no attributed obligation reads as pass with basis: "confirmed_by_diff"; the diff itself is complete evidence for something that is gone, so the item is not left grey as unverified. These removals now count in coverage.items_pass rather than coverage.items_unverified; the grade adjusts those two item counts to agree with the confirmed item verdicts. Read the item’s basis when explaining why a grade passed or remained unverified. A failed structural item is not an unknown: its blocker says failed and names the spec check ids in failed_by. The grade headline groups those failed items by check and keeps “could not be confirmed implemented” for items no check or structural oracle decided. If an item failed structurally without a named failed check, the reason says not implemented or implemented differently from the spec; only an undecided item uses “could not be confirmed.” The grade response reference describes the corresponding failed_items counts and failed_by review-member field. When the grade has obligations, its headline also names structural changes not yet confirmed that were not already counted as blockers: it distinguishes changes with no covering spec check from changes whose checks reached no verdict. These remain separate from failed-item counts. In the flow view, an item the grade marks unverified and attributes no check to is unverified, not a pass merely because a traced check read or keyed on its column; see the API Reference for the flow fields and count. The card is green only when the comparison has zero unexplained, indeterminate, and errored reads, no readings are withheld, and the measuring run did not report clean: false. A missing count is not treated as zero. Refused runs show the Prover’s reason, including the known pairing reason when nothing was compared; if unresolved blockers also exist, the refusal names them alongside that reason. Failed runs say that the comparison did not finish; neither is a verdict. The card provides Review findings and Detailed view links for a completed comparison; Detailed view falls back to the comparison’s Venn view when estate coordinates do not resolve. When a specified grade stands for a comparison whose tables paired, the card takes its verdict and counts from that grade, as the review Overview does, rather than from the raw table-comparison verdict. Its accounting reports the grade’s explained, unexplained, indeterminate, and errored counts; source tables outside the spec’s scope are named separately and are not counted as unexplained. A pending grade is shown as still being graded, without table counts. A verified paired grade is green only when it measured its drift and the grade’s errored obligations plus the comparison’s errored reads total zero. A reshaped build whose tables paired none continues to take its verdict from its spec grade without table counts. See the read_comparison guidance for the presented.spec_grade fields and read cost. For a grade of a derived build whose source and target share little by identity, clients can request a flow view to trace ordered output columns back to the source columns named by the spec and checks, and to account for target columns declared by the sealed target_model. The view distinguishes columns derived by that model from columns whose lineage a spec check establishes; see the API Reference for their states, source-column readings, and counts. When the grade carried no specification, the view explains why there are no spec-ordered columns to trace rather than failing; see the API Reference for that response shape. For how the flow view attributes failed checks—including table-name resolution, ambiguous unqualified names, incomplete traces, and SQL dialect selection—see the flow endpoint reference. For spec-backed flows, the source and target captions name the dialect and database recorded on the snapshots the grade compared. Call it when opening the flow, not as a run-progress poll. When only the counts are needed, request shape=summary; use the default shape=full to show the traced columns, checks and snapshot tables. Summary still reads the inventories and parses SQL to count item states, but avoids producing and transferring the detail lists. The comparison stage uses scope preserved in the spec_conformance run-list summary to choose the Flow or Venn view and explain why; see the list_runs tool guidance for those summary fields. Check-only reads of scoped source inputs appear as comparison references, not unread inputs; the API reference defines the column-level status behavior. Comparison cards defer their undeclared-target withholding caveat to the proof response contract. Clarification review is deliberately after reliance. A person may ratify an agent-made clarification after a seal cites it; the seal then shows person-ratified provenance. If a person overturns it or the recording agent withdraws it on the owner’s word, every seal that cites it and every verdict measured over those seals reads reopened at read time. The reopened run carries the cause in reopened and its outcome becomes not_verified, so a previously green comparison is not presented as a standing verdict. The seat run that produced the seal is not itself reopened. On the review page, an open finding last seen by a verdict over that reopened seal is marked as resting on it, rather than shown as a live failure of a standing verdict; the finding remains open and its history is unchanged. See the ledger response fields; the same notice is available when an agent reads the finding’s history with read_finding. See also the clarification review and reopened verdict API contract for the exact fields and review permissions. For how Prover finding reads handle hidden episode sightings, see the read_finding contract. When presented.kind == "comparison_card", answer briefly: state the status or verdict only when the card carries one, ask at most one follow-up question when needed, and offer “tell me more” for the long form. This keeps the agent response from repeating the counts that the card already shows. The Chat and threads guide shows the user-facing layout.

​

Four words you will see on a run

A proof reports in the same status vocabulary as every other run, and the one reading that trips people up is that a proof whose comparison did not succeed stops before the grade — grading a comparison that failed would be grading nothing. docs/prover/prove.md lists every status a proof can reach and what a caller should do about each. And as everywhere else in the Prover, the status is not the verdict: How a run works covers that distinction.

​

An errored read is unmeasured

When the live re-read needed to decide a comparable table errors, the comparison emits an errored element. This is not an indeterminate finding: indeterminate means the comparison reached the data but could not settle it, while errored means the read produced no measurement. It counts in neither the licensed, unlicensed, nor indeterminate totals, and a diff with any errored element is not clean. Treat it as an instrument or connection problem, using the SQLSTATE, retryability, and failure basis in the comparison summary, rather than as evidence about the estates. The single-comparison API exposes the same errored_reads and clean measurements, plus any comparable_digest_refold disclosure; see the API reference. For a graded proof, the grade view keeps this population separate from findings in unmeasured_elements. Each entry identifies the failed instrument with element_id, its comparison and object coordinates, and the read basis; cause is included when the diff supplied a coded failure cause. unmeasured_elements_basis explains the population. An empty list means every element reported by the diff was measured, while null means the grade recorded no element population (for example, no grade ran or the grade predates these fields). Do not treat an errored element as drift or as an indeterminate ruling: it contributes to neither verdict count and the comparison is not clean.

​

Read the verdict basis, not just the verdict word

Comparison summaries include verdict_bases for the verdicts and named causes that actually occur in that diff. match, licensed, and unlicensed describe measured data; indeterminate describes a comparison that was not measured or could not be attributed; errored means the read itself failed before measurement. For an indeterminate element, use its cause and the matching entry in verdict_bases instead of collapsing every abstention into one generic bucket. In particular, cross_representation_precision_unverified is a float-versus-exact numeric boundary that was not compared beyond float precision, and outside_characterized_scope is a target surplus outside the source scan’s characterized boundary. boundary_not_numeric means that a numeric column’s boundary summary on the named side was not numeric, so the extrema could not be compared as quantities; inspect the column’s null and distinct counts for the underlying values. A substitution can decide this boundary when the source extremum is exactly the literal it rewrites and the target extremum is numeric. If a structural item also catches the reading, it is attributed to those items instead of remaining indeterminate only when every catching item states a change and the same substitution accounts for the column’s entire content-digest movement, including its null-count change. Otherwise the reading remains indeterminate. instrument_void means a person previously ruled the instrument’s reading at that finding’s locus an instrument_defect; a later proof honours that standing ruling as indeterminate instead of re-minting the same finding as unlicensed. For findings whose ledger identity does not include detail, the resulting element’s detail says it was voided, names the actor and ruling time when available, and explains that the reading was withheld rather than re-charged; identity-scoped findings retain their original detail so the ruling remains on the same ledger row. These are instrument limits or rulings, not evidence that the estates differ. When the target characterization declared an absence, the proof summary also carries the declared absent_scope_basis and the measured absent_relations that support it. The closed basis vocabulary is relocation and frozen_build_did_not_produce. The former means a decision-10 relocation has not moved the declared relations into the round-0 target yet; the latter means the measured build failed before producing them and is backed by build_evidence (armed_by, build_rc, error_summary, before_side_measured, and offset-bearing measured_at). The proof prefixes unmeasured_elements_basis with this cause only for elements over relations actually measured absent, so those elements are reported as unbuilt rather than as failed reads. If the absence licence cannot be read, the proof reports that unreadable licence on the same basis field instead of silently treating the target as ordinary.

​

Rounds, and asking the same thing twice

Repair rounds are numbered from 0. Round 0 is the first build, and the number the caller submits is the number the proof reports and stamps on every measurement it creates. A run can also carry an episode round, which belongs to reconciliation episodes rather than to proofs — separate numbering spaces, and a proof is not an episode. Submitting the same proof twice does not run it twice. A repeat is answered by the proof that already holds the answer, marked as reused, rather than by a second run measuring the same thing again. That is why re-asking is cheap, and why a run list does not fill with duplicates when the same acting bot and authenticated user retry. A retry from another identity starts its own proof rather than receiving the earlier result. A run marked superseded is a different and rarer event — it is about the grade, when two different proofs arrive at the same one while it is still running. For the proof/comparison submission-identity split, including the comparison_reused_basis disclosure and the round_n re-measure lever, see the proof API reference. For compiled grades, a reused response includes reused_basis, which explains what the matching identity turned on. When it names the request’s estate_coordinate, the earlier verdict is about the same measured estate. When no coordinate was supplied, it states that the sealed spec, binding, round, and tiers matched but that the identity did not establish that the estate submitted here is the estate the earlier run graded. A fresh grade returns reused_basis: null; see the API reference for the response field and the coordinate’s request semantics.

​

What a run reports back

Every run type answers at one address and in one shape, so nobody needs to know which workflow produced a run in order to ask how it is doing. What a reviewer leans on is the provenance stamped on it when it was created — which build served it, which doctrine it was pinned to, who ran it — and, on a proof, what it reports about its own loop: whether it certifies, which round it was, what regressed, and the source/target snapshot pair it certifies. Every timestamp backed by the estate store — not only the run envelope — is served as a UTC-aware ISO-8601 value; the API reference defines the snapshot and timestamp contract, including the malformed-timestamp exception. docs/prover/run-envelope.md remains the field-by-field shape reference. For committed fork election results in a compiled-spec grade, including the readings_not_taken and taken_verdict fields, see the grade response reference. For the grade’s unadopted offers and per-obligation requirement_source provenance fields, see the grade response reference. Each obligation also reports which target tables its target_sql reads. If the grade cannot parse that SQL in the target engine’s dialect, target_sql_unreadable gives the parser’s reason rather than implying the check reads no columns; the API reference defines the per-obligation fields.

​

Checked substitutions

A passing sealed check can license a narrow literal-to-NULL substitution even when the spec declares no estate-wide value_substitution rule. This is not a license for every passing check: the grade recognizes only a nondegenerate, outright-PASS keyed membership check that reads one whole table on each side and compares the same column. Its target expression must preserve that column while mapping NULL to a string marker; its source expression must preserve the same column while mapping one string literal to that same marker. A source-side TRIM around the literal test is allowed; a renamed column, bounded text cast, or other expression is not recognized. The check licenses only that literal becoming NULL on its compared source column, and only when its target table is the comparison’s paired counterpart and row-check coverage for that table is confirmed. For an ambiguity fork, only the passing member selected by the committed lean can license it. The column’s decided column_content_digest must agree with the substitution, and each licensed reading must be consistent with it; the check does not license other columns, column_max_length, or categorical_value_counts. Finding rule_ids names the proving obligation id, not an accepted_differences rule id. For the authoring-side clause refs, see spec-author identity and constitution.

​

Reporting a completed run

Prover tool answers are for the agent to correct its work, not text to forward to a person. Decide who is reading and relay the relevant outcome in that person’s terms; a self-check gives the agent a to-do list, not a transcript for the person. In a live chat, ask only a business question that still makes sense without Prover terms and whose answer depends on that business; include a recommended answer. If the spec reserves ratification to the person, ask them to approve it even when the recommendation seems clear. In an unattended goal, mission or blueprint run, fix what the agent owns, record unresolved business questions with a recommendation, and continue with unblocked work; wait only when a person’s answer blocks a step. The Prover toolkit reference documents the audience and audience_note fields on each answer. A terminal proof or grade provides envelope.report_this as its record line. Use it as the source for every report; do not reconstruct its verdict, counts, or ids from the nested summary. Quote it word for word and label it as the record when reporting to a data engineer, to anyone asking for the line, or in any record you write. In chat with a business owner, do not quote it: give the plain-language answer, use only the numbers in that sentence, and include the review link where the record lives. It names failing obligation ids and full identifiers returned by the record, so do not supply an id that no tool returned in the thread. A named failed check includes (<mismatched_key_count> of <rows_compared> rows) when its mismatch count is known and it compared at least one row; when that count is a floor, it is rendered as at least N rather than as an exact measurement. When mismatched_key_count is null, the sentence uses the key-probe sizing described for the failed-check headline when available; other checks without a measurable size have no suffix. The report names up to ten failed checks, plus an eleventh when it is the only one beyond that limit; when more remain unnamed, it summarizes them as and N more and points to summary.verdict.failed_checks, where each remaining check is named with its size. For grades, it also names unmet-scope objects and every derived table excluded from the claim, with its recorded exclusion reason or, when none is recorded, that no passing declared check covers it. It reports how many items the review opened with when the grade carries that population. This opening count is not the live number still awaiting disposition: read the review for that. If you add your own interpretation of a failure, put it in a separate sentence and label it as your reading; do not let that interpretation change the reported tally. The sentence uses the grade’s own verdict; a recorded failed check is not described as verified just because conformance.verified remains true. The record carries no cause or fix order: unless a run field names a causal link, report failures independently and label any inferred cause, link, or proposed order as your inference in the sentence that states it. A heading alone does not make that distinction. One cause is recorded: when a proof’s comparison ran under an assumption withdrawn for the estate pair, the line names each withdrawal (who withdrew it, when, why) and how many readings it moved, as licensed readings now unlicensed or readings it made comparable now indeterminate. Attribute a changed reading to that withdrawal before any other cause. When a grade records all classification buckets, the comparison counts in this line use the grade’s classification: drift, spec_licensed and platform_licensed replace the comparison’s pre-spec unlicensed count. The line includes the comparison’s errored-read count when recorded. If classification.model_licensed is nonzero, the line names that subset as derived by the target model rather than licensed by the platform; the remaining platform-licensed count keeps the latter wording. When a complete classification has derived_checked entries, the line also counts those derived tables as not compared cell by cell (covered by checks). If the grade has no complete classification, it reports the comparison’s counts instead. The API reference defines the field and when it is null. Give every build you report its own report_this sentence, including when one reply covers several builds. Read each sentence before your interpretation; when the audience is to receive the quoted record line, quote it first. A table, list or comparison that names a build without grounding the report in its sentence is not a substitute. When a grade says readings are licensed by the spec, report them as licensed rather than as unlicensed drift or blockers. When a check you authored fails on a build you believe is correct, report a failed check, not a build defect. Read the check’s SQL against the mapping clause it cites; repair the check if it does not measure that clause, or open an adjudication if the result is unclear. Do not call it a build defect until that review or an adjudication says so. Evidence for an approver must quote the record’s counts and the obligation ids in the seal you proved against. A waiver covers drift, not readings the grade already licenses.

​

Prover run progress

Every run poll carries progress, next_step and next, including list rows and terminal responses. progress has exactly nine keys: phase, phase_basis, source_message_count, last_activity, write_version, unavailable_reason, streaming, last_chunk_at and stream_chunk_count. For a seat-backed run, dispatching means its thread has no message yet and working means the thread has been written to; working is not a liveness verdict because the message count is cumulative. Compare last_activity or either counter across polls to see whether the seat is still writing. A failed read reports phase: "unknown" with the reason and null counters rather than claiming working; terminal runs report their own lifecycle status as the phase and do not read the thread. Runs without a seat thread also publish the same shape with an explanatory unavailable_reason. The spec-author stall outcome is documented in the author-seat API reference: use error_type: "run_stalled" and its next action to restart after checking committed work. The stall watch compares the thread’s writes with activity reported by the runtime that dispatched the turn; an unreadable runtime view gives no verdict. Before the row becomes terminal, the driver asks that runtime’s hard-stop to stop the turn, retrying refused requests under the configured stop policy. Configure the bound and stop policy in In-product spec author settings. next_step translates the lifecycle into an action, in words. Live runs say when to poll again (about 20 seconds); completed runs point to their output, refused and failed runs explain which summary field to read before submitting again, and cancelled or superseded runs say that nothing further will be written. No new setting enables this block. next is the same fact as a literal call — {verb, args, why} — for a caller that would rather act than parse a sentence. Both are derived by one owner from the status, the run type and the envelope’s own summary, so they can never name different things. verb is null, never absent, when no call by this caller moves the work along: a decision a person records, a permission an administrator grants, a refusal to fix before resubmitting. A failing grade that read no comparison gets its own Human Review population: each failed check is a blocker on the grade’s review, where a person can record a ruling or a one-time exception. The review is explicitly proofless — it says that no comparison against a build was made — so it can never carry an approval, and no run-level approval is offered for it. Its next names the proof that creates the comparison beside the grade: prove for a single sealed spec, or grade over a SET’s spec_hashes with the structural tier. Until that follow-up reads a comparison, report the failures as reviewed but not approvable. The finished grade and its get_run poll also hand over this review’s URL and dashboard path; see the grade tool reference for the returned fields and null-URL cases. On a terminal run that produced a comparison, four rules pick it, in order: work the run left UNMEASURED that one argument would determine (a re-prove carrying row_identity); then measured findings, which offer the adjudicate call — a proof never opens an adjudication itself, and a clean comparison’s next says there is nothing to adjudicate; then a clean comparison that carried no spec, which advises author_spec while stating that what was proved is that the data values agree and nothing beyond them; then a clean graded proof, whose remaining act is a person’s. A proof also carries its comparison child’s verdict counts at summary.comparison_counts so its own envelope can say whether anything stands. The three prover_tools answer shapes carry next too — a run handle reads it back off its envelope, a read names the verb that consumes what it produced, and a refusal names the act that unblocks it. The same refusal contract applies to the other Prover-family tool groups, including source_contract_tools and the adjudication, conformance, court, and ruling tools. An unidentified refusal means the turn has no signed-in person against whom to check the permission. This is not a permission denial, so no administrator action is needed. Tell the user to repeat the act in a turn they start, or in a mission they started; the normal permission check applies there. A permission refusal instead means an identified person lacks the permission and may need an administrator to grant it. A supported product-woken turn can carry its thread owner’s visibility without being that person’s act; see the identity rules below. When a Prover action starts a Blueprint, missing Blueprint execute access is a permission refusal, not a service fault. Ask an administrator to grant the role execute on that Blueprint before retrying; the Blueprint mission-start API contract describes the HTTP denial fields.

​

Unattended mission visibility

On an unattended mission turn, Prover scopes reads to the person who started the mission when the mission identifies a valid originator. This visibility alone does not make that person the caller or satisfy permission checks. An approval still needs a truthful basis and must be within a goal or mission that person set. If no originator can be established, a scoped read returns unidentified rather than not_found, which would imply the object does not exist. If the mission identity cannot be read, Prover returns unavailable for a scoped read that needs it, so the caller can retry. Product-woken turns—including mailbox deliveries, run-finished notices, handoff completions, held-goal nudges, and scheduled runs—can carry the thread owner’s id marked as borrowed. Prover uses that id for the owner’s visibility and to open their saved connections, but the turn acts as the agent on behalf of the owner: permission checks use the agent’s allowlist, and run attribution names the agent and the owner. Visibility alone does not authorize an approval; an agent’s approval must be part of a goal or mission the person set and is recorded with that basis. A person’s own prompt and their own held words are not treated as borrowed turns. The owner-scoped proposal, bundle, and package-list reads are read_proposal, read_bundles, and list_packages in the Prover tool reference.

​

A fault is a re-read, not a terminal answer

refusal.kind: "fault" means the service failed; it does not mean that the system declined the request, and it does not prove that no work started. Re-read before reporting the act as finished. The refusal’s next names the same verb and the caller’s same arguments and identifiers, so make that call to discover whether a standing record already owns the act. That re-read returns the existing work as reused or reports a conflict instead of starting a second one. This rule also applies when an exception escaped any Prover-family verb without a more specific classification: the tool still returns the refusal shape with kind: "fault", so callers can branch on refusal and next instead of treating a bare tool error as a completed or terminal run. When the operation is not safe to repeat, next.verb is null; read the durable record named by the operation before retrying. When a run or proceeding id was allocated before the failure, the fault names that id and the read verb to use. For the retryable unavailable refusal used while a service is starting, see the service-error mapping. HTTP 410 Gone maps to not_found, not fault. Proof admission has one additional hand-off case: if the serving loop stops before the admission reaches it, nothing was admitted; if it stops after hand-off, the result is indeterminate. For recovery and the request identity to reuse, follow the proof endpoint reference. The Adjudicator exposes the same nine-key block on every response from POST /api/estate/adjudication/runs/{run_id}/adjudicate. If a call omits round_n, it joins a proceeding already running for that run under any round; when none is running, the omitted round uses 0. Name a round to open or read that specific proceeding. Re-call the endpoint with the same run_id and the response’s round_n to poll the proceeding that answered; its next_step is specific to that proceeding, and its partial ruling remains in verdicts against finding_count. The response also carries started_at; see the API reference for its round-selection, timestamp, and nullability contracts. When a grading run opens the proceeding, its snapshot also briefs earlier verdicts for pair-scoped durable findings in prior_verdicts; see the fetch_adjudication_materials contract. The proceeding has no timeout; it ends when the seat submits or orphan reconciliation closes it. In active mode, if the completed verdicts name no comparison held by the instance for staging, the proceeding closes as failed instead of remaining open for retry; its verdicts remain readable and next_step directs the caller to open a new proceeding. A ledger-refused disposition package also closes the proceeding as failed, rather than retryable; the submission tool contract distinguishes it from a failed package write. A fresh proceeding also requires an LLM provider, while repeating a round that already has a proceeding is a read; see the API reference for the response fields. A run detail read can also opt into include_proceedings=true to list the proceedings opened on that run (addressing only, newest first); use that pointer because completing a proceeding updates adjudication tables, not the run’s grade-time summary. When a proceeding wake carries verdicts, its routing fields and the durable object_name / column locus are populated from the findings ledger, so a wake and a poll identify the same finding even though the wake may also include materials. For a graded proof, the summary includes rounds_used_basis alongside rounds_used; the basis is always a value, not null. When the request names no round, the basis says “no round was supplied on the request, so this proof is the first and only round it can account for”. When the caller names a round, it says “the caller named this proof’s round, and rounds_used is round_label + 1 in the one 0-based numbering space (round 0 is the first build)”. The proof also includes ask_level and ask_level_basis. The builder-facing page uses finding when work is under durable finding IDs, or ticket when the ticket states the work because the product owns none of the observed items. A proof delivers no builder page, so its ask_level is null and the basis explains that absence. An ungraded proof carries neither grade-side key: spec: null and spec_basis state that the comparison ran without a specification. For a graded proof, the obligation regression tier is a statement about the series, not one adjacent round pair. A round above 0 walks the earlier finished grades in the same series in order, including readable late-completion records for grades that arrived after their run row was reaped. A FAIL after an earlier PASS opens a demotion, and that demotion remains in the current tier until a later round grades the obligation PASS again. The tier therefore lists every demotion still open at round n; each row carries from_round and to_round so the round that first failed is not lost. A second consecutive FAIL does not reopen or re-date the row. Only PASS and FAIL are measurements. An unverified or errored obligation neither opens nor closes a demotion, and the walk passes through that round. Obligations that could not be measured, or whose verdict could not be attributed to a sealed structural item that this tier can follow, are listed in obligation_regressions_unmeasured with a basis. The latter is still a measured verdict; it is unmeasured only for this round-over-round structural tier. When no obligation was measured, the tier is unmeasured (certifies: null) rather than an empty list that could be mistaken for a clean result. The tier also remains unmeasured when the series walk cannot read the required earlier rounds. The grading path also refuses an obligation with an unknown non-null kind instead of falling through to the keyed comparison contract. A typo therefore cannot become a determinate PASS; correct the kind and grade again. null remains optional where the artifact contract permits it. For an eligible keyed obligation whose source is Foundry and whose source SQL reads only dataset RIDs, the grade can use their full landed Databricks copies instead of reading those rows from Foundry. Each RID must have one unambiguous stamped full copy in the target-side schemas; the copy must not be marked as a pipeline rebuild, and the target SQL must not read that same table. This is selected during the grade, not retried only after a Foundry query fails. The result’s source_read identifies each copy and its warehouse-reported last-altered time, so interpret the verdict against the rows as landed, not as a fresh read of Foundry. The same route can serve a source-side invariant whose relation is a dataset RID, but not when any obligation’s target-side read uses that copy. An invariant graded on the target stays on the target. A keyed obligation’s grain_probe also runs against copies when it reads only dataset RIDs covered by the copies already used for source_sql; any other probe remains on the source. The degeneracy reading follows a copied source_sql and carries the same source_read evidence. The API response reference documents the field shape; the Foundry migration tools guide explains stamping and adoption. builder attribution requires both facts: the sealed specification is unchanged by the series identity, and the bracketing rounds graded different target snapshots. If the estate did not change, or either round has no target snapshot (for example, an obligations-only grade), attribution is null and attribution_basis explains why. The series walk uses the snapshot ids each grade recorded; on a finished grading run, they may be stored under summary.provenance rather than at the summary’s top level. The product path has no compiled-spec gating flag, so every demotion row is demoting: true and includes demoting_basis. Round 0 is measured-empty only when the grade measured at least one obligation; a round whose obligations are all unverified/errored, or a spec that declares none, is unmeasured. A caller that omits the round is not treated as round 0: the grade still runs, but the obligation tier reports that no series position was named.

​

When a grade did not measure

The API response reference documents the exact measurement contract: the obligation_verdicts.unverified list names errored or otherwise undecided obligations, including the declared relation for each obligation so an errored invariant still has a locus; comparison obligations use null. drift_basis prevents an empty measurement from becoming a clean certification. It also explains how spec_hash_basis and projected_spec_hash_basis distinguish a registered compiled artifact from a run-only projection, including older runs that lack those fields. For a declared target mapping, history_not_testable is the companion list for historized images whose source history was not graded. Each entry names the image and explains whether the mapping lacked a readable history source or its generated history obligation did not decide; an empty list means every rendered history check decided, not that a latest-state table was assumed to contain complete history. An errored obligation can carry a declared cause: spec_as_written means the instrument refused the obligation before touching an estate, while instrument means the grade could not bind or answer it, including a target statement that could not execute. Read the obligation’s error beside cause; retry unchanged only for a likely transient failure such as a timeout or dropped connection. If the error names a statement, relation, or column, correct the relevant connection or catalog, spec statement, or target before grading again. For keyed checks, a measured missing target column can instead produce FAIL; see the verification response contract. An engine that cannot answer the obligation needs another instrument or a ruling. A missing cause is deliberately not classified from the error text. When an errored obligation carries errored_sql, its hashes and character counts point to the sealed source and/or target statements without exposing SQL in the run record; the compiled-grade API reference describes how to read those pointers. A PASS over a measured population of zero rows instead ends as nothing_to_check in both the obligation’s verdict and status: the check ran, but the data gave it no rows to decide. coverage.nothing_to_check counts these obligations, and coverage.items_nothing_to_check counts structural items whose attached checks all ended this way. They are not passes, failures, errors, or unmeasured checks, and they do not confirm the relations they cover. When every declared check has this ending, the grade is not_verified and its headline explains that no check confirms the target; empty checks alongside other outcomes are called out without counting for or against the claim. For a seal with a recorded clause_gate, the grade lists unchecked mapping clauses only from the clauses that gate counted. If a commissioned document had nothing to count, clauses_not_checked is empty: a ledger entry cannot make a clause number supplied by the author into a clause of that document. This does not change the reading when no document was commissioned. An unchecked mapping clause can still be linked to a structural item. When its ledger entry’s refs name item ids, the grade says the clause is covered by those items and gives their verdicts; those items do not become sealed checks for the clause. These links appear as carried_by_items in the entry under obligation_verdicts.clauses_not_checked, with each item’s item_id, verdict, and basis. If there are no ledger refs, an exact item id mentioned in the clause text or seal note instead appears in items_its_note_names; this is reported only as an item the seal note names, not as grade-asserted coverage. The headline and report_this give the linkage and item verdicts for the clauses they list; see the spec-author tool guide for how to record structural refs. Each compiled grade also carries a degeneracy reading by obligation. measured means the probe read the obligation’s expected source side and checked its three known degeneracies (empty, all-NULL, and all-zero); errored means that read was attempted but refused or failed; unmeasured means the probe did not run for that obligation or could not open the source. A measured reading with no findings is not evidence that the obligation can fail — it only says that none of those three degeneracies was observed. If an obligation is FAIL but its measured expected source side is empty, the grade reports it as unverified: the comparison shows target rows without establishing that the build is wrong, because the check as written has no source rows to compare. For a violation-count measure, zero violations over rows that exist is the check’s passing claim rather than an all-zero degeneracy: the grade runs an additional read-only population count and includes the number of rows counted over in the basis. Only a count over no rows remains degenerate. Other all-zero measures retain the all-zero finding. Committed leans now explain rival failures in the grade summary.

​

Drift findings declare their coordinate

In a completed conformance grade, each drift_finding discrepancy declares its join coordinate in comparison, object_name, and column. comparison names the ledger’s comparison, object_name names the object, and column is the column name or null for an object-grain difference. Join or group drift findings with these fields; ref and evidence remain the addressing and human-readable forms, respectively, and should not be parsed to recover the coordinate. Older persisted summaries may omit the fields, so a read of those summaries retains the legacy fallback rather than inventing coordinates. When a discrepancy carries a non-null bucket, treat it as a lean, not as a ruling or a punch-list placement. auto: true means a deterministic rule supplied the lean; auto: false means it came from a judge or that no deterministic rule supplied one. Read placement for where a finding was actually put and is_lean for whether an opinion exists. A null bucket means the adjudicator must decide without a lean. The grade also discloses an incoherent obligation-coverage block when its counters do not close; do not read a floored zero remainder as proof that every obligation was accounted for. The stored grade is terminal, but a later ledger ruling can still change the placement shown by a run read. For a grade read with a row-bearing shape, Genesis joins ruled coordinates to the discrepancy’s comparison, object_name, and column; it fills placement and placement_label only when every ruling for that coordinate agrees. An unruled coordinate or conflicting rulings remain unplaced and therefore still count as awaiting adjudication. The served awaiting_adjudication total is recomputed from those returned rows, while summary.adjudication.buckets remains the grade-time value. An envelope-only read has no discrepancy rows and does not perform this ruling lookup.

​

When the named spec is no longer reachable

Run envelopes and proof rows also expose spec_hash_resolvable and spec_hash_resolvable_basis. These are read-time checks against the compiled-spec store on the instance serving the response; they do not rewrite the stored spec_hash. A reader can use them to tell whether a completed grade can still be fetched for re-verification, rather than treating every status: succeeded run as reachable. spec_hash_resolvable is true with a basis beginning registered: when this instance holds the compiled spec named by the run. It is false when the store was read and the artifact is absent. The corresponding basis begins artifact_absent: when the run said it graded a registered compiled artifact but this instance does not hold it; projection_seal_pre_contract: identifies a grade written before the spec_hash contract, whose hash was a per-run projection seal that was never registered; direct_envelope_seal: identifies a direct grade whose hash is the sealed envelope itself; and unattributed_hash: means the record names a hash but does not say what it represents. The value is null when no measurement was made. Its basis is the exact sentence this run names no spec_hash, so there is no artifact to resolve when the run names no hash, or begins this response did not read the compiled-spec store when the response did not read the store, including a GET /api/estate/runs/{run_id}?shape=legacy poll. The spec_hash_resolvable_basis field is always present on the envelope, so callers do not need to infer whether an omitted field means “not applicable” or “not measured.”

​

The spec-author seat

A specification is mechanized by an agent in a seat: one thread, read-only access to the estate, and a constitution pinned by name, version and content hash. The tools refuse to run when that pin is not in force, and the seal records it — which is what lets a reviewer say, months later, which doctrine a specification was written under. The seat is listed in your agents as Prover Spec Registrar, beside Prover Adjudicator and Prover Consult. Its agent ID is spec-author, which is what the PROVER_CANARY_SPEC_BOT setting and its sealed specifications’ provenance name. It registers a specification a person wrote; it does not invent one. The open interpretation policy and its Prover Spec Registrar (open policy) bot (spec-author-open) are retired: lean is the only policy, a run that names open is refused, and startup removes the spec-author-open bot row while keeping its threads and history. A specification sealed under open stays readable and is repaired under lean. New seat runs use Registrar authoring tooling by default. For per-run and deployment opt-outs, phase checkpoint snapshots, skip requirements and run-end cleanup, see the Registrar tool guide. For the polling payload, see the Genesis API reference. The constitution may be an ordered set of files rather than one file. The seat must read every pinned file in order before sealing; finalization verifies the files actually served to that thread. See Spec-author identity and constitution for the current file order, refusal behavior, and v9.25’s source-side-only R7 boundary. For constitution v9.27’s derived-build and carried-image seal rules, see the seal findings and registration fields. Constitution v9.28 encodes a “when X, then Y” rule as a violation count over the target (rows where X holds and Y does not, expected 0), not as a membership; see Spec-author identity and constitution. Constitution v9.29 lets the seat seal partially: clauses it cannot prove yet are sealed as open, with a reason, a remedy and the evidence, and the seat run reads sealed_partial; a follow-up names the partial seal as repair_of to add them; see Spec-author identity and constitution. Constitution v9.30 stops the seat asking what a migration already answers: preserve-the-source properties (NULL counts, empty string vs NULL, whole-row multisets, types, keys, value domains) are adopted as migration defaults and checked, a question about what the source holds is measured, and only an intended deviation is put to a person as an open clause with a recommended answer that does not block the seal; see Spec-author identity and constitution. Constitution v9.31 adopts every migration default silently, the row count per key included: if the answer would be the same for every customer, it is not a question. What does reach a person (owner or operator) is a choice only they can make, in the business terms of their own data, with what each choice costs and a recommended answer. Questions the seat withholds as migration defaults remain recorded separately from the questions sent to the owner; the author-seat API response documents that field. Constitution v9.32 asks every height, key or grain check (a row count, a distinct-key count, a violation count, a total) to name the table it measures, through owning_relation or a linked structural item; registration refuses one that names neither, and a check whose only reading of that table states a typed number is refused as measuring nothing. Constitution v9.34 requires a fresh Registrar round to declare each target-mapping image column listed in metadata_columns with a column structural item, including columns with no source input. An undeclared column prevents the spec from sealing; see the finalize_spec refusal details for the accepted declaration loci and repair guidance. The v9.5 constitution also requires collection-valued checks to state the result for both empty and NULL collections on both sides; see the spec-author tool reference for the normalization rule. Target-engine preparation only compiles the target expression, so it does not replace that semantic check. When the seat registers a target mapping, it probes every readable hub key even if another hub’s probe fails; the refusal names all failed probes and preserves findings from probes that completed. See the spec-author tool reference for the registration contract. Conversation-level mapping continuity and its early refusal path are covered in the author_spec contract. The seat applies the same proposer-owned undeclared_input seal refusal when an input scope does not agree with target_model; see the finalization refusal details for the mapping requirements and target-only input exception. When no mapping was proposed for a target built from other tables, it returns the same unmapped_reshape refusal instead of sealing; the finalization refusal details describe the proposer response. When no mapping was proposed for a target built from other tables, it returns the same unmapped_reshape refusal instead of sealing; the finalization refusal details describe the proposer response. When an unsided invariant names a relation the declared target model builds, the seat’s registration rules may infer invariant_side: "target" from measured source absence; see the obligation registration contract for the inference receipt and the ambiguity refusal when both estates hold the relation. If registration cannot establish the side and leaves the invariant source-graded, see the finalize_spec contract for the seal-time refusal when its build-output relation is absent from the source. For a historized image, the seat asks where the source keeps its per-batch history and expects that relation in the mapping’s history declaration. The mapping renders its row-membership check as well as the history check; when no source history is declared, the resulting grade names the image in history_not_testable instead of treating a latest-state snapshot as proof of history. See Declared target mappings and Data Vault shapes for the declaration shape and grading rule. Mapping registration also checks declared references against their referenced source columns. When a registered mapping splits a source object, register_scope refuses a same expectation immediately—even if an image keeps the object’s name—so scope each image as new; see the register_target_model contract and finalization refusal details. Finalization also refuses carried_column_added when an add_column item names a column the mapping carries into a differently named image, carried_column_item for any other column item on such a column, excluded_but_delivered when the scope excludes an object the mapping delivers, unassessed_but_assessed when the spec scope, structural items, or obligations name a table the mapping leaves unassessed, unassessed_without_scope when unassessed tables have no spec scope, and invariant_grades_nothing for an invariant with no constraint the grade counts; see the same finalization refusal details. Successful seals can also carry non-blocking review_findings for contradictory live clarifications or uncovered must_match structural items; see the finalize_spec tool reference for their conditions and how to act on them. The seat behaves like every other trigger: it returns a handle at once, accepts the same bounded wait, and is watched at the same address as everything else. The terminal response contract is in the author-seat API reference. When an HTTP caller resubmits a prior seat run, it must name that run with resubmission_of; unlike a same-conversation resubmission, HTTP does not infer a mapping to carry. See the author-seat request fields. For a connection serving both estates as separate catalogs, see the author-seat API reference and author_spec tool contract for the source_catalog and target_catalog request fields. Seat queries: see _query_database. The constitution states what the diff already covers, so the seat writes only what is beyond it. Every proof runs the system diff first, and it measures object presence, column presence, types, row counts with row identity, value distributions and keys mechanically on both estates. Restating any of that as an obligation doubles a finding, and a hand-written measurement frozen at authoring time can contradict the diff’s own at proof time. What is left is what only judgment finds: business rules, semantic invariants, cross-table consistency, derived-value rules — plus anything the ticket states as an absolute, because the diff compares the two estates and can never evaluate a figure, type or domain the ticket names on its own. 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. When several specifications are graded as one set, a cross-table check can use owning_relation to attribute the check to the one member that owns the relation it names; the full field contract and fallback behavior are in the spec-author tool reference. A one-line ticket is a valid 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 seat seals the smallest specification that carries a row-set claim and the diff carries everything else. That is the right answer for a lift-and-shift; a ticket that states a rule, a derivation, a domain or a reshape gets a correspondingly larger specification. Membership root-axis defaults and the registration receipt are documented in the register_obligation contract. For a TIME target column ratified for STRING HH:mm:ss storage, the seat must declare the source column’s form when registering its value binding; it does not infer the form from the values. See the register_time_value_binding reference for the accepted forms, unresolved 000000 behavior, SQLite text-encoding support, and how unsupported-engine refusals are routed. A repair round hands the seat nothing. When a grade or a review finds something wrong with a specification, the seat re-authors it — and it is not given the prior specification in its brief, nor can it reach the sealed file. It loads that specification through its own tools, edits what the findings actually name, and re-seals. Most untouched content carries into the new seal unchanged, and the new seal records the one it repaired, so the chain back to round 0 stays readable. A prior NOT APPLICABLE clause may instead need grounding again; see the load_prior_spec response. See the author_spec tooling guidance. load_prior_spec reports the inherited setting. A seal made under the retired open policy is repaired under lean; the repair run records that in seat_settings_inherited. Classic tooling is retained only for repairing a classic-sealed spec: a classic commission must name that seal as repair_of, or it is refused at submit and nothing starts. Any repair may name its prior as repair_of: when it names no catalogs, the seat then reads in the prior’s catalogs from its first query rather than only once load_prior_spec has run. See the author_spec tool reference for the per-run override, and the load_prior_spec response for inherited-setting details. On a classic repair, a commissioned owner clarification can rule out a carried check through a deletion amendment on finalize_spec; see the finalize_spec repair guidance. If load_prior_spec cannot read the seat run, it refuses to seed; follow the retry and commissioning guidance in the load_prior_spec reference before continuing. A repair commissioned without either catalog can inherit it from the prior when the corresponding source or target connection matches. A chat or CLI repair without a seat run also inherits the prior’s recorded connection and, when it remains bound there, its catalog placement; if that prior recorded no connection, its lineage is followed to the nearest ancestor that did. See the load_prior_spec response for the repair binding behavior. When it re-registers a seeded declaration unchanged, the tool preserves that sealed shape instead of refusing it for a newly introduced conditional rule; changing a conditional field still invokes validation. See the spec-author tool reference for the exact field-level contract. That contract also refuses SQL whose NOT IN subquery can yield NULL; use the register_obligation guidance for the affected fields and safe rewrites. The repair-round tool reference documents the fixed prior-grade reading returned by load_prior_spec, including obligations whose latest grade could not decide them. The tool checks for registered draft work before paying for that grade and provenance read; an occupied draft is refused without those reads, while a successful seed records one fixed grade block for the round. The seal also records evidence that each obligation source relation was observed during authoring. That evidence is not tied to one bind mechanism: a resolution probe, registered query transport, catalog read, or executed sample can provide the receipt. A repair round carries the prior seal’s evidence for source relations it does not introduce, while a newly introduced source relation must be observed before sealing. The tool-level receipt fields and refusal behavior are documented in spec-author tools — relation observation evidence. The receipt’s connection must also match the estate the seat was commissioned against; otherwise the seal refuses a spec re-anchored on a copy unless the operator explicitly declares the substitute source and reason with source_estate_basis. See the author_spec tool documentation for the parameter shape and caller rule. The sealed provenance also distinguishes surface: "seat" from surface: "tool", so a specification authored by direct tool calls is not mistaken for one written under the seat’s constitution. The seat can also receive a caller-declared asset inventory. Each handed-over asset must be labelled canonical or hypothetical with the caller’s basis; the seat does not infer or correct provenance. It reports that inventory before deriving obligations. A hypothetical asset produces a findings pass and stops before sealing, so the caller can resolve those findings and submit a second run whose assets are all canonical. A run with no separately declared assets remains the valid one-line-ticket case. The request and response fields are documented in the author-seat API reference. An asset may also carry the document itself, inline, as a file in a local bot-git repository, or as a file attached to the current chat. For a chat attachment, pass the File ID or Git Path shown by its attachment notice. When the notice spells the attachment as a repository asset in uploads, omit ref only when no local bot-git repository named uploads exists; when that local repository exists, supply its ref. See the author_spec tool reference. The submitting user must be allowed to open the conversation that contains an attached upload or a file under the shared uploads repository. Otherwise, the asset is refused before its bytes are read and the authoring run does not start. Genesis resolves repository and upload files at submission, stores each document beside the run, and the seat reads it in 50,000-character pages with read_spec_asset rather than working from a caller’s transcription. Numbered items and table rows in those documents are clauses the seal must account for; asset clause keys are namespaced as <asset>#<key>. The intake and seal expose the source, character count, SHA-256, and storage metadata, not the document body. The seat’s limits and unreadable-asset refusal are defined in the spec-author tool reference. The caller may also pass clarification record ids for decisions the ticket leaves open. Use list_clarifications when the id is not known; it lists the estate’s rulings, review state, and citing sealed specifications. The seat accepts only records belonging to the named estate, and the sealed specification keeps each record’s label and recorded identity. An agent record also says which signed-in person the conversation was with, or says unauthenticated when auth was disabled; that does not make the ruling person-ratified. If the recording agent later withdraws the ruling on the owner’s word, it cannot be cited by new authoring; see the withdraw_clarification tool. This is distinct from ticket prose: a heading that calls a decision customer-ratified does not establish that provenance. The spec inspector exposes the resulting who_decided view, and the exact recording and authoring calls are in the Prover toolkit reference.

​

Open questions and provider faults

When the seat cannot settle a business question by measuring the estate, it returns the question in open_questions rather than dropping it. A terminal run notification can bring the numbered questions back to the agent that called author_spec; the run envelope’s next then names resolve_open_question for the next unresolved number. Resolve each with a recorded clarification or an explicit reason to proceed without an answer. The spec can be sealed while questions remain open; its sealed seat view reports how many owner-directed questions the authoring turn left for resolution and directs the agent to answer or confirm each. The run envelope’s next continues to track the unresolved question separately. Only after every question is resolved does the sealed seat hand off to prove; the same resolution state is visible from read_spec and the Estate API. A completed authoring run can also offer a true check the seat declined solely because the ticket states no rule requiring it. This is separate from open_questions: the notification gives the obligation id and a ready-made question to put to the ticket owner, word for word. A numeric maximum or minimum is labeled an observed bound, not a stated requirement: the current data satisfies it, but that alone does not make it a business rule. The offer asks whether the business requires that bound; it is still offered because only the owner can decide. If the owner agrees, create a record_clarification record with the offered statement and a subject, then commission author_spec again with its returned id in clarification_ids; the new seal carries the check as a stated rule. The rule belongs to the owner, so do not answer the offer yourself. A separate terminal notice can list migration defaults the seat offered but did not register; these are distinct from owner-rule offers. See the read_spec reference for how they appear in offered_not_adopted and the repair path. If the model provider drops or stalls the stream during the seat’s turn, the driver keeps the run alive and retries in the same thread after estate_char.spec_author.provider_fault_retry_seconds seconds (default 60; 0 retries immediately). A retry that faults again is retried after twice the previous wait (60, 120, 240 seconds at the defaults), up to estate_char.spec_author.provider_fault_retry_attempts retries (default 3) and estate_char.spec_author.provider_fault_retry_ceiling_seconds of total wait (default 900), so a short provider outage does not cost the run. The brief and work already registered by the seat remain in that thread. A provider fault after the last retry fails the run with error_type: "provider_fault"; invalid or rejected requests are not retried. See spec-author settings for the bounds and the exact configuration contract. If limits are lowered mid-run so a previously recorded retry is no longer allowed, the driver closes the run as a provider_fault instead of leaving it open for stale-run reconciliation. The ticket may also state how the change must be built. In that case the author records those customer words in the optional SUBSTRATE section with register_substrate; it is sealed for later retrieval but is not an obligation and is not graded. After the build, the building agent can read that section by spec_hash and submit a labelled statement: self_certification with anchored: true when the spec declares a substrate, or substrate_declaration with anchored: false when it declares none. Either record is explicitly a statement, not a proof, and carries is_proof: false; mechanical substrate checks, not the statement, are what can later contradict it. See spec-author tools and the substrate API endpoints. For transition-contract source characterization, an engine whose inventory is not available through the database connector is refused before any catalog read; see the transition_contract_tools documentation for the refusal semantics. Do not key a catalog comparison on ordinal_position. information_schema.columns.ordinal_position is engine-specific: BigQuery numbers columns from 1 and Databricks from 0. The seal gate refuses an obligation that reads information_schema.columns on either side without a portable rank and uses ordinal_position as a key, because a correct column order can otherwise pair each column with its neighbour on the other engine. Rank the columns within each relation instead, for example with ROW_NUMBER() OVER (PARTITION BY table_name ORDER BY ordinal_position), and use that portable rank as the key. Using ordinal_position only in compare_columns or ORDER BY does not trigger this refusal; a rank aliased back to ordinal_position is accepted only when it is partitioned by table_name and ordered by ordinal_position.

​

What “certifies” means

A proof reports whether it certifies, and always with the reason it earned. There are three, and the middle one is the one worth understanding:

• Nothing counted against it. Clean.
• Something was broken and fixed inside the loop. Every row that counted against certification was re-graded as passing, so the proof certifies.
• Something is still open. At least one row that counts against certification was not repaired, and the proof does not certify.
• A tier could not be measured. The proof reports certifies: null with a basis naming the missing record; it does not treat an unreadable tier as clean.

Two properties behind those three:

• A regression repaired under the notice turn is a passing row. The builder broke something and fixed it inside the loop, and the row records that the repair was made under the notice it was given. That is the loop working, and recording it as a failure would punish the mechanism that caught it.
• Certification reads both tiers. Regressions are measured over findings and over obligations, and the two are never merged, because an issue and an obligation are different things about different objects. A run that looks clean at one tier can hold the demotion that stopped it certifying at the other.
• A proceeding rule belongs to a durable finding. When a conformance run has no usable locus, the item-level match is accepted only for one open durable finding; ambiguous or unmatched checks are refused instead of becoming synthetic finding keys. See the adjudicate_conformance_run tool contract for the matching and refusal behavior.
• Obligation rows are product measurements. They compare the persisted per-obligation verdict blocks across rounds. The product path does not invent re-grade, notice-turn, or finding links for these rows; those fields remain empty when the product did not perform those actions.

​

Review decisions are not certification

Certification is a reading a run produced about itself. The review decision is a person’s statement about the comparison, and the two are not the same act: a proof that certifies is evidence in front of you, not a signature on your behalf. What an approval attests to and how its authority is recorded are set out in Roles and approvals, including the basis stored when an agent acts for a person.

​

For the agent doing this

The calls, the response shapes and the refusals live with the code, in the Genesis repository under docs/prover/ — contract-shaped, written for an agent reading before it acts, and each page states how it was verified. docs/prover/index.md is the map of that reference. This page never restates the calls. To read the attestation summary bound to a comparison, use the comparison-attestation API reference. When an agent walks the remediation findings worklist, use the bounded GET /api/estate/findings page contract: pass each response’s next_cursor as cursor until has_more is false. Evidence is opt-in because it is the large column; request it only when the caller needs witness values rather than the default slim listing. For supported distinct-count findings, the witness view can list values held on only one side; the API reference documents the longest-value pane’s length-rank pairing and the binary sample rendering. Systemic-family annotations expose whether their coordinates were persisted or computed for that read; the API reference defines family_signature_shape on findings and signature_shape on family rollups. The distinction is operational only: it does not change the family id or grouping, and no configuration is required. When preparing a disposition package, enumerate a comparison with the naming-only finding_keys shape (or the API’s view=keys) instead of loading evidence the caller will not read. The package response includes the staging-time coverage denominator; read it back to report how much of the comparison the proposed batch actually covers. The public review lifecycle permits one open initial package per comparison, so a second proposal must finish or withdraw the standing package before trying again. See the propose_finding_disposition_package contract for the open_package_conflicts warning returned when a staged item disagrees with another still-open package on the same estate pair.

​

Next

• Overview — what the Prover measures and how its six components fit together.
• How a run works — statuses, provenance, and where to watch.
• Roles and approvals — what lands in front of you and what each button attests to.