Verification Inventory

This page is the authoritative inventory for verification counts. Only counts that are stable enough to check automatically are tracked here.

The goal is to track coverage of key system properties and regression gates, not raw unit-test volume.

When one of these values changes legitimately:

1. update the underlying source of truth,
2. refresh this page,
3. rerun just check-verification-inventory.

The numeric rows in this section are source-derived and checked by toolkit/xtask/src/checks/verification_inventory.rs.

Current Formal Verification Claim

Telltale is formally verified for the declared shipped surface documented in this inventory, under the assumptions listed in the public TCB ledger below.

The exact public claim is:

Telltale is formally verified for its declared shipped surface: the Lean session-type, projection, protocol-machine, and conservation-property models and theorems, the theorem-defined Rust↔Lean protocol-machine runtime correspondence core for the audited supported corpus, the shipped first-party handler/transport boundary as documented by machine-checkable contract profiles, and the shipped first-party crate artifacts through the audited artifact-correspondence pipeline.

This does not mean every Rust API, compiler helper, macro path, plugin, or third-party integration is mechanically proved. Anything outside the declared shipped surface is listed explicitly below and is not part of the formal claim.

The runtime heap now has a focused Lean parity lane for canonical bytes, tagged preimages, ordering, proof-path structure, and deterministic replay. Its digest algorithm remains an operational conformance surface checked through published vectors and runtime tests rather than a first-class Lean hash model.

The simulator assurance story now includes explicit exact-backend parity, canonical replay reproduction, exact checkpoint resume, durable WAL fault injection and crash/recovery matrices, batch-order reproducibility, fail-closed theorem-classification matrices, approximation admissibility gates, nested distributed invariance, and helper-surface non-authoritativeness checks. These remain executable assurance lanes rather than part of the current mechanized formal claim.

The search crate now has a scoped Lean fairness lane as well. The current proved search fairness surface is:

• canonical serial search is exact one-step fair for the current legal min-key batch
• canonical serial search now has an executable reduced machine semantics plus an explicit reduced Rust-facing state/artifact projection boundary
• canonical serial search now also has an executable full-machine semantics, an exported full-state artifact projection, and premise-scoped full-step refinement contracts back into the reduced executable lane
• canonical serial search now also has a reduced machine-level invariant and projection layer, including executable machine-step invariant preservation, executable trace refinement into the packaged machine theorem surface, and a machine-trace restatement of current min-key eventual service
• canonical serial search also has a dynamic liveness theorem under an explicit stability premise: if an entry remains continuously eligible and no strictly better entry appears, it is eventually serviced
• canonical serial search has a fixed-phase termination theorem under an explicit finite reachable-node premise bundle
• canonical serial search also has a rebuild-aware ARA-style termination theorem under an explicit lexicographic phase/work measure premise bundle
• canonical serial search has both bounded strict-preemption and finite better-entry exhaustion theorems for entries that are not initially in the current min-key batch
• canonical serial search now also has a scheduler-facing non-min service theorem whose public statement no longer exposes bounded-better-arrival or finite-better-universe terminology
• canonical serial search has both frontier-level and machine-level witness-path goal-reachability theorems for the reduced model
• canonical serial search now also has a graph-reachability-driven completeness theorem under explicit reachable-path, finiteness, and heuristic premises
• canonical serial search now also has a raw-successor-semantics completeness theorem whose public statement quantifies over the domain successor contract instead of a user-supplied ready-path witness
• canonical serial search also has an explicit machine-level bridge from goal reachability to incumbent publication under a publication premise bundle
• canonical serial search now also has an eventual optimal-goal publication theorem under explicit admissibility and consistency premises
• threaded exact single-lane search has the same exact one-step fairness through reduced one-step, commit-trace, state-slice, and observation-slice refinement theorems to canonical serial search
• batched exact search has a certified-window fairness theorem with explicit premises plus a bounded dynamic starvation-freedom theorem under an explicit bounded-preemption premise, and its theorem-pack/export surface now also carries explicit support-class metadata alongside the certified multi-step window-trace validity theorem
• envelope-bounded batched search now also has a certified-window theorem surface, theorem-backed normalized-commit observables, and a runtime certificate/export path aligned with the theorem pack

