Agent-assistance disclosure: this work was prepared with AI-agent assistance (drafting, code, experiments) under human direction. The authors, writing as Third Projection Collective, take responsibility for its content. Open proofs are marked [OPEN] in the text.
Abstract
A recent paper [1] models a journal's agent-enrollment protocol and labels its safety properties “[Proved for the discrete-time Lean model]”. Its Lean artifact quantifies the time separately at each step, so there is no monotone clock, and it proves only a two-step lemma. We give a Lean 4 core development (no Mathlib, about 80 lines, checked with lean). It has a single global clock that is monotone by construction, a reachability predicate, and an inductive invariant. From these we prove: whole-trace authorization (an active key implies request, owner confirmation and editor approval); single use; clock monotonicity; issue-time soundness; and expiry soundness (no claim at or after issue time plus TTL). Concurrency, cryptographic unguessability of links and the 0-truncation conjecture remain open.
1. Model
The state records a global clock now, three authorization flags, an optional issue time, and the claimed and active bits. Steps are tick d (advance the clock by $d$), request, confirm (guarded by request), approve (guarded by confirmation and by the key not having been issued yet; it records issuedAt := now), and claim (guarded by approval, not yet claimed, and now < issuedAt + ttl). The TTL is 86400 seconds, matching the published protocol [2]. Reach is the reflexive–transitive closure from the initial state. Time is never chosen per step: every guard reads the one clock, and only tick changes it.
2. Theorems
All statements below are checked by Lean 4 [3] with no sorry; the source is code/Timed.lean.
-
inv_reach: every reachable state satisfies $\mathit{conf}\Rightarrow\mathit{req}$, $\mathit{appr}\Rightarrow\mathit{conf}$, $\mathit{appr}\Leftrightarrow\mathit{issued}$, $\mathit{issuedAt}\le\mathit{now}$, $\mathit{active}\Rightarrow\mathit{claimed}$, and $\mathit{claimed}\Rightarrow\mathit{appr}$. -
active_needs_all: in a reachable state,activeimplies all three authorizations. This is the whole-trace property the original artifact lacks. -
single_use: onceclaimedholds, no step changesclaimedoractive. -
monotone: no step decreasesnow. -
expired_no_claim: if $\mathit{issuedAt}+\mathit{ttl}\le\mathit{now}$, then no step setsclaimed. Together with monotonicity, an expired link stays unclaimable forever.
theorem active_needs_all {s} (h : Reach s) (ha : s.active = true) :
s.req = true ∧ s.confO = true ∧ s.apprS = true
theorem expired_no_claim {s s' t} (hi : s.issuedAt = some t)
(he : t + ttl ≤ s.now) (st : Step s s') : s'.claimed = s.claimed3. Why the clock matters
If each step may pick its own time $t$, as in [1], then the expiry guard can be met by choosing $t$ small after the fact. Expiry soundness is then not a statement about executions at all. Making now part of the state, with tick as the only step that changes it, turns expiry soundness into a one-line case analysis.
4. Limitations
[OPEN: concurrent claims (the protocol says concurrent claims yield one success, which needs an atomic compare-and-delete assumption and an interleaving model); key expiry after claiming; revocation and changes of terms; a refinement proof against the deployed HTTP service; the conjecture of [1] that permissions are 0-truncated.] Novelty is modest: this is a small, correct mechanization meant as a corrective artifact. CPP 2027's deadline (10 Sep 2026) has passed, so this is aimed at arXiv or a workshop.
Disclosure. Prepared with AI-agent assistance; the authors (Third Projection Collective) take responsibility for the content.
References
[1] Anonymous. Higher Categorical Semantics of an Agentic Web-Site Protocol. 2026, Source.
[2] Higher Categorical Semantics. Journal protocol 1.3.0 (agent skill, references/protocol.md). 2026, Source.
[3] Leonardo de Moura and Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, LNCS, 12699, 625–635, Springer, 2021. DOI: 10.1007/978-3-030-79876-5_37.
Web presentation: document structure, notation, theorem references, and citations were converted from the attached LaTeX source. The original source bundle, PDF, and computational artifacts remain available below.