TLA+ Specifications · TLC Model Checking · Receipt v2 Staged Roadmap
Formal TLA+ models in the ACGS workspace verify state-machine invariants under explicit network and provider assumptions. They complement—and never replace—runtime tests, cryptographic key management, and deployment controls.
01 · External-Effect Contract Taxonomy
UNKNOWN depends on the provider.When a tool call times out after leaving the local process, no local state machine can deduce on its own whether the remote API executed the action. The TLA+ models classify external providers into four contract classes.
The provider accepts a grant-bound idempotency key (acgs:effect:v1:<sha256>) and exposes an atomic query_and_fence(key) operation that either confirms prior execution or permanently blocks late arrival of that key.
The provider has no explicit cancel/fence endpoint, but enforces a server-side request expiry deadline D and supports status lookup by key. Waiting until t_send + D + ε (maximum clock skew) before querying status acts as a time-based fence.
Two-phase candidate staging and atomic store commit (COMMITTED | DENIED | CONFLICTED) with post-commit outbox delivery.
Providers without idempotency keys, fencing, or bounded delivery cutoffs cannot safely transition from UNKNOWN to NOT_DONE without human or out-of-band reconciliation.
02 · TLC-Checked Safety Invariants
∀ g ∈ Grants : Cardinality({e ∈ providerExecuted : KeyGrant(e) = g}) ≤ 1At most one external side effect can execute per issued grant across any sequence of network timeouts, retries, and reconciliations, provided the provider honors the idempotency key and query_and_fence contract.
∀ k ∈ EffectKeys : state[k] = "NOT_DONE" ⇒ k ∉ providerExecuted ∧ k ∈ providerFencedThe local store never transitions an effect to NOT_DONE (and never releases its reserved budget) while the request could still execute on the remote provider.
settled + reserved ≤ capacity ∧ settled = SumExecuted(DONE) ∧ reserved = SumHeld(RESERVED ∪ IN_FLIGHT ∪ UNKNOWN)Total settled plus in-flight/unknown reservations never exceeds the configured EffectBudget capacity. Unconfirmed timeouts hold their reservation until fenced.
03 · Multi-Agent Coordination Specs
Acgs-Swarm maintains formal TLA+ specifications covering its Atomic Proposal & Constitutional Commit (APCC) protocol, peer-vote settlement quorum, and governed handoff state transitions.
Inspect Acgs-Swarm/specs on GitHubKey Boundary · APCC Outbox vs. External Provider Effects
In Acgs-Swarm/specs/apcc.tla, committing a candidate state atomically records the decision and queues an outbox entry inside the authority store (SQLite default, optional PostgreSQL 17). That guarantees internal state-commit consistency—it does not by itself turn an arbitrary third-party HTTP endpoint into a FENCEABLE provider.
04 · Staged Engineering Branch (Pre-Release)
Published PyPI packages today target acgs-lite==3.0.1 (with slices A1–A3 on main at 0cd5e56). A semver-major 4.0.0 branch (26 commits, verified by 7,791 unit tests and two security-review rounds) stages the following hardening changes and explicit residual limits:
Commits the server-assigned grant_id alongside policy_digest, method_qualname, argument_digest, and context_digest while preserving v1 byte compatibility.
GovernedCallable(authorization_profile=PRODUCTION) requires a non-ephemeral Ed25519 receipt_signer and trusted_execution_keys pinned with execution scope; missing either raises LegitimacyInvariantError.
GovernedCallable and GovernedAgent deny non-JSON objects (GOVERNANCE-PAYLOAD-UNEVALUABLE) and oversize payloads (GOVERNANCE-PAYLOAD-OVERSIZE) instead of truncating previews.
Rule matching unions verdicts over the original text and NFKC-normalized text with Unicode 16.0.0 Cf and Default_Ignorable_Code_Point characters stripped, closing zero-width and fullwidth evasion.
Recomputes argument_digest immediately before invoking the callable to detect post-grant mutation, and records KeyboardInterrupt / SystemExit / GeneratorExit as PARTIAL or FAILED rather than leaving attempts STARTED.
Documented Residual Limits (Not Claimed in 4.0.0)
governance_action still selects conditional rules.Cf normalization strips zero-width and fullwidth evasions but does not map cross-script homoglyphs (such as Cyrillic lookalikes).acgs-lite>=3.0.1,<4 and will require a <5 pin bump once 4.0.0 is published to PyPI.Choose one tool. Define what it may do. Inspect what happens when a request crosses the boundary.