Prove, Science & Studio

Open a Prove session WebSocket

Upgrades the connection to a WebSocket for a Backbuild Prove kernel session. The request must carry an `Upgrade: websocket` header. Authentication is handled inside the ProveControllerDO after the upgrade. Browser clients must supply a valid `Origin` header matching the platform's allowed origin list; CLI clients without an `Origin` header are accepted. Each call mints a fresh server-generated session identifier — clients never supply their own. The negotiated sub-protocol is `prove-v1`.

Public Public: no authentication

Parameters

Responses

Prove service health check

Returns a simple liveness response for the Backbuild Prove service. Not authenticated; always returns `200` with `status: healthy` when the Worker is up.

Public Public: no authentication

Responses

Prove service capability information

Returns static metadata about the Backbuild Prove service: version, supported languages, protocol details, primitive rule count, and connection limits. Not authenticated; the response is static and does not reveal per-tenant state.

Public Public: no authentication

Responses

List solver-DAG operations for a scope

Returns all active (and optionally superseded) solver-DAG operations visible at `scope`. The SP applies the project → tenant → global scope walk so that project-scoped operations inherit tenant and global operations. `project_scope_id` is required when `scope=project`. Requires `bbprove.read` permission.

Auth Session JWT (Bearer)

Parameters

Responses

Register a DAG solver operation

Registers a new solver-DAG operation (a named rewrite strategy) at `global`, `tenant`, or `project` scope. The scope walk and permission checks are enforced by the stored procedure: `tenant.write` or `global.write` permission is required. `global` scope writes additionally require platform-staff-level permission (`bbprove.global.write`) which is not held by ordinary organization owners — the SP returns `403 FORBIDDEN` for such attempts. `project_scope_id` is required when `scope` is `project`.

Auth Session JWT (Bearer)

Request Body

Responses

Tag a theorem as a rewrite rule for an operation

Associates a theorem (by `theorem_id`) as a rewrite rule on the given solver-DAG operation. The optional `rule_order` determines priority (lower = higher priority); `direction` constrains the rule's application direction. Requires `bbprove.tenant.write` (or `bbprove.global.write` for global-scope operations) permission.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Remove a theorem rule from an operation

Removes the association between the given theorem and solver-DAG operation. Requires `bbprove.tenant.write` (or `bbprove.global.write`) permission.

Auth Session JWT (Bearer)

Parameters

Responses

Supersede (soft-retract) a solver-DAG operation

Marks the given operation as superseded by `new_operation_id`. Superseded operations are excluded from the default listing (`include_superseded=false`) but remain queryable for audit purposes. Requires `bbprove.tenant.admin` (or `bbprove.global.admin`) permission.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

List test cases for an operation

Returns the static test cases attached to the given solver-DAG operation. Inactive (soft-deleted) test cases are excluded by default; pass `include_inactive=true` to include them. Requires `bbprove.read` permission.

Auth Session JWT (Bearer)

Parameters

Responses

Add a static test case to an operation

Attaches a static LaTeX test case to the given solver-DAG operation. An optional `expected_output` and `oracle_kind` control how the kernel verifier evaluates the test. Requires `bbprove.tenant.write` (or `bbprove.global.write`) permission.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Look up a solver-DAG operation by name

Fetches a single solver-DAG operation by its `(scope, name)` key. The SP applies the scope walk for `project` scope (project → tenant → global). `project_scope_id` is required when `scope=project`. Requires `bbprove.read` permission.

Auth Session JWT (Bearer)

Parameters

Responses

Block a content hash at tenant scope

Suppresses a global DAG content hash at the organization (tenant) level, preventing it from being applied within the org even when it is present in a global operation. `blocked_content_hash` must be a 64-character lowercase hex SHA-256 digest. Requires `bbprove.tenant.admin` permission.

Auth Session JWT (Bearer)

Request Body

Responses

Revoke a tenant-scope content hash block

Removes a previously added tenant-level DAG content hash block, restoring access to the global hash. Requires `bbprove.tenant.admin` permission.

Auth Session JWT (Bearer)

Parameters

Responses

Deactivate (soft-delete) a test case

