diff --git a/jcp/SPEC.md b/jcp/SPEC.md
index b20e80943..883866a4d 100644
--- a/jcp/SPEC.md
+++ b/jcp/SPEC.md
@@ -172,6 +172,27 @@ decision against the revoked grant **or any chain containing it**: a delegation
 subtree dies with any of its ancestors. Both the direct and the chained decision
 path MUST enforce this.
 
+**Propagation.** The rule above binds an enforcement point *once it holds the
+revocation*, and says nothing about how it comes to hold one. §4.3 requires an enforcement point to deny a revoked grant **once it holds the
+revocation**, and says nothing about how it comes to hold one. With a budget
+sharded across N enforcement points (§4.5), a revocation that has reached three
+of five leaves the grant live at two, and — the part that matters for an audit —
+an allow issued by a point that *had not yet heard* is indistinguishable, after
+the fact, from an allow by a point that heard and ignored it. The first is a
+propagation delay. The second is a violation of this specification.
+
+An implementation that supports revocation **MUST** define how revocations reach
+its enforcement points, and **SHOULD** let each point state how current its
+revocation knowledge is, as a marker monotonic in whatever its revocation feed
+counts — a sequence number, a log index, a timestamp. JCP neither defines nor
+interprets the marker; it requires only that a larger value mean "has seen at
+least as much".
+
+Given a revocation issued at marker `M`, an allow from a point at
+`known_through < M` is explicable and one at `known_through >= M` is not. Where a
+point states no marker, an auditor **MUST** treat its allows as *unverifiable*
+for revocation rather than as compliant — "did not say" is not "was current".
+
 ### 4.4 Delegation control (REQUIRED)
 
 A grant MAY carry `delegate_depth`: how many further attenuation hops it
@@ -374,6 +395,71 @@ An empty caveat set is omitted from the canonical encoding, so a grant without
 caveats is byte-identical to one minted before they existed — its content id and
 signature are unchanged. Conformance class **C24**.
 
+### 4.10 Flow: what a value's provenance may exercise (OPTIONAL)
+
+A grant answers *who* may do *what*, for *how many joules*. It does not answer
+where the **argument** came from. An agent holding a legitimate grant, handed a
+value that originated in an untrusted channel, exercises real authority on
+attacker-chosen input — and every check above passes, because the grant is valid
+and the action is granted.
+
+A value therefore carries a **label**, and a grant MAY carry a ceiling the label
+must sit below.
+
+```
+Label { integrity: Integrity, origins: Origins, readers: Readers }
+```
+
+The three components order independently and the label order is their product.
+`⊥` is a principal-authored value from no channel, readable by all — the label of
+anything in a run that has touched no untrusted source. `⊤` is untrusted, from
+anywhere, readable by nobody.
+
+**JCP consumes a label; it does not compute one.** Propagation — the label of a
+result being at least the join of the labels of everything that went into it — is
+the host's job, because only the host sees the data move. JCP's contribution is
+the gate and, below, the rule that an *uncomputed* label is not a clean one. A
+host that propagates badly will present a label JCP cannot audit; what JCP
+guarantees is that a host which propagates at all gets a decision bound to what
+it reported, and that one which does not gets a refusal rather than a pass.
+
+A grant expresses its ceiling as a `FlowBelow` caveat (§4.9) carrying a
+`FlowCeiling`: the ceiling label, and optionally a `tainted_budget_uj` — a
+separate, smaller joule allowance for calls whose argument is not `⊥`. Where a
+chain carries several, they compose to the **strictest**; attenuation never
+widens one.
+
+An enforcement point MAY also configure a **taint floor** per resource — the flow
+analogue of a trust root (§7). The ceiling is what the *issuer* will permit; the
+floor is what the *enforcement point* will accept regardless of who granted what.
+Default-open, so an unconfigured point behaves exactly as before.
+
+**The gate.** A decision is denied unless the argument's label sits at or below
+the grant's ceiling **and** the resource's taint floor does not refuse its
+origins. Three cases are distinguished, and the distinction is the point:
+
+| facts | meaning | result |
+|---|---|---|
+| absent | provenance was **not computed** | **fails closed** where a ceiling is present; a ceiling-free grant is unaffected |
+| `⊥` | computed, and clean | passes any ceiling |
+| labelled | computed, and tainted | tested against the ceiling and the floor |
+
+"Not computed" **MUST NOT** be read as "clean". An un-migrated caller that cannot
+say where its argument came from has not established that the argument is safe,
+and a grant whose issuer took the trouble to set a ceiling MUST NOT be exercised
+on an unlabelled value.
+
+**Where the check sits is normative.** It MUST run *after* capability and
+signature verification — the ceiling lives inside an authenticated grant, so
+judging flow before the signature would seal a verdict over attacker-chosen
+policy — and *before* caveats and the budget test, so that **a tainted call costs
+zero joules**. A denial on flow is the same invariant as a denial on capability:
+nothing is debited and nothing runs.
+
+A grant carrying no `FlowBelow` caveat is byte-identical to one minted before
+flow existed, and an enforcement point with no taint floor configured decides
+exactly as it did before. Conformance class **C25**.
+
 ## 5. Energy (REQUIRED)
 
 Every metered cost is integer microjoules with a provenance tag: `HwShunt`
