Docs / Guides

contract assurance · 80-formal.md · 81-engineering.md · 82-consumer.md · 83-gate.md · guide · card

Assurance

The problem assurance solves

A specification is only useful if the engine follows it. Assurance gathers three kinds of evidence, and each proves something different. Lean, a proof checker, proves properties of a model. A differential test checks that the engine agrees with the model on generated cases. Engineering checks test source changes and search quality. The assurance claim names what it covers and which assumptions it trusts (claim-sentenceassurance.scope-claim.claim-sentenceThe assurance claim reads: these named decisions satisfy these named Lean specifications under these stated runtime assumptions; each list resolves to code paths, constants and components in the tree.).

Models and proofs

Authors write each model definition from the specification text and from no engine source (from-the-specassurance.model.from-the-specEach definition is written from the specification text and derived from no engine source.). Every definition is total, so the model answers every input (total-definitionsassurance.model.total-definitionsEvery definition is total and computable: none is marked partial, noncomputable or opaque, and decidable equality on each finite enumeration is derived.).

The policy proofs cover combining enforcement layers. For example, every member layer admits a row the composed filter admits (composition-soundassurance.prove.composition-soundcomposed_sound: a row the fold over a list admits is admitted by every member of that list.). Each theorem states its negative space: what it leaves open, such as whether execution reaches the filter at all (negative-spaceassurance.prove.negative-spaceBeside each theorem, its negative space states what it leaves open: that the required members were in the list, that a member removes rather than tests, and that execution reaches the fold before an effect.).

The protocol model describes how leases, fenced commits, pauses and crashes change state (protocol-modelassurance.model.protocol-modelThe protocol model is a total, computable step function over two lease paths, the compaction lease guarding a table pointer and the run lease guarding a commit log: grant, raise, renewal, expiry, release, fenced commit, pause, message delay and crash.). A bounded check evaluates every invariant over every short step sequence and prints the shortest breaking one (protocol-checkassurance.model.protocol-checkThe gate evaluates every invariant on each state reached by every step sequence over three nodes and four lease generations; a breaking state raises ProtocolInvariantViolated, printing the shortest sequence reaching it.).

Why a successful build proves too little