Soft-deletes a DAG operation test case by setting `is_active=false`. The test case remains in the audit trail and can be retrieved with `include_inactive=true`. Requires `bbprove.tenant.write` (or `bbprove.global.write`) permission.

Auth Session JWT (Bearer)

Parameters

Responses

List DAG theorems for a scope

Returns solver-DAG theorems visible at `scope`. The SP walks the scope hierarchy (project → tenant → global). Optional `name_prefix` prefix-matches on theorem names. Requires `bbprove.read` permission.

Auth Session JWT (Bearer)

Parameters

Responses

Register a DAG theorem

Registers a new theorem in the solver-DAG knowledge base at `global`, `tenant`, or `project` scope. `proof_latex` and `conclusion` carry the formal content; `proof_class` classifies the audit status. Setting `kernel_verified=true` requires platform-staff-level permission (`bbprove.global.write`) — the SP returns `403 FORBIDDEN` for ordinary callers. `project_scope_id` is required when `scope=project`.

Auth Session JWT (Bearer)

Request Body

Responses

Supersede (soft-retract) a DAG theorem

Marks the given theorem as superseded by `new_theorem_id`. Superseded theorems are excluded from default listings but remain queryable for audit and rule-resolution purposes. Requires `bbprove.tenant.admin` (or `bbprove.global.admin`) permission.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Look up a DAG theorem by name

Fetches a single solver-DAG theorem by its `(scope, name)` key. The SP applies the scope walk for `project` scope. Requires `bbprove.read` permission.

Auth Session JWT (Bearer)

Parameters

Responses

Get a document version

Fetches a single document version by its id. The caller must be a member of the owning project. A document the caller cannot see is indistinguishable from a non-existent one (404).

Auth Session JWT (Bearer)

Parameters

Responses

Get per-document AI-check preference

Returns the calling user's AI-check preference override for the given document. `enable_ai_check` is `null` when no per-document override row exists (the effective setting falls back to the per-project default). Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Responses

Set per-document AI-check preference

Upserts the calling user's AI-check preference override for the given document. The SP is idempotent — setting the same value twice is a no-op. Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Clear per-document AI-check preference

Removes the calling user's per-document AI-check override row so the effective setting reverts to the per-user-per-project preference, then the project default. Idempotent — deleting a non-existent row returns `{ was_present: false }`. Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Responses

Get document version history

Returns the full version chain for the document identified by `documentId`. The caller must supply `project_id` and `path` query parameters; these allow the server to locate the chain efficiently and verify that `documentId` belongs to it. Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Responses

Get Backbuild Prove entitlement

Returns the organization's current Backbuild Prove subscription state (enabled, tier, status, included languages, add-ons). Any authenticated org member may call this endpoint without needing an active subscription — it is used by the UI to gate feature rendering. Returns a disabled stub when no subscription exists; returns `503` when the database is transiently unavailable.

Auth Session JWT (Bearer)

Responses

List governance theorem catalog

Returns the platform-wide governance theorem catalog, optionally filtered by `category`, `language`, or `compliance_framework`. Gated by the `governance` feature flag within the Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

Get a governance theorem

Returns a single governance theorem from the platform catalog, including its full formal specification, compliance mappings, and associated proof artifacts. Gated by the `governance` feature flag.

Auth Session JWT (Bearer)

Parameters

Responses

List activated proof languages

Returns the set of proof languages activated for the caller's organization. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Responses

Activate or deactivate a proof language

Activates or deactivates a proof language for the caller's organization. `mode` defaults to `activate` when omitted. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Request Body

Responses

Probe Lean 4 verification service health

Checks whether the platform's Lean 4 cross-validation service is reachable and responsive. Any authenticated org member may call this without an active subscription. The response is always `200` — the `status` field (`ok` or `error`) inside `data` conveys liveness; an `error` value means the service is unreachable or not configured. The `configured` flag distinguishes "not provisioned" from "provisioned but unhealthy".

Auth Session JWT (Bearer)

Responses

Get PDF build status

Returns the current status of a PDF build. JWT + project-membership required; no Prove entitlement gate (viewers must be able to poll regardless of subscription state).

Auth Session JWT (Bearer)

Parameters

Responses

Download a rendered PDF