@@ -743,4 +829,5 @@ gate.
 - **C21 — checkpoints + amendments:** an agent checkpoints its own state; only the grant's issuer — a principal distinct from the agent — may amend, only to tighten; an agent steering itself, a non-issuer amending, a widening amendment, and an amendment bound to a different checkpoint are each refused.
 - **C23 — receipt binds its payload + profile migration:** a `jcp/2` receipt commits the `payload_hash` it decided over; substituting only the payload (same grant, action, and cost) fails verification — the forgery a payload-blind receipt could not detect; and receipts published under `jcp/1` still verify, because the verifier recomputes the preimage under the profile the receipt names rather than assuming one.
 - **C24 — caveats:** a caveat embedded in the grant is enforced offline by the decision point; `PayloadIs` makes a grant one-shot (a replay with different arguments is denied `caveat-unsatisfied`); `MaxCostUj` bounds a single invocation independently of the cumulative budget; a caveat may narrow below the capability; attenuation inherits every parent caveat and refuses to drop one; and a grant with no caveats encodes byte-identically to one minted before they existed.
+- **C25 — flow:** a value's propagated label must sit at or below the grant's ceiling and clear the resource's taint floor; an argument whose provenance was **not computed** fails closed against a ceilinged grant rather than passing as clean; several ceilings in a chain compose to the strictest and attenuation never widens one; a flow denial debits nothing, so a tainted call costs zero joules; and a grant with no flow caveat encodes byte-identically to one minted before flow existed.
 - **C22 — dual ceilings:** a money ceiling beside the joule ceiling is enforced independently — the first to bind denies (`funds-exceeded` / `budget-exceeded`), a foreign-currency cost is refused `currency-mismatch` rather than converted, an allow debits both dimensions and a deny debits neither, and an absent money ceiling encodes byte-identically to a joules-only grant (so its content id and signature are unchanged). Attenuation narrows money independently: dropping, raising, or re-denominating a bounded parent's ceiling is refused; a plain attenuation inherits it.
