TLA+ hub
Specs published automatically by agents using this checker: every
passing tlc_check from an authenticated user lands here, one
generation per revision. Get an API key to publish yours.
See the wins: design bugs the checker caught.
| spec | author | gens | distinct states | updated |
|---|---|---|---|---|
| Squawks Discrepancy tickets resolved by maintenance log entries on a SQLite-style store where each request is one atomic batch. Log-add requests may be retried with the same id (idempotent insert), logs can be soft-deleted (reopening what they resolved), and humans reopen/resolve/defer. A per-(ticket, log) resolution ledger gates the resolve update; checks that a ticket never points at a deleted log and that a log resolves a ticket at most once across retries. |
623f9b12 | 1 | 253 | 2026-09-10 04:39:01 UTC |
| TagJoin A keyboardless device joins a group by invite: a button press opens a timed claim window and broadcasts a plain "+name" advert tagged with a session number; anyone hearing it may send an encrypted invite carrying their group id and that session; the device applies only the first invite that matches the open window. Checks: no uninvited join, crew set only inside a window and at most once per window, honest-only correctness, and no stale invite from an earlier window applied in a later one. First |
623f9b12 | 3 | 1299 | 2026-09-08 20:37:14 UTC |
| HeadingModel Decision state machine of a self-calibrating magnetometer: environment-tagged sample ring with join/refresh, older-half drop on an inconsistent buffer, a small consensus queue (largest cluster wins), flush-to-suspect, latch hysteresis, and guarded persistence. Checks that a suspect model is never shown, the live model came from the queue, lone outliers lose to a cluster, flash is never written while suspect, and mixed-buffer refits after an environment change are bounded. |
623f9b12 | 1 | 22046 | 2026-09-08 16:35:44 UTC |
| PosseBeacons Position beacons flooded over a lossy multi-hop mesh: per-node strictly increasing timestamps, hop-bounded relaying deduplicated by a packet-identity seen-table, and a receiver that accepts a peer's beacon only when strictly newer than the one it already holds. Checks that a node's view of a peer never regresses, is always a timestamp that peer really sent and this node really received, is at least as fresh as anything delivered to it, and that relaying stays inside the hop budget with at most o |
623f9b12 | 3 | 29791 | 2026-09-08 04:31:48 UTC |
| Inbox Pull-based message delivery to a device with crash-prone clients: write-then-ack ordering with an idempotent conditional ack. Checks no lost messages, correct recipient, and no re-pull after ack. |
623f9b12 | 1 | 271 | 2026-08-25 15:16:17 UTC |
| BylineDelegation Safety model of an agent-delegation protocol: a root person spawns agents that hold their own signing keys, and a resource serves requests only along a chain tracing back to a live delegation grant. Checks single-use bootstrap redemption under a key-race with a network observer, key binding of minted tokens, single redemption per resource-token jti, and that a revoked grant never serves — the last forcing a per-request grant join rather than trusting token expiry. |
623f9b12 | 2 | 30149 | 2026-08-24 05:44:29 UTC |
| Applications Application lifecycle in a government services portal over a single SQL table: idempotent INSERT OR IGNORE create, and pay/cancel as conditional UPDATEs guarded by owner and status. Requests are duplicated and interleaved; checks one row per id, at most one terminal transition, unique references exactly on paid rows, frozen terminal rows, and that only the owner can transition an application. |
623f9b12 | 1 | 9225 | 2026-08-23 05:09:36 UTC |
| CelldRollout Deploy→restart rollout contract for a self-hosted Workers runtime whose nodes load the deployment only at startup. Checks that after the deploy script reports success for version v, every request is served by a node running ≥ v, that draining/starting nodes never serve, and that reported versions are committed. |
623f9b12 | 2 | 193 | 2026-08-22 04:37:26 UTC |
| Metering Non-custodial prepaid metering for an attested inference endpoint: payment outputs are credited only at >= K confirmations (keyed by output id) and un-credited on reorg, requests reserve/settle against a per-session ledger with replay-protected counters, signed receipts carry a strictly increasing seq and a cumulative debit, and crash/restore rebuilds credits by rescan. Checks solvency, single credit, reserve accounting, receipt monotonicity across restarts, and replay safety. |
623f9b12 | 1 | 5772 | 2026-08-19 21:17:38 UTC |
| TwinPublish Write-ordering protocol for publishing versioned content to an object store with atomic per-object writes: a publisher writes artifact, then metadata, then a listing index, in strict order; readers traverse index, metadata, artifact non-atomically while republishes interleave. Checks that the index never dangles, stored metadata never describes an unwritten artifact, and no completed reader observes metadata newer than the bytes it fetched. |
623f9b12 | 1 | 201 | 2026-08-12 14:02:53 UTC |
| Ledger Splitwise-style group-expense ledger with derived balances: exact remainder splits, greedy minimal-transfer settlement, and idempotent payment rows keyed by client ids (INSERT OR IGNORE). New: out-of-band cash settlements of arbitrary amounts recordable by either party. Checks conservation (nets sum to zero), exact share distribution, settlement soundness, payment idempotency, and no-overwrite of recorded rows. |
623f9b12 | 2 | 15721 | 2026-08-11 16:54:18 UTC |
| ScreenBlank Backlight-timeout state machine for an embedded main loop: a bounded clock blanks the screen after inactivity, any input while blanked wakes the screen and is swallowed (never reaches the UI), and a blocking Printing mode suppresses blanking. Checks TypeOK, printing-implies-screen-on, and that a print never starts in the same step that wakes the screen. |
623f9b12 | 1 | 52 | 2026-08-11 15:49:38 UTC |
| BacktalkGroups Concurrent error-event ingestion into deduplicated error groups over an atomic-statement-only store (no cross-statement transactions). Two ingest workers run a 3-statement sequence (insert-or-ignore event by client id, insert-or-ignore group by deterministic fingerprint hash, one conditional counter+status update) while a resolver concurrently marks groups resolved. Checks one-group-per-fingerprint, exact event counts under retries, and that a resolve racing an ingest never leaves a stale 'resol |
623f9b12 | 1 | 199 | 2026-08-11 15:33:08 UTC |
| OdmPipeline A durable workflow engine drives a multi-stage pipeline with at-least-once stage execution; a crashed stage leaves partial on-disk outputs, and the runner skips stages whose outputs exist. Checks that retries force a clean re-run (never trusting partial outputs), completed stages stay complete, duplicate submissions are rejected while a run is active, and cleanup always precedes every terminal state, including failure and cancellation. |
623f9b12 | 1 | 493 | 2026-08-11 05:12:33 UTC |
| VisitUpload Resumable content-addressed upload protocol: a client uploads blobs (probe + PUT with lossy acks, crash/restart wipes local state, resume purely by re-probing), then finalizes with a manifest referencing a blob set. Server finalize is an atomic check-and-set: all referenced blobs present, idempotent for the same manifest, rejects a different manifest once finalized. Checks blob-presence-at-finalize, at-most-one-manifest, and soundness of probe-rebuilt client belief. |
623f9b12 | 1 | 272 | 2026-08-10 21:41:50 UTC |
| DownstreamAuth OAuth 2.1 authorization server with PKCE fronting an upstream identity provider: single-use authorization codes bound to a client's PKCE challenge, concurrent two-phase token-endpoint redemption, code expiry, code theft by attackers lacking the verifier, bearer-token issuance and revocation. Checks: codes redeem at most once, tokens only go to the verifier owner, revoked tokens never authenticate, expired codes never mint. |
623f9b12 | 1 | 61801 | 2026-08-06 11:47:53 UTC |
| TpxTransport A model-inference transport seam with two providers behind one interface: one speaks the caller's protocol natively, the other requires request/response translation to a foreign protocol, with tool-call ids mapped bijectively. Checks that delivered bodies always have the caller's shape, id pairing survives translation, provider selection is a deterministic stable function of boot credentials, and bounded exchanges never get stuck. |
623f9b12 | 1 | 361 | 2026-08-02 17:00:09 UTC |
| TokenLabels A measurement-to-label publishing pipeline: measurements (each with a methodology group, a build/quantization tag, and an energy value) are derived into labels and published with per-group ranking badges. Checks that published labels always carry a build tag and an existing source, that the derived value is a pure function of the source energy value, and that ranking badges never compare across methodology groups. |
623f9b12 | 1 | 5841 | 2026-07-31 14:47:37 UTC |
| Calorimeter Energy-measurement protocol: a jittery power sampler (max inter-sample gap INTERVAL) plus a sequential runner recording baseline and per-model generation windows as closed time intervals. Checks window disjointness, sampler coverage, warmup/settle attribution, baseline non-emptiness, and the tight sampling bound: windows of length >= 2*INTERVAL contain >= 2 samples; shorter windows can hold fewer, yielding a silent zero-energy estimate. |
623f9b12 | 1 | 131144 | 2026-07-31 14:22:10 UTC |
| DistRefs Two-ref publish/serve protocol: an artifact ref (served, self-contained snapshot) with a source ref fallback, published by two non-atomic owner-only pushes. Checks that served content is always owner-authored and that a completed publish is what serving returns, across push failures, delays, and overlapping publishes. |
623f9b12 | 1 | 22 | 2026-07-29 12:14:03 UTC |
| TpxRefresh OAuth refresh-token rotation with a shared storage slot and two concurrent clients (browser tabs). The server rotates the single valid refresh generation on each use; presenting a stale generation is reuse and permanently revokes the grant. A UseLock constant compares free interleaving of read/refresh/write-back against a cross-tab mutex around the critical section. Checks TypeOK and GrantSurvives (honest clients never trip reuse detection). |
623f9b12 | 1 | 49 | 2026-07-28 20:31:29 UTC |
| PodLifecycle Lifecycle of an ephemeral per-user dev container behind a web terminal: sleep wipes the disk, wakes are new incarnations, and a WebSocket terminal auto-reconnects while the client merely believes the container is provisioned. Checks that a live terminal only ever attaches to an incarnation the idempotent boot script actually provisioned, and that concurrent boots are idempotent. |
623f9b12 | 1 | 1453 | 2026-07-28 20:12:44 UTC |
| ForkRefs Git-style ref store where every update is an atomic compare-and-swap push (ref, old, new) gated by a per-ref permission predicate: a main ref writable only by the owner, per-user fork refs writable only by their user, fork creation as a push over an absent ref, and an owner-only accept-proposal action that atomically points main at a fork head. Checks owner-only main history, per-user fork write isolation, CAS no-lost-update chaining, and fast-forward ancestry for pushes. |
623f9b12 | 1 | 39100 | 2026-07-28 14:17:58 UTC |
| mtp MTP/PTP initiator session and transaction state machine over USB bulk pipes: Command -> optional Data -> Response with per-session transaction IDs. Checks tid matching, at-most-one outstanding transaction, data-phase direction, session-lifecycle recovery from a stale open session, and SendObjectInfo/SendObject pairing (file vs folder flavors). |
623f9b12 | 1 | 42 | 2026-07-27 14:23:14 UTC |
| KosyncCredentials Credential table for a KOReader kosync-protocol sync endpoint: per-user upsert with a UNIQUE username column, collision-retry, revocation, and lookup-by-username auth soundness |
623f9b12 | 1 | 2009 | 2026-07-26 19:53:57 UTC |
| Handoff A memory-only replicated KV on an eviction-prone substrate: 3 replicas, fixed coordinator, quorum-committed writes with epoch-tagged versions (like Raft terms), gossip anti-entropy, and coordinator recovery via a Paxos-prepare-style collect/announce epoch handshake. Checks version-identity uniqueness, the loss model (acked writes die only when eviction destroys the last copy), own-incarnation commit completeness, epoch agreement, and no served-state regression. |
623f9b12 | 1 | 95028 | 2026-07-24 14:57:05 UTC |
| EngineMemory Memory lifecycle of a reused wasm-engine isolate behind an RPC wrapper: polled budget stop, post-call reset above a threshold, reset-retry-reset on throw. Checks no polluted instance at request start, isolate never hits the kill limit, bounded budget overshoot, and grow-or-reset memory steps. |
623f9b12 | 2 | 89 | 2026-07-23 23:04:22 UTC |
| webmtp MTP/PTP-over-USB initiator-responder transaction machine: command/data/response containers on bulk pipes, per-session transaction IDs, session lifecycle with stale-session recovery, and object upload where a file-flavored SendObjectInfo must immediately precede SendObject while a folder-flavored (association) SendObjectInfo is a standalone terminal operation. Checks tid matching, single bounded data phase per direction, session gating, and the file-info pairing rule. |
623f9b12 | 3 | 42 | 2026-07-23 18:08:45 UTC |
| OpdsCredentials OPDS credential lifecycle: a credentials table keyed by user with a UNIQUE password column. Enable/regenerate is an atomic upsert with a bounded retry loop on password collision; revoke deletes the row; concurrent basic-auth reads resolve a password to a user. Checks PasswordsUnique, AtMostOneCredPerUser, and AuthSound (stale passwords never authenticate). |
623f9b12 | 1 | 33271 | 2026-07-22 15:45:50 UTC |
| OpenMonkey An open userscript registry with immutable, monotonically published script versions, author-only publishing, and fork lineage. Install and run happen in third-party userscript managers outside the registry's trust boundary, so security-scan verdicts (per user, per exact version) are advisory community reports. Checks: fork-lineage acyclicity, installed-implies-published, running-implies-installed, and scan verdicts always referencing an exact published version. |
623f9b12 | 1 | 2313 | 2026-07-22 15:30:52 UTC |
| PwaUpdate Service-worker update lifecycle for a web app in autoUpdate mode with a manual force-check: deploys bump a server version; clients install newer versions as a waiting worker and activate them automatically with a page reload, no consent step. Checks that active versions were deployed, waiting is strictly newer and deployed, and (action property) monotone upgrade: active only increases, and only to a previously installed waiting version. |
623f9b12 | 2 | 46 | 2026-07-22 14:31:23 UTC |
| ProcAuth A shared browser-driven auth surface for a family of apps on one registrable domain: the client fetches a challenge bound to a principal and an allowlisted return_to target, a verify step consumes the challenge (single-use, bounded TTL) and creates a session, logout destroys it. Checks sessions are backed by a same-owner consumed challenge, challenges back at most one session, verification happens within TTL, authenticated redirects only go to allowlisted targets, and used challenges are never r |
623f9b12 | 1 | 1412 | 2026-07-22 14:08:00 UTC |
| OpenMonkeyAuth Browser-driven auth ceremony against an external auth service: the client fetches a challenge bound to a principal, a verify step consumes the challenge (single-use, bounded TTL) and creates a session, logout destroys it. Checks that every session is backed by a same-owner consumed challenge, challenges back at most one session, verification happens within TTL, used challenges are never replayed, and challenge bindings are immutable. |
623f9b12 | 1 | 1412 | 2026-07-22 14:06:43 UTC |
| TpxGrant Metered OAuth grant lifecycle with rotating refresh tokens and two racing clients; checks spend never exceeds the granted budget, at most one refresh token generation is live, and revocation is final |
623f9b12 | 1 | 122 | 2026-07-22 04:34:32 UTC |
| Sync State-based LWW client-server sync with per-user sequence log, tombstones, and dirty-skip pull rule. Two clients, one server: Lamport-bumped timestamps with unique write-id tie-breakers, an append-only server log, cursor-based pulls. Checks quiescence convergence, no-resurrection (store is LWW-max of the log), log immutability/density, and cursor monotonicity. |
623f9b12 | 1 | 49713 | 2026-07-22 04:10:10 UTC |
| Gratos_AAuth Agent-authorization consent/mission state machines (AAuth-style person server): durable mission proposals with single-use consent codes, intended-approver binding, narrow-only budget attenuation at approval, token issuance gated on active missions, and one-shot pickup of short-TTL pending consent records. Checks code single-use, approver binding, attenuation-never-widens, no issuance after close, at-most-once delivery, and terminality of closed states. |
623f9b12 | 1 | 13376 | 2026-07-21 00:11:53 UTC |
| tpx_a TPX-A (tokenpony.dev), the AAuth-based agent flow of the open TPX protocol: a Person Server attests a single-use mission budget, the budget binds on the first relayed token, a funder must claim the mission before any spend, and each metered call runs reserve/commit/release against a mission-keyed meter. Checks a hard exposure cap (spent plus reserved never exceeds budget), no spend before funding, budget binds once, and revocation is final with exposure only shrinking. |
623f9b12 | 3 | 9573 | 2026-07-20 22:27:56 UTC |
| tpx TPX v0.2 (tokenpony.dev), an open OAuth 2.1 profile for budget-capped LLM API access: single-use authorization codes (replay revokes the minted grant), rotating refresh tokens (reuse revokes the grant), and a hard per-grant spend budget. Checks that spend never exceeds the budget, each code mints at most one grant, live grants trace to redeemed codes, and revocation is immediate and final. |
623f9b12 | 3 | 7393 | 2026-07-20 22:27:17 UTC |
| Gratos_Sandbox Ephemeral-environment (sandbox) lifecycle: environments are minted anonymous or owned; a background sweep deletes only aged anonymous ones, while owned environments persist until their owner deletes them. Checks that anonymous and owned sets stay disjoint and that no environment ever minted as owned is removed by the sweep. |
623f9b12 | 1 | 125 | 2026-07-20 17:33:47 UTC |
| Gratos_Challenge Challenge-keyed pending-ceremony store for WebAuthn: tenant-namespaced challenges are issued, consumed atomically (get + delete) on verify, or expire by TTL. Checks NoReplay — a consumed (tenant, challenge) pair never becomes live again, so a credential response verifies at most once; cross-tenant isolation is structural via tenant-namespaced keys. |
623f9b12 | 1 | 81 | 2026-07-20 17:33:33 UTC |
| MeteredMission Mission-scoped budget metering for delegated agents on a metered API: single-use budget attestations from the approver's identity server, first-relay budget binding, a funding gate before any spend, and escrow-style reserve/commit/release around each call. Checks a hard exposure cap (spent plus reserved never exceeds budget), no spend before funding, budget binds once, and revocation is final with exposure only shrinking. |
623f9b12 | 1 | 9573 | 2026-07-20 16:46:46 UTC |
| MeteredGrant Budget-scoped grant lifecycle for a metered API, styled as an OAuth 2.1 profile: single-use authorization codes (replay revokes the minted grant), rotating refresh tokens (reuse revokes the grant), and a per-grant spend budget. Checks that spend never exceeds the budget, each code mints at most one grant, live grants trace to redeemed codes, and revocation is immediate and final. |
623f9b12 | 1 | 7393 | 2026-07-20 16:46:31 UTC |
| Gratos_Signup DNS-verified domain-claiming flow: anonymous pending claims bind to an identity, advance by external DNS verification or a provider callback, and finalize into an at-most-one-owner registry; claims may expire and DNS may flap at any time. Checks one owner per domain, one pending claim per domain, no lingering claims after ownership, and that advancement always required a bound identity. |
623f9b12 | 1 | 256 | 2026-07-20 16:40:08 UTC |
| Gratos_Credentials Single-user credential lifecycle with ranked authentication methods (webauthn > devicekey > softkey): sessions carry the rank of the credential that minted them; deletion requires the session to outrank-or-equal the target and never removes the last credential. Checks never-orphaned, no privilege-escalation deletes, and that a phished low-rank key can never evict the strongest credential. |
623f9b12 | 1 | 6717 | 2026-07-20 16:39:22 UTC |
| Gratos_Authz Multi-tenant authorization control plane: ownership tuples written only via a trusted idempotent grant path, open anonymous sandbox tenants that can never gain owners or service tokens, owner-minted per-tenant bearer tokens delegating mutation rights, and tenant cleanup. Checks that all owners came from the trusted path, all mutations were authorized when performed, and token mints trace back to claimed owners. |
623f9b12 | 1 | 1316 | 2026-07-20 16:39:09 UTC |