Streams the rendered PDF for a `done` build. Returns `409 CONFLICT` when the build is in any state other than `done` (e.g. `queued`, `running`, `failed`). JWT + project-membership required; no Prove entitlement gate.

Auth Session JWT (Bearer)

Parameters

Responses

Get PDF build error log

Streams the captured builder log for a failed PDF build. Returns `404 NOT_FOUND` if no error log was captured (e.g. build never ran or the log was not retained). JWT + project-membership required; no Prove entitlement gate.

Auth Session JWT (Bearer)

Parameters

Responses

List project certifications

Returns the certification bundles published to the project, ordered most recent first. A certification records a cryptographically signed snapshot of the project's proof state at a point in time. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

Create (publish) a certification

Publishes a new certification for the project by recording the signed bundle metadata. The bundle bytes must already be in storage (uploaded via the `upload-relay` endpoint). The request body carries the Ed25519 public key, signature, storage key, SHA-256 digest, file hashes, and theorem counts. A `bundle_published` notification is emitted to all Prove notification subscribers for the project. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Revoke a certification

Revokes a published certification. A revocation reason is REQUIRED and must describe the specific grounds. Revoked certifications are flagged on the public verification page. A `bundle_revoked` notification is emitted to all project notification subscribers. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Upload a certification bundle via relay

Receives a `.tar.gz` certification bundle and writes it to storage after running these server-side checks in order: (1) SHA-256 digest verification against the URL `sha` parameter, (2) gzip magic-byte presence (first two bytes must be `0x1f 0x8b`), (3) PDF active-content marker scan on the first 5 MiB, (4) decompression-bomb guard (absolute expansion cap and 100:1 ratio cap), (5) suppression-list check. Payloads that fail any check are rejected with an appropriate `4xx` code. Bundles exceeding 50 MiB are rejected with `413`. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

Get a bundle upload URL

Issues a pre-authenticated upload URL for a certification bundle. The caller provides the SHA-256 hex digest of the bundle; the server returns the relay upload URL and the storage key to use in the subsequent `certificationCreate` call. The upload must be completed via the corresponding `PUT` relay endpoint within the returned `expires_in` window (3600 seconds). Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Run hypothesis-to-theorem promotion engine

Runs the cascading promotion engine for the project: any hypothesis whose obligations are all discharged is promoted to a theorem, which may in turn discharge obligations on other hypotheses. Returns the list of promoted hypothesis IDs and the total count. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

Get compliance dashboard

Returns the project's compliance posture across all attached governance frameworks: overall score, per-framework control status, and top violations. Gated by the `compliance` feature flag.

Auth Session JWT (Bearer)

Parameters

Responses

List proof contracts for a project

Returns the formal contracts (pre/post-conditions, invariants) associated with source files in the project, optionally filtered by `file_path`. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

Get project Prove dashboard

Returns aggregated proof coverage metrics for the project dashboard: total theorems, proven/failing/partial counts, coverage percentage, recent run history, and top-level domain breakdown. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

Get project proof dependency tree

Returns the directed dependency graph of theorems, lemmas, and axioms for the project. Nodes are the individual proof artifacts; edges represent `requires` / `imports` relationships. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

List project discoveries

Returns the project-scoped feed of 5σ discoveries (kernel artifacts where `is_discovery` is true), enriched with first-discovery timestamp and parent hypothesis. Paginated and filtered by a lookback window. JWT-authenticated; no Prove entitlement gate (any project member may view discoveries).

Auth Session JWT (Bearer)

Parameters

Responses

List project documents

Returns documents in the project. By default only the HEAD (latest) version of each document is returned. Pass `head_only=false` to include all historical versions. Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Responses

Save (or no-op) a document version

Persists a new version of a document in the given project. The body carries the full source content; if the content is byte-for-byte identical to the current HEAD the server may return the existing version (no-op). `format` defaults to `pf2` when omitted. Supplying an existing `document_id` anchors the version onto that document chain; omit it to let the server create a new chain.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Upload a document asset (image)