diff --git a/jcp/jcp-rs/crates/jcp-runtime/src/lib.rs b/jcp/jcp-rs/crates/jcp-runtime/src/lib.rs
index 2dbf08560..924f9a54b 100644
--- a/jcp/jcp-rs/crates/jcp-runtime/src/lib.rs
+++ b/jcp/jcp-rs/crates/jcp-runtime/src/lib.rs
@@ -61,6 +61,11 @@ pub struct Runtime {
     /// another.
     spent_minor: HashMap<ContentId, u64>,
     revocations: RevocationSet,
+    /// How current this point's revocation knowledge is (SPEC §4.3,
+    /// Propagation). `None` — the default — means it has not said, which an
+    /// auditor must read as *unverifiable*, not as current. Opaque and
+    /// monotonic in whatever the deployment's revocation feed counts.
+    revocation_marker: Option<u64>,
     /// Configured trust roots (SPEC §7): resource → the root-issuer keys this
     /// enforcement point honors for it. Empty for a resource = not configured
     /// (open); once any root is configured for a resource, a chain whose root
@@ -302,6 +307,45 @@ impl Runtime {
         self.revocations.contains(grant_id)
     }
 
+    /// Declare how current this enforcement point's revocation knowledge is
+    /// (SPEC §4.3).
+    ///
+    /// The marker is opaque to JCP and monotonic in whatever the deployment's
+    /// revocation feed counts — a sequence number, a log index, a timestamp.
+    /// JCP neither defines nor interprets it; it only requires that a larger
+    /// value mean "has seen at least as much".
+    ///
+    /// Why it exists. §4.3 requires an enforcement point to deny a revoked
+    /// grant *once it has the revocation*, and says nothing about how it gets
+    /// one. With budgets sharded across N points (§4.5), a revocation that has
+    /// reached three of five leaves the grant live at two — and an allow from
+    /// a point that had not yet heard is indistinguishable, after the fact,
+    /// from an allow by a point that had heard and ignored it. The first is a
+    /// propagation delay; the second is a violation of this spec. Recording
+    /// the marker is what separates them: given a revocation issued at marker
+    /// M, an allow from a point at `known_through < M` is explicable, and one
+    /// at `>= M` is not.
+    ///
+    /// **Honest limit:** this is state on the enforcement point, and the
+    /// `jcp/2` receipt does not carry it. An auditor reconciling receipts
+    /// against a revocation feed therefore needs the point to report its marker
+    /// out of band. Putting it in the signed core would be the stronger
+    /// binding and is a wire change reaching every `Decision` construction site
+    /// across six standards' reference implementations, which do not build
+    /// together.
+    pub fn revocation_known_through(&mut self, marker: u64) {
+        self.revocation_marker = Some(marker);
+    }
+
+    /// The marker last declared by [`Runtime::revocation_known_through`].
+    ///
+    /// `None` means this point has not said how current its knowledge is. That
+    /// is not "fully current": an auditor MUST treat its allows as
+    /// unverifiable for revocation rather than as compliant (SPEC §4.3).
+    pub fn revocation_marker(&self) -> Option<u64> {
+        self.revocation_marker
+    }
+
     /// Configure a trust root (SPEC §7): honor `issuer` as a root for
     /// `resource`. The same local, pairwise trust shape as `authorized_keys` —
     /// no certificate authority, no hierarchy. Once any root is configured for
@@ -1114,6 +1158,45 @@ mod tests {
         assert_eq!(d.verdict, Verdict::Deny(DenyReason::BadSignature));
     }
 
+    #[test]
+    fn an_unstated_revocation_marker_is_not_a_current_one() {
+        // SPEC §4.3, Propagation. The marker exists so an allow can be told
+        // apart from an allow by a point that had not yet heard. The default
+        // must therefore be "has not said" and not a number an auditor could
+        // read as current — `None`, never `Some(0)`, which would claim the
+        // point had seen the start of the feed.
+        let mut rt = Runtime::new();
+        assert_eq!(rt.revocation_marker(), None, "a fresh point must not claim currency");
+        rt.revocation_known_through(42);
+        assert_eq!(rt.revocation_marker(), Some(42));
+        // Monotonic is the deployment's contract, not this crate's: JCP does
+        // not interpret the marker, so it does not police its direction either.
+        // Stated plainly because a reader could expect a clamp here.
+        rt.revocation_known_through(7);
+        assert_eq!(rt.revocation_marker(), Some(7), "JCP neither defines nor polices the feed's order");
+        // And declaring one changes no decision: it is a statement about the
+        // point's knowledge, not an input to the gate. Checked against a
+        // runtime that actually holds a revocation — comparing two runtimes
+        // with empty revocation sets would pass however the marker behaved.
+        let (sg, holder, r) = setup();
+        let f = frame(&sg, r, "read", Trust::Control);
+        let mut rt = Runtime::new();
+        let sr = jcp_grant::revoke(&sk(1), &sg.grant, [7; 16]).unwrap();
+        rt.apply_revocation(&sr, &sg.grant).unwrap();
+        assert_eq!(
+            rt.decide(&f, &sg, holder, Energy::measured(1), 10).verdict,
+            Verdict::Deny(DenyReason::Revoked),
+            "premise: the grant is revoked at this point"
+        );
+        rt.revocation_known_through(99);
+        assert_eq!(
+            rt.decide(&f, &sg, holder, Energy::measured(1), 10).verdict,
+            Verdict::Deny(DenyReason::Revoked),
+            "declaring a marker un-revoked a grant: the marker is not an input to the gate"
+        );
+        assert!(rt.is_revoked(&sg.grant.id()));
+    }
+
     #[test]
     fn revoked_grant_denied() {
         let (sg, holder, r) = setup();