marcelofarias · marcelofarias · May 22, 2026 · May 22, 2026 · May 22, 2026 · May 22, 2026
diff --git a/AGENTS.md b/AGENTS.md
@@ -194,8 +194,18 @@ parse the resulting `{ ok: false, diagnostics: [...] }` envelope.
 | RES001 | (0.3+) `Result.try` / `Result.tryAsync` with no body. | `Result.try { <body that may throw> }`. |
 | INT001 | (0.7+) A fn declares `intent: "pure"` but also has `uses { … }`. (0.8+) Also fires when `intent: "pure"` is combined with `reads { … }` or `writes { … }`. Pure functions may not declare capabilities or resource dependencies. | Either drop the conflicting header clause(s) or change the intent to reflect the actual behaviour. |
 | SYN001 | Duplicate fn header clause (e.g. two `reads { }` on the same fn, or two `intent:`), or a label inside `reads {}` / `writes {}` that is not a plain identifier. `parseFn` is version-agnostic, so SYN001 fires whenever a duplicate clause is written regardless of the `?bs` pin. | Declare each header clause once; merge label lists rather than repeating the clause; use bare identifiers (not quoted strings) as labels. |
-| THR001 | (0.9+) A fn (or a same-file callee, transitively) throws an exception type not declared in the fn's `throws {}`. If `loadUser` calls `fetchRow throws { NetworkError }`, `loadUser` must also declare `throws { NetworkError }`. | Add the missing type(s) to `throws {}` at each level of the call chain. |
+| INT002 | (0.7+) A fn declares `intent: "pure"` but its body directly references a stdlib capability (e.g. `http.get`, `fs.read`). Pure intent is enforced at the body level as well as the header. | Remove the stdlib call from the body, or change the intent. |
+| CAP003 | (0.9+, warning) A fn is declared `unsafe "reason" fn name(…)` and also has a `uses { … }` clause. The compiler cannot prove the capability is actually reached — the assertion is programmer-owned. Non-blocking; the fn compiles. | Remove the `uses {}` clause if it is not needed, or document why the assertion is trusted. |
+| EFF002 | (0.7+) A callback parameter declares `uses { … }` capabilities beyond what the outer fn declares. A fn that claims `uses { net }` cannot safely accept a callback that also writes to `fs` — the outer declaration would be a lie. | Extend the outer fn's `uses {}` to cover the callback's full capability set, or narrow the callback's annotation. |
+| EFF003 | (0.9+) A callback parameter declares `reads { … }` labels not covered by the outer fn's `reads {}`. Same structural rule as EFF002 applied to resource read dependencies. | Add the missing label(s) to the outer fn's `reads {}`, or narrow the callback annotation. |
+| EFF004 | (0.9+) A callback parameter declares `writes { … }` labels not covered by the outer fn's `writes {}`. | Add the missing label(s) to the outer fn's `writes {}`, or narrow the callback annotation. |
+| DEP001 | (0.9+) A fn's body (or a callee in the same file) reads a resource label not declared in the fn's own `reads {}`. Transitivity is enforced: if `loadUser` calls `fetchRow` which reads `userDb`, `loadUser` must also declare `reads { userDb }`. | Add the missing label(s) to `reads {}`, or remove the undeclared read. |
+| DEP002 | (0.9+) Same as DEP001 but for `writes {}` labels. A fn whose callee writes a resource must declare that write in its own header. | Add the missing label(s) to `writes {}`, or remove the undeclared write. |
+| THR001 | (0.9+) A fn's body (or a same-file callee) throws an exception type not declared in the fn's `throws {}`. Transitivity is enforced: if `loadUser` calls `fetchRow throws { NetworkError }`, `loadUser` must also declare `throws { NetworkError }`. | Add the missing type(s) to `throws {}`, or add a `match` / `unsafe` to suppress the propagation. |
 | THR002 | (0.9+) A fn body directly constructs `err(TypeName(...))`, `err(new TypeName(...))`, or `err(TypeName)` where `TypeName` (CapCase) is not declared in the fn's own `throws {}` clause. Producer-side complement to THR001. | Add `TypeName` to the fn's `throws {}`, or change the error construction to use a declared type. |