Stream-uploads an image asset into the given document's asset store. The upload pipeline validates in this order: UUID params → document effective-access write-gate → R2 binding check → body size cap → magic-byte image type sniff + dimension/frame/ratio caps + SVG sanitization → content-addressed R2 PUT. Access is gated by project membership and write-grant, not a Prove subscription, so all document authors (regardless of subscription state) can upload images. Knowing the resulting content-addressed `sha256` does not grant read access — delivery requires a re-checked read on the owning document per request.

Auth Session JWT (Bearer)

Parameters

Responses

Deliver a document asset (image)

Streams the immutable image asset identified by its content-addressed `assetSha` (64-character lowercase hex SHA-256). Read access on the owning document is re-checked on every request — a revoked membership cannot use a cached URL to keep accessing assets. Supports `If-None-Match` for conditional GET (304). The `ext` query parameter is required to reconstruct the storage key.

Auth Session JWT (Bearer)

Parameters

Responses

Submit a document for PDF rendering

Submits the HEAD version of the given document for asynchronous PDF rendering. A new `bbprove_pdf_builds` row is created with status `queued` and a build job is enqueued. If `idempotent` is true (default) and a `done` build for the same input already exists, that build is returned immediately with `reused: true`. `queue_warning` in the response is non-null when the internal build queue was unavailable — the row is still created and can be replayed. Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Upsert a document draft

Creates or replaces the in-progress draft for the given `(project, path)` tuple. There is at most one draft per `(org, project, path)`; every PUT overwrites the previous draft body. Returns persisted metadata only — content is not echoed to minimize auto-save response size. Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Get a document draft

Fetches the in-progress draft for `(project, path)`. Always returns a stable envelope: `{ exists: false }` when no draft is present; `{ exists: true, draft: { ... } }` otherwise. The `:path` segment must be URL-encoded by the caller. Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Responses

Discard a document draft

Discards the in-progress draft for `(project, path)`. Idempotent — `{ discarded: false }` is returned when no draft existed. Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Responses

Publish a document draft

Atomically materializes the in-progress draft into a new document version and clears the draft. If no draft exists for the given `(project, path)`, returns `404 NOT_FOUND` with `error.sub_code = 'PUBLISH_NO_DRAFT'`. If the draft's base version is stale (another commit landed since the draft was saved), returns `409 CONFLICT` with `error.sub_code = 'PUBLISH_CONFLICT'` and `error.details` carrying `{ current_head_version_id, current_head_version, draft_base_version_id, draft_base_version }` to enable a 3-way merge in the editor. Requires an active Backbuild Prove entitlement.

Auth Session JWT (Bearer)

Parameters

Responses

Enable Backbuild Prove for a project

Initializes Backbuild Prove on an existing project, creating the necessary database rows and default settings. Idempotent — calling it on an already-enabled project is a no-op. Requires an active Backbuild Prove subscription and membership in the project.

Auth Session JWT (Bearer)

Parameters

Responses

List governance theorems attached to a project

Returns the governance theorem attachments for the project, including the severity override and current compliance status. Gated by the `governance` feature flag.

Auth Session JWT (Bearer)

Parameters

Responses

Attach a governance theorem to a project

Attaches a governance theorem from the platform catalog to the project. An optional `severity_override` controls whether violations are reported as `warning`, `error`, or `ignored`; the catalog default is used when omitted. Gated by the `governance` feature flag.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Detach a governance theorem from a project

Removes a governance theorem attachment from the project. Gated by the `governance` feature flag.

Auth Session JWT (Bearer)

Parameters

Responses

List governance violations for a project

Returns paginated governance violations — instances where the project's proof state does not satisfy an attached governance theorem. Optionally filtered by `attachment_id` and whether to include resolved violations. Gated by the `violations` feature flag.

Auth Session JWT (Bearer)

Parameters

Responses

Suppress (accept exception for) a governance violation

Marks a governance violation as suppressed (accepted exception), recording the justification reason. Suppressed violations are excluded from default violation counts but remain in the audit trail. A `reason` of 1–2000 characters is required. Gated by the `violations` feature flag.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Get the user's persisted graph layout

Returns the calling user's persisted node positions and viewport for the project's proof artifact graph. Layouts are keyed per `(organization, project, user)` — each collaborator has independent node positions. Returns `null` under `data` when no layout has been saved yet (the client falls back to an automatic Verlet-physics layout). JWT-authenticated; project membership required.

