A second agent wrote Conway's Life cleanly on current main (works first
time, all 200 generations clean, 0 corruption signatures, all contracts
Tier 1).  Their think-aloud transcript surfaced three concrete SKILL.md
gaps:

1. array_length: returns Int per the registration but flows freely
   into Nat positions via the bidirectional Int <: Nat permitted by
   the type checker (verifier-enforced via Z3).  The old comment said
   "returns Int (always >= 0)" -- correct but agents read this and
   reach for int_to_nat unnecessarily before discovering empirically
   that they don't need it.  Updated to "returns Nat (the array
   length, flows to either Nat or Int positions)" matching user-
   visible behaviour.

2. array_fold closure shape: the SKILL pinned the De Bruijn slot
   mapping (@Int.0 = element, @Int.1 = accumulator) but never spelled
   out the resulting signature shape (fn(@acc, @elem -> @acc)).
   Agents have to derive it via the rightmost = .0 rule, and one
   wrote a probe to confirm before using array_fold for population
   counting.  Three-line comment added making the shape explicit.

3. Tuple construction: SKILL mentioned @tuple<Int, String> as a type
   exactly once (line 388) with no construction or destructuring
   example.  An agent considered using array_fold over a tuple table
   of (dr, dc) offset pairs for neighbour counting, hunted for tuple
   literal syntax, didn't find any, and fell back to a verbose
   sequential let chain.  Tuples DO work -- the constructor is just
   the upper-case Tuple name -- but it has to be discovered by guess
   or by reading the spec grammar.  Added a brief subsection in the
   "Composite types" area showing Tuple(...) construction and match
   destructuring.

Plus a side-effect: scripts/check_skill_examples.py allowlist line
numbers re-anchored to match the new SKILL.md line offsets.  Both
the array_fold edit and the Tuple subsection bumped subsequent line
numbers; fix_allowlists.py auto-shifted most entries but missed two
which were patched manually.

Validation:
- All 56 SKILL.md vera blocks parse, 62 allowlisted, 0 failed
- pytest tests/ -q: 3,747 passed, 14 skipped
- check_doc_counts / check_limitations_sync / check_site_assets clean

Co-Authored-By: Claude <noreply@anthropic.invalid>

CI fix:
- Added a [Unreleased] CHANGELOG entry covering the three SKILL fixes
  + the allowlist re-anchoring tooling change.  Previous push failed
  the lint job because the changelog hook was unsatisfied.

CodeRabbit fix (verified against current code):
- The allowlist tuple at line 1905 was suppressing a parseable
  example (CORRECT add-with-effects full function) -- removed.  The
  description "Wrong: bare @int + @int without indices" that lived
  there was actually the correct description for the bare-add code
  at line 1942 (where the entry's previous label "Common mistake
  example, bare if/else" was just wrong -- the block is bare add,
  not if/else).  Net change: drop the misplaced entry, fix the
  description on its rightful neighbour.

Bonus low-hanging fix folded in for #605:
- SKILL.md "decreases (termination)" subsection opening rewritten
  to lead with the pure-vs-effectful rule prominently rather than
  saying "Required on recursive functions" (which was misleading
  for effectful recursion).  Two recent agents writing Conway's
  Life had to triangulate this rule between FizzBuzz and the State
  example; the explicit one-liner lets future agents answer it on
  first read.  #605 stays open for the broader doc-prominence work
  (this is the ~5-line subset that was cheap to fold in).

Validation:
- 56 SKILL.md vera blocks parse, 62 allowlisted, 0 failed
- pytest tests/ -q: green
- check_doc_counts / check_limitations_sync / check_site_assets clean

Co-Authored-By: Claude <noreply@anthropic.invalid>

…terp)

Two concrete fix proposals from the second Conway's Life agent's
design memo, closing the timing and rendering halves of the terminal-
vs-browser IO seam without language changes.  Updated the #608 row to
point at both sub-issues so anyone reading KNOWN_ISSUES sees the full
fix path rather than just the framing.

Co-Authored-By: Claude <noreply@anthropic.invalid>

Two Conway's Life agent experiments on --target browser surfaced
five concrete blockers (issues #602/#603/#604/#609/#610) and an
explicit design memo (#608) mapping each obstacle to a concrete
runtime-only fix.  The current stabilisation framing covers
codegen reliability and walker completeness but treats browser-
target reliability as a separate concern.  The agent's diagnosis
makes that split harder to defend: "write once, run anywhere"
is currently true for pure computation and approximate-to-false
for anything with timing or screen output.  Two of the fixes
(#609 JSPI-driven IO.sleep, #610 ANSI subset interpreter) close
the timing and rendering halves of the seam without language
changes -- adding them to the stabilisation tier commits to
"browser-target Vera is something you'd actually use" before
the agent-integration push.

Changes:
- Expanded the campaign-pattern list from two patterns to three;
  third pattern documents the browser-target seam with links to
  the umbrella issue (#608) and the five concrete blockers.
- Added #609 (JSPI-driven IO.sleep) as item 3 in the stabilisation
  tier, with rationale + the WebAssembly JSPI / Asyncify mechanism.
- Added #610 (ANSI subset interpreter) as item 4 in the same tier,
  paired with #609 -- together they close the seam and let life.vera
  (terminal version) run unchanged on --target browser.
- Renumbered #595 from item 3 to item 5 (now last in stabilisation,
  since it's contingent on an upstream wasmtime-py release).
- Renumbered the agent-integration tier items 4/5/6 -> 6/7/8 to
  match.
- Updated the "What moves when" gate from "#4 starts when #1-#3
  are closed" to "#6 starts when #1-#5 are closed".

Co-Authored-By: Claude <noreply@anthropic.invalid>

Audit pass requested before merging #601: walk every limitation list
across SKILL.md, vera/README.md, spec/, and KNOWN_ISSUES.md to (a)
remove anything we've closed off and (b) add anything we've newly
flagged.

Result of audit:
- No closed issues found stale-listed in any open-limitation table.
  All references to closed issues (#588, #593, #520, #589) are
  referential prose ('X turned out to be...', 'see #520's pattern')
  rather than open-issue listings.  Nothing to remove.
- Five limitation entries were missing across three docs:
  * SKILL.md Known Limitations: browser-target IO seam (#608).
  * SKILL.md Known Bugs and Workarounds: #602 (string interp invalid
    WASM with workaround) and #604 (prelude combinators skipped on
    browser target).
  * vera/README.md Current Limitations: browser-target IO seam.
  * spec/12-runtime.md "## 12.8 Limitations" replaced 'No open
    limitations.' with the two browser-runtime gaps (#609 JSPI sleep,
    #610 ANSI subset interpreter).
- spec/11-compilation.md left as 'No open limitations' deliberately;
  #602 and #604 are bugs that belong in KNOWN_ISSUES, not enduring
  compilation-model limitations of the spec.

Validation: SKILL examples parse (56 OK / 62 allowlisted / 0 failed),
doc counts consistent, limitations sync clean (36 in KNOWN_ISSUES,
18 in vera/README, 4 across spec chapters).

Co-Authored-By: Claude <noreply@anthropic.invalid>