These search fairness claims are exposed operationally through the SearchFairnessArtifact and SearchFairnessCertificate runtime surfaces and checked by the dedicated just check-search-fairness gate, the Rust↔Lean search parity suite, and the verification-inventory gate. The current theorem pack is a first-class Lean artifact under Runtime.Proofs.Search.TheoremPack, with a mirrored Rust SearchTheoremPackArtifact for release-facing inventory export, now including per-theorem support classes that distinguish executable-semantics theorems, refinement corollaries, and premise-scoped theorems. Exact runtime runs now also export SearchStateArtifact plus per-round state/certificate traces. They also export SearchRouteBoundArtifact, whose current discovery surface is an observed run-scoped bound to first candidate publication, an observed recovery bound after the latest epoch transition, and a theorem-backed one-step goal-window service bound from the fairness certificate surface, now packaged as a structured SearchRouteDiscoveryCertificate and attached to the exact observed goal-window and publication steps for that run. The selected-route summary also carries a stable generic metric list alongside its scalar convenience fields. Its current quality surface remains profile-scoped rather than a separate Lean end-to-end discovery theorem. The release/provenance lane records the generated target/search-theorem-pack/search-theorem-pack.json artifact plus the generated canonical vector artifact target/search-artifacts/search-vectors-v1.json and the generated recovery vector artifact target/search-artifacts/search-recovery-vectors-v1.json. These claims are also backed by source-controlled search artifact vectors checked by the search_vectors and search_recovery_vectors conformance tests. They are still narrower than a blanket proof of fairness and completeness for all future frontier growth, all rebuild schedules, and all parallel modes without premises.

Claimed Surface

The current proved or proof-backed claimed surface is:

• the Lean SessionTypes, SessionCoTypes, Choreography, Protocol, and Runtime models and theorem libraries
• the strict Rust↔Lean correspondence corpora and comparison contracts tracked in the Lean correspondence rows below
• the first-class protocol-critical capability/finalization/transition model carried by the Lean capability-model surface and its strict Rust↔Lean bridge correspondence suite
• the packaged first-party crates and binaries only at the level of operationally checked artifact/release assurance, not full mechanized proof

Compiler and Macro Claim Boundary

The current public formal-verification claim does not include any Rust parser, lowering, projection, import/export, or macro-expansion entry path. More concretely: the current public formal-verification claim does not include any Rust parser, lowering, projection, import/export, or macro-expansion entry path.

For the current claim:

• parse_choreography_str, parse_choreography_file, choreography_to_global, local_to_local_r, Rust-side projection/codegen/import-export helpers, and tell! macro expansion are outside the formal claim
• because those entry paths are outside the current formal claim, no compiler-facing theorem-object JSON/import-export path remains on the current claim-critical path
• those Rust compiler and macro paths are still covered by strict operational gates, especially the compiler-pipeline, projection-equivalence, exact-shape JSON, Lean-validator, and macro-UI suites
• the exact DSL fragment that would need mechanized compiler proof before the public claim can broaden is the theory-convertible subset already tracked in the property table below: straight-line send/recv, communicated choice, call, counted loop, and guarded recursion
• par, case/of, timeout, and any other fail-closed or runtime-only forms are outside both the current formal claim and that future proof-target subset

Artifact Correspondence Claim

For the current public claim, the shipped first-party crate artifacts are covered only by operational artifact correspondence, not by mechanized proof.

More concretely, the current release/artifact claim is:

• every publishable first-party crate tarball for the released version is built from the checked workspace manifests for that version
• the packaged tarballs compiled by the artifact lane are the same tarballs whose hashes, sizes, git revision, toolchain versions, and critical embedded resource hashes are recorded in the provenance manifest under target/package-artifact-tarballs/provenance.json
• critical embedded resources on the shipped path, including packaged README files, the embedded runtime grammar, and release metadata like the WASM example lockfile, are part of the audited artifact pipeline rather than an unchecked side channel

This is still narrower than a fully reproduced, mechanically proved binary build pipeline. Cargo, crates.io, git hosting, and the local build toolchain remain explicit external assumptions.

Out of Scope / Assumption Boundaries