Auth Session JWT (Bearer)

Parameters

Responses

Save the user's graph layout

Upserts the calling user's node positions and viewport for the project's proof artifact graph. Sending an empty `nodes` array with no `viewport` fields deletes the stored layout (reset to automatic Verlet-physics). JWT-authenticated; project membership required.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Get handoff contract report

Generates a handoff contract report for the project: a structured, machine-readable summary of all proven contracts suitable for passing to an external system, audit, or release gate. Pass `include_unaudited=false` to exclude contracts that have not completed the audit workflow (defaults to including them). Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

Register a hypothesis

Registers a named hypothesis with its discharge obligations, `\impliedfrom` links, and `\dischargedby` declarations. `source_file_path` is canonicalized server-side for path confinement. `obligations` carries the structured formal conditions that must be discharged for the hypothesis to be promoted to a theorem. `implied_from` lists hypothesis labels that imply this one. `dischargedby` can reference existing labels or forward references (by kind + name). Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Get hypothesis discharge status graph

Returns the full hypothesis/obligation/implication/promotion graph for the project: each hypothesis with its discharge obligations, current promotion state, and `\impliedfrom`/`\dischargedby` edges. Used by the dashboard to render the hypothesis discharge state. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

List proof issues for a project

Returns paginated proof issues (type errors, failing theorems, lint warnings) for the project, with optional filters by file path, language, and domain. Page/page_size pagination (default page 1, page_size 50). Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

List Lean 4 verification reports

Returns Lean 4 verifier reports for the project, with optional filtering by `filter` (e.g. `errors`, `warnings`, `all`) and `file_path`. Gated by the `lean4` feature flag within the Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

Get project notification settings

Returns the notification channel configuration and event filters for the project. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Responses

Update project notification settings

Updates the notification channel configuration and event filters for the project. All fields are optional — only provided fields are updated. `cooldown_minutes` controls the minimum gap between repeated notifications for the same event type (0–1440). Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

Sync a paired-repository document manifest

Bulk-syncs the document manifest from a paired external repository into the platform's document catalog. The `org_id` is always derived from the authenticated session — the body must not include it. A manifest may contain up to 5 000 file entries. Each entry's `rel_path` is re-canonicalized server-side for path confinement. Pass `prune: true` to remove catalog entries for files absent from the manifest. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

List PDF builds for a project

Returns PDF build records for the project, most recent first. Optionally filter by `document_id` or `status`. JWT + project-membership required; no Prove entitlement gate.

Auth Session JWT (Bearer)

Parameters

Responses

Get project PDF build defaults

Returns the per-project default PDF build settings (theme, primary language). JWT + project-membership (viewer level) required; no Prove entitlement gate so viewers always have access to display the Build PDF UX defaults.

Auth Session JWT (Bearer)

Parameters

Responses

Upsert project PDF build defaults

Persists per-project PDF build defaults (theme, primary language). Requires JWT + Backbuild Prove entitlement. Editor-level membership is enforced inside the stored procedure. At least one field must be present; unknown fields are rejected (`additionalProperties: false`).

Auth Session JWT (Bearer)

Parameters

Request Body

Responses

List project predictions

Returns the predictions for the given project, optionally filtered by parent hypothesis. Predictions are created by the kernel from `\prediction{...}` macros in the document source — they are not directly mutable via this API. JWT-authenticated; project-membership enforced inside the stored procedure.

Auth Session JWT (Bearer)

Parameters

Responses

Get a prediction

Returns a single prediction with its structured observables and computational evidence. JWT-authenticated; project-membership enforced inside the stored procedure. If the returned prediction does not belong to the URL `projectId`, `404 NOT_FOUND` is returned.

Auth Session JWT (Bearer)

Parameters

Responses

Set proof class for theorems

Bulk-updates the proof class of theorems to `unaudited`, `audited`, or `public_api`. Exactly one of `theorem_ids` (array of UUIDv7s) or `theorem_names` (array of strings) must be supplied. Requires an active Backbuild Prove subscription.

Auth Session JWT (Bearer)

Parameters

Request Body

Responses