+| THR003 | (0.9+) A callback parameter declares `throws { … }` types not covered by the outer fn's `throws {}`. Same structural rule as THR001 applied to callback parameters. | Add the missing type(s) to the outer fn's `throws {}`, or narrow the callback annotation. |
+| VER001 | (warning, < 0.9) A non-empty `reads {}` or `writes {}` clause is declared on a fn in a file pinned below `?bs 0.9`. DEP001/DEP002 enforcement is not active; the annotation is documentation only. Non-blocking. | Upgrade the pin to `?bs 0.9` to activate enforcement, or leave it knowing it is unenforced. |
+| VER002 | (warning, < 0.9) A non-empty `throws {}` clause is declared on a fn in a file pinned below `?bs 0.9`. THR001 enforcement is not active; the annotation is documentation only. Non-blocking. | Upgrade the pin to `?bs 0.9` to activate enforcement, or leave it knowing it is unenforced. |
 
 When you add a new compiler error, allocate the next free code in the same
 range (`BSnnn` for general parse errors, `CAPnnn` for capability checks,

diff --git a/README.md b/README.md
@@ -178,7 +178,7 @@ claude mcp add botscript -- npx -y @mbfarias/botscript-mcp
 | ----------- | -------------------------------------- | --------------------------------------------------------------------------------------------------- |
 | `primer`    | (no args)                              | The canonical language primer (same text the `?primer` directive emits).                            |
 | `transform` | `{ source: string, filename?: string }` | `{ ok: true, code, forms, version }` on success, or `{ ok: false, diagnostics: [...] }` on failure. |
-| `explain`   | `{ code: string }`                     | Long-form explanation for any stable diagnostic code (`BS001`, `BS002`, `CAP001`–`CAP003`, `DEP001`, `DEP002`, `EFF002`–`EFF004`, `FMT001`, `INT001`, `INT002`, `RES001`, `SYN001`, `THR001`–`THR003`, `UNS001`–`UNS004`) plus a fails/passes example pair. |
+| `explain`   | `{ code: string }`                     | Long-form explanation for any stable diagnostic code (`BS001`, `BS002`, `CAP001`–`CAP003`, `DEP001`, `DEP002`, `EFF002`–`EFF004`, `FMT001`, `INT001`, `INT002`, `RES001`, `SYN001`, `THR001`–`THR003`, `UNS001`–`UNS004`, `VER001`–`VER002`) plus a fails/passes example pair. |
 
 A bot's loop becomes deterministic: `transform` → if `ok=false`, read
 `diagnostics[0].code` → `explain(code)` → apply `rewrite` → `transform` again.

diff --git a/packages/compiler/src/error-codes.ts b/packages/compiler/src/error-codes.ts
@@ -412,6 +412,44 @@ const E: Record<string, ErrorCodeEntry> = {
       "  else ok(s)\n" +
       "}",
   },
+  VER001: {
+    code: "VER001",
+    title: "reads {} / writes {} declared below the ?bs 0.9 enforcement floor — annotation is unenforced",
+    rule:
+      "DEP001/DEP002 (reads/writes transitivity) are enforced from `?bs 0.9`; a non-empty `reads {}` or " +
+      "`writes {}` clause on a file pinned below 0.9 is accepted but not verified — it is documentation only",
+    idiom:
+      "annotate now if you intend to enforce later, but know that reviewers reading the header " +
+      "cannot assume the compiler has checked it; upgrade the pin to `?bs 0.9` to activate enforcement",
+    rewrite:
+      "upgrade pin to `?bs 0.9` to activate DEP001/DEP002 enforcement",
+    example:
+      "// before — reads {} at ?bs 0.8 is documentation only (VER001 warning)\n" +
+      "?bs 0.8\n" +
+      "fn loadUser(id: string) reads { userDb } -> string = id\n\n" +
+      "// after — enforcement active\n" +
+      "?bs 0.9\n" +
+      "fn loadUser(id: string) reads { userDb } -> string = id",
+  },
+  VER002: {
+    code: "VER002",
+    title: "throws {} declared below the ?bs 0.9 enforcement floor — annotation is unenforced",
+    rule:
+      "THR001 (throws transitivity) is enforced from `?bs 0.9`; a non-empty " +
+      "`throws {}` clause on a file pinned below 0.9 is accepted but not verified — it is documentation only",
+    idiom:
+      "annotate now if you intend to enforce later, but know that reviewers reading the header " +
+      "cannot assume the compiler has checked it; upgrade the pin to `?bs 0.9` to activate enforcement",
+    rewrite:
+      "upgrade pin to `?bs 0.9` to activate THR001 enforcement",
+    example:
+      "// before — throws {} at ?bs 0.8 is documentation only (VER002 warning)\n" +
+      "?bs 0.8\n" +
+      "fn loadUser(id: string) throws { NetworkError } -> string = id\n\n" +
+      "// after — enforcement active\n" +
+      "?bs 0.9\n" +
+      "fn loadUser(id: string) throws { NetworkError } -> string = id",
+  },
 };
 
 export function getErrorCode(code: string): ErrorCodeEntry | undefined {

diff --git a/packages/compiler/src/passes/ver-check.ts b/packages/compiler/src/passes/ver-check.ts
@@ -0,0 +1,108 @@
+/**
+ * Version-floor warning for unenforced effect declarations (?bs < 0.9).
+ *
+ * Effect annotations are parsed and accepted at any version, but enforcement
+ * only kicks in from `?bs 0.9`:
+ *
+ *   - `reads {}` / `writes {}` + DEP001/DEP002: enforced from `?bs 0.9`
+ *   - `throws {}` + THR001: enforced from `?bs 0.9`
+ *
+ * When a non-empty clause is present on a file pinned below its enforcement
+ * floor, the compiler accepts it silently — the annotation is documentation,
+ * not a verified claim. A reviewer reading the header would reasonably assume
+ * the compiler has verified the transitivity claim; it has not.
+ *
+ *   VER001  A non-empty `reads {}` or `writes {}` clause is declared on a fn
+ *           whose file is pinned below `?bs 0.9`. DEP001/DEP002 are not
+ *           enforced; the annotation is documentation only.
+ *
+ *   VER002  A non-empty `throws {}` clause is declared on a fn whose file is
+ *           pinned below `?bs 0.9`. THR001 is not enforced; the annotation
+ *           is documentation only.
+ *
+ * Both VER001 and VER002 are warnings (non-blocking) — the intended pattern
+ * of "annotate first, then upgrade the pin" is valid. The warning makes the
+ * lack of enforcement visible so reviewers are not given false assurance.
+ *
+ * Only non-empty clauses are flagged. An empty `reads {}` / `throws {}` on
+ * an old-pin file is likely an intentional forward-declaration placeholder
+ * and does not create false assurance.
+ *
+ *   ?bs 0.9+  This pass is a no-op (enforcement is active, no warning needed).
+ */
+
+import type { Diagnostic } from "../diagnostics.js";
+import { getErrorCode } from "../error-codes.js";
+import { parseProgram } from "../parser/parse.js";
+import { locationOf } from "./_location.js";
+import { atLeast, type VersionInfo } from "./version.js";
+
+export interface VerCheckResult {
+  code: string;
+  warnings: ReadonlyArray<Diagnostic>;
+}
+
+export function passVerCheck(src: string, version: VersionInfo): VerCheckResult {
+  // Enforcement is active at 0.9 — no warning needed.
+  if (atLeast(version.resolved, "0.9")) return { code: src, warnings: [] };
+
+  const allowGenerics = atLeast(version.resolved, "0.4");
+  const program = parseProgram(src, { allowGenerics, includeNestedFns: true });
+  const warnings: Diagnostic[] = [];
+
+  const ver001 = getErrorCode("VER001")!;
+  const ver002 = getErrorCode("VER002")!;
+
+  for (const { decl } of program.fns) {
+    const hasUnenforcedReads = (decl.reads?.length ?? 0) > 0;
+    const hasUnenforcedWrites = (decl.writes?.length ?? 0) > 0;
+    const hasUnenforcedThrows = (decl.throws?.length ?? 0) > 0;
+
+    if (hasUnenforcedReads || hasUnenforcedWrites) {
+      const { line, column } = locationOf(src, decl.fnKeywordStart);
+      const clauses: string[] = [];
+      if (hasUnenforcedReads) clauses.push(`reads { ${decl.reads!.join(", ")} }`);
+      if (hasUnenforcedWrites) clauses.push(`writes { ${decl.writes!.join(", ")} }`);
+      const clauseStr = clauses.join(" / ");
+
+      warnings.push({
+        code: "VER001",
+        severity: "warning",
+        file: null,
+        line,
+        column,
+        start: decl.fnKeywordStart,
+        end: decl.nameStart + decl.name.length,
+        message:
+          `fn '${decl.name}' declares ${clauseStr} at ?bs ${version.resolved} — ` +
+          `DEP001/DEP002 enforcement requires ?bs 0.9; this annotation is unenforced`,
+        rule: ver001.rule,
+        idiom: ver001.idiom,
+        rewrite: ver001.rewrite,
+      });
+    }
+
+    if (hasUnenforcedThrows) {
+      const { line, column } = locationOf(src, decl.fnKeywordStart);
+      const throwsStr = `throws { ${decl.throws!.join(", ")} }`;
+
+      warnings.push({
+        code: "VER002",
+        severity: "warning",
+        file: null,
+        line,
+        column,
+        start: decl.fnKeywordStart,
+        end: decl.nameStart + decl.name.length,
+        message:
+          `fn '${decl.name}' declares ${throwsStr} at ?bs ${version.resolved} — ` +
+          `THR001 enforcement requires ?bs 0.9; this annotation is unenforced`,
+        rule: ver002.rule,
+        idiom: ver002.idiom,
+        rewrite: ver002.rewrite,
+      });
+    }
+  }
+
+  return { code: src, warnings };
+}
diff --git a/packages/compiler/src/transform.ts b/packages/compiler/src/transform.ts
@@ -7,6 +7,7 @@ import { passCapCheck } from "./passes/cap-check.js";
 import { passFn } from "./passes/fn.js";
 import { passImports } from "./passes/imports.js";
 import { passCapAssert } from "./passes/cap-assert.js";
+import { passVerCheck } from "./passes/ver-check.js";
 import { passDepCheck } from "./passes/dep-check.js";
 import { passThrCheck } from "./passes/thr-check.js";
 import { passEffCheck } from "./passes/eff-check.js";
@@ -62,6 +63,11 @@ const PASS_PIPELINE: ReadonlyArray<PipelineEntry> = [
   // message "intent says pure but has uses { net }" is seen before the
   // transitive capability walk, which produces noisier output.
   { name: "intentCheck", fn: passIntentCheck, minVersion: "0.7" },
+  // verCheck: non-blocking warning (VER001/VER002) when reads/writes/throws
+  // annotations are declared below their enforcement floor (?bs 0.9). Runs
+  // early so it can see the full, unmodified header. No-op at 0.9+ because
+  // the enforcement passes (depCheck, thrCheck) already validate the claims.
+  { name: "verCheck", fn: passVerCheck },
   // effCheck: header-level check that the outer fn's capabilities cover the
   // effect annotations on its callback parameters (EFF002). Runs alongside
   // intentCheck — both are header consistency checks before the body walk.