Lean compiles a proof that still contains an unfinished step. The assumption audit therefore reads the compiled environment, not the build’s exit status (verdict-inputassurance.audit-assumptions.verdict-inputA verdict is a function of the elaborated environment and the inventory alone; source text, declaration counts and the build's exit status decide nothing.). A proof depending on the hole assumption fails the audit (hole-assumptionassurance.audit-assumptions.hole-assumptionA footprint containing the hole assumption raises ProofHoleAssumption, naming the declaration, whatever its syntax spells.).

A theorem whose statement changed without its inventory entry fails too (statement-driftassurance.audit-assumptions.statement-driftA required constant whose elaborated statement differs from its expected text raises TheoremStatementDrift, printing both.). A recheck rebuilds from pinned source in an environment holding no credential (credential-freeassurance.recheck.credential-freeA recheck environment exposing a token, a signing key or a registry login raises RecheckEnvironmentCredentialed, naming the variable or file carrying it.).

Following one change

A contributor changes zone admission so the allow-set entry on-prem:* rejects on-prem:lab, a zone the specification admits (disjunctiveauthority.place.disjunctiveA zone is admitted when any entry matches. A bare category matches every identifier in it; an entry carrying an identifier matches that identifier alone.).

Zone admission is one of the harness’s decision cases (decision-casesassurance.differential-test.decision-casesA case names one decision: table-pattern coverage, grant narrowing, zone admission against an allow-set, session-zone resolution, or credential admission; a placement decision also carries the zone it resolved.). The harness runs the reference binary, built from the model’s definitions, and the engine’s decision module on each generated case (harnessassurance.differential-test.harnessThe harness drives the reference binary and the decision module's native and WebAssembly builds over each generated case and compares their decisions field by field.).

The reference admits and the engine rejects. The harness shrinks the case to a minimal form and records it (minimizedassurance.differential-test.minimizedA disagreement is shrunk until no single field removal, string shortening or byte removal keeps any two of the three decisions apart, and the minimized case is recorded.). Every later run replays that case before any fresh one (corpus-replayassurance.differential-test.corpus-replayEvery counterexample-corpus case replays before any freshly generated case.).

The full formal stage runs nightly, not on every change (formal-stageassurance.gate.formal-stageThe nightly formal stage runs check-command, command, protocol-check, the protocol differential over 10000 generated cases on both lease paths, and journal-check; a non-zero exit from any reds the run.). A change merged between two nightly runs therefore holds no formal result until the next run.

The claim stays within its evidence. A composition proof offered as a mediation proof fails, because composition says nothing about whether every read passes the filter (mediation-from-compositionassurance.prove.mediation-from-compositionA filter-composition theorem offered as a mediation theorem raises MediationClaimedFromComposition.).

Engineering checks

Enforcement and credential resolution each resolve to one implementation (one-homeassurance.structure-tree.one-homeEnforcement, control-plane state, credential resolution, statement guarding and visibility each resolve to one implementation in the engine; a surface reaches one through the engine route or the registered view compiling it in.). Contributors and the gate run the same typed subcommands (one-pathassurance.automate.one-pathThe gate invokes the subcommand a contributor invokes.).

A change to Rust source adds a test that fails against the base commit (test-firstassurance.test.test-firstA change altering Rust source under crates/ or tools/ adds or alters a test under a package's tests/ that fails against the base commit's source; a change without one raises TestNotFirst.). The gate runs its stages in a fixed order (stage-sequenceassurance.gate.stage-sequenceThe gate runs its stages in order — pins, toolchain, schema, test-first, workspace, acceptance, evaluate, features, crate graph, connectors, TypeScript surfaces, formal, unwired, budget — all of both tiers when none is named, else the named subset, which --plan prints.). A shared target directory recompiles workspace packages per checkout (checkout-artifactsassurance.build.checkout-artifacts.cargo/config.toml names the checkout root, and every workspace package's build script folds its canonical path into the package fingerprint, so a shared target directory recompiles workspace packages per checkout while unchanged dependencies stay fresh.).

Search quality

Evaluation loads its corpus through the real store and retriever (through-the-storeassurance.evaluate.through-the-storeThe corpus loads through the real store, and the retriever under test calls ranked-call with the options a caller passes.). A row a case forbids holds at zero percent of returned rows (forbidden-row-rateassurance.evaluate.forbidden-row-rateA row named in a must-not-retrieve set holds at 0 percent of a regression case's returned rows.). A baseline update only moves entries in the improving direction (raise-onlyassurance.baseline.raise-onlyA baseline update runs after every gate and floor passes, moves each improved entry to its measured value, moves none in the worse direction, and adds no path.).

A backtest replays historical cases. The report places each case by its resolution instant relative to the reader model’s training cutoff (cutoff-sliceassurance.backtest.cutoff-sliceA backtest report places each case by its resolution instant minus the reader's post-training cutoff and states leakage against a declared reference, a cutoff discontinuity or a clean control model, never a bare pre/post gap.). A split removes from training every case whose label interval overlaps a test case’s, and every case starting within the embargo span after a test fold ends (splitassurance.backtest.splitA split purges each training case whose label interval overlaps a test case's, and embargoes each training case starting within a declared span after a test fold ends.).

Forecast tracks keep separate scores and pool into no single figure (tracks-separateassurance.forecast.tracks-separateBacktest, prospective, tool-free and tool-using scores never pool into one figure.). The target ledger ties each measured target to the specification rule it serves (ledgerassurance.measure.ledgerevals/ledger.toml holds one entry per tracked target: an id, an owning clause id, a run-report metric path, a tier, a method naming one integration test, bench target, case set or probe, and a threshold.).

Releases and consumers

contextful-ci tag creates a signed tag only after every release check clears; a dirty working tree fails first (dirty-treeassurance.release.dirty-treeA working tree or index differing from HEAD raises TagTreeDirty.). The conformance suite runs the released artifact through its public surfaces, outside a source checkout (suiteassurance.consumer.suitecontextful-conformance --binary <path> --output <report> executes its versioned scenarios through the supplied artifact's public CLI and HTTP surfaces outside a source checkout.).

A Cloudflare app ships through one hand-dispatched workflow whose single step is the command an operator runs locally (one-commandassurance.deploy-apps.one-commandThe workflow's one run step is contextful-ci deploy cloudflare --app "$APP", the command an operator runs locally with the same two environment variables.); the deploy succeeds only once the app answers its expected status (healthassurance.deploy-apps.healthAfter wrangler deploy, the command repeats an anonymous GET / to the URL wrangler reports until a status in the app's expected set arrives or --health-wait elapses, printing each status alone; the wait elapsing raises DeployUnhealthy, naming the last status.).