First-class protocol-critical capability semantics are in scope. General host application authorization is out of scope.

The current public claim does not include:

• Rust parser/lowering/projection/import-export and tell! macro expansion
• user-supplied handlers, transports, plugins, or deployment adapters
• third-party infrastructure or deployment environments
• Cargo, crates.io, git hosting, OS, compiler, and toolchain correctness beyond the documented operational checks
• cryptographic hardness assumptions beyond standard SHA-256-style assumptions
• a blanket claim that every shipped Rust code path is mechanically proved
• general host application authorization or arbitrary app-policy capability systems unrelated to protocol-critical semantics

Final Surface Audit

This table is the final public audit of which major surfaces are inside the formal claim and which are deliberately outside it.

Public TCB Ledger

The current trusted computing base for the public claim is:

If that TCB shrinks or the claim broadens, this section must be updated before a broader public wording is used.

Final Public Claim Text

Use this exact wording in docs, release material, and summaries:

Telltale is formally verified for the declared shipped surface documented in the verification inventory, under the listed public assumptions and TCB.

Supporting scope statement:

The declared shipped surface includes the Lean semantics/theorems, the theorem-defined Rust↔Lean protocol-machine runtime correspondence core, the shipped first-party handler/transport contract boundary, and the shipped first-party crate artifacts through the audited artifact-correspondence pipeline. It does not include Rust compiler/macro entry paths or third-party integrations unless stated otherwise.

Supporting TCB statement:

The remaining public TCB consists of the Lean kernel and imported proof libraries, the minimized Rust/Lean bridge/interchange layer, the comparison- checked Rust runtime implementation for the claim-critical surface, the documented first-party handler/transport boundary, the audited release/package and generated-resource pipeline, and external build/delivery infrastructure such as Cargo, crates.io, git hosting, and the underlying toolchains.

Refinement Coverage Map

This map names the current protocol-machine state surfaces that matter to the claimed runtime story and shows whether they are already inside the exact Rust↔Lean refinement slice.

Gate Ownership

The verification surface is organized around three canonical just-entry lanes. just ci-dry-run, check.yml, and verify.yml should call these names rather than duplicating their inner gate lists by hand.

For staged diffs restricted to the simulator subsystem, the narrower local gate is now just check-simulator-subsystem-staged. That path is intentionally local-only and does not replace the canonical repo-wide lanes above. It exists so simulator-only staged work still gets formatting, compile, test, and simulator-doc link enforcement without being blocked by unrelated pre-existing breakage elsewhere in the workspace.

The dedicated local search-fairness gate is just check-search-fairness. That gate is intentionally narrower than the canonical repo-wide lanes above and exists to keep the Lean theorem-pack, parity fixture, and inventory rows aligned while working inside telltale-search.

Property Coverage Baseline

This baseline records whether each conserved-property bucket has at least one high-signal executable assurance suite today. It is intentionally curated. The aim is to make gaps explicit rather than to produce vanity totals.

Bridge Normalization Trust Surface

The Lean bridge still contains a small amount of trusted normalization logic. That logic is intentionally narrow and is audited explicitly in CI by just check-bridge-normalization. The rows in this table are source-derived and checked by telltale_bridge::bridge_normalization_ledger() via toolkit/xtask/src/checks/bridge_normalization_ledger.rs.

Enforcing artifacts:

• rust/bridge/src/protocol_machine_trace.rs
• rust/bridge/tests/protocol_machine_correspondence_tests.rs
• rust/bridge/tests/protocol_machine_differential_steps.rs Session-status ordering is no longer part of the trusted comparison surface. Both the Lean runner and Rust-side correspondence harness now emit session rows in canonical sid order, so comparison is exact rather than normalized.

The older schema_version backfill helper remains only as a test-only compatibility shim for legacy fixture coverage. It is outside the claim-critical bridge surface and must not synthesize semantic content.

Explicit Unsupported / Fail-Closed Notes

No explicit unsupported or fail-closed implementation-gap notes remain in the tracked inventory. New notes should be added here only for intentional, documented non-goals or for temporary regressions that are not yet executable.

The inventory deliberately does not track raw unit-test totals, assertion counts, or line counts for tests.