Verification

#Verify reports; deploy gates

verify and deploy are separate commands with different jobs:

• bounded verify runs the Z3 prover and prints the full report: every obligation, every counterexample, and the non-blocking advisories. It is your fast feedback loop while you author the policy.
• bounded deploy runs static validation and compilation (a malformed policy, an impossible tier/invariant pairing, or an uncompilable rule is rejected), and the server then re-runs the prover’s deploy gate: a policy whose blocking proof obligations fail is rejected, fail-closed. The previous good policy stays live.

So the workflow is: iterate with verify until every blocking obligation passes and you have reviewed the advisories, then deploy. A DISPROVED blocking obligation is a wall at deploy time. Intentional denies, runtime-safety notes, and unbound attestations are non-blocking advisories left to your judgment.

#Proofs, not tests

A test checks the inputs you thought of. Each obligation below is a statement checked over all modeled inputs: every document state, every payload, every caller. Read each item’s proofStatus; a successful command or a passed: true advisory is not itself a proof:

• PROVED, holds universally; a report entry records the obligation, expression, solver result, and timing. bounded verify does not write local proof certificate files; deploy re-runs the same gate server-side.
• DISPROVED, a concrete counterexample exists, and you get it: the exact variable assignments that break the property. A blocking obligation with this verdict is rejected at deploy.
• UNKNOWN, no proof was established. This is the explicit status for valid runtime-only advisories such as flowBound, windowSum, and a bound over .values. Those rows can be non-blocking and runtime-enforced or maintained, but they are never PROVED.
• UNSUPPORTED / TIMEOUT, the verifier could not encode or finish the obligation. Neither counts as PROVED. Invalid declarations and over-claimed coverage can be rejected by validation; an inconclusive blocking obligation does not pass the deploy gate. A bare-string attestation remains a non-blocking advisory.

checkTautology(amount <= 100 || amount > 100)        DISPROVED  (89ms)
  counterexample: @newData.amount = null

checkAuthRequired(create)                            DISPROVED  (52ms)
  counterexample: @user.id = null,
                  @newData.ownerId = null
  null == null satisfies "ownerId == @user.id"
  suggestion: add "@user.id != null" before the ownership check

The null counterexample above is the canonical example of why this matters: “x ≤ 100 or x > 100” reads like a tautology until a field is missing. No test suite writes that case; the solver finds it in 89ms.

#The obligations table

Rule-property obligations, generated for every collection from its rules:

Invariant proof rows and advisories, generated for declared invariants. Formal transaction postcondition obligations must be PROVED; runtime-only advisory rows stay UNKNOWN and are excluded from the combined formal claim:

Function-auth obligations, generated per declared Bounded Function from its auth rule. Without actAs, function <name>: caller-scoped invocation records that writes run as the verified caller; it is not an admin-only proof. A function with actAs instead emits function <name>: actAs service identity is admin-gated: its auth rule must imply the admin predicate. An over-permissive privileged hatch (auth: "true" or "@user.id != null") is DISPROVED with a non-admin counterexample and blocks deploy.

#The two-layer coverage model

Two distinct layers carry formal claims, with different runtime coverage. Knowing which layer a guarantee lives in tells you exactly where it is enforced.

Layer A, rule properties: one bytecode, one semantics

Auth-required, immutability, dead-rule, implication and counterexample analysis are proven once against your policy expressions, and enforced identically everywhere, because the same compiled rule bytecode executes in every enforcing runtime. Nothing is ported, so nothing can drift.

Layer B, invariants: proof status and runtime reach are separate

The six boundary types and windowSum do not all have the same proof or runtime coverage. PROVED, runtime-enforced, runtime-maintained, and onchain-supported are four distinct claims:

An UNKNOWN row may be valid and non-blocking, but the UI, CLI, SDK, or application must not relabel it PROVED. An onchain bound is not enforced at all. The source program implements more invariant forms than the currently registered v1 deployments; the deploy capability gate rejects newer metadata until the target program is upgraded and registered. See the declaration details on Invariants.

#The honest trust boundary

• Proofs cover declared constraints. An invariant you didn’t declare isn’t proven, bounded verify proposes candidates from your schema, you arbitrate intent.
• The proofs are about modeled policy obligations, not application code being bug-free. A frontend can still be wrong, and runtime-only constraints protect only their documented enforcement surfaces.
• Liveness is not claimed: a proof that invalid writes are rejected is not a proof that every valid write shape is accepted.
• Rolling caps account exactly the events written to the declared append-only scope, spending that bypasses the collection is outside the statement.