aallan · aallan · Sep 7, 2026 · Sep 6, 2026 · Sep 6, 2026 · Sep 7, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
diff --git a/FAQ.md b/FAQ.md
@@ -279,7 +279,7 @@ The reference compiler is under active development. The current release includes
 
 - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
 - A 14-chapter formal specification
-- 13,575 tests, including a 253-program conformance suite
+- 13,686 tests, including a 253-program conformance suite
 - 43 working example programs
 - 164 built-in functions covering strings, arrays, math, parsing, and data types
 - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation

diff --git a/README.md b/README.md
@@ -261,7 +261,7 @@ cp /path/to/vera/SKILL.md ~/.claude/skills/vera-language/SKILL.md
 
 ## Project status
 
-Vera is in **active development** at v0.1.13: 2,000+ commits, 211 releases, 13,575 tests, 95% Python code coverage, 253 conformance programs, 43 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
+Vera is in **active development** at v0.1.13: 2,000+ commits, 211 releases, 13,686 tests, 95% Python code coverage, 253 conformance programs, 43 examples, and a 14-chapter specification. Known bugs and limitations are tracked in **[KNOWN_ISSUES.md](KNOWN_ISSUES.md)**. See **[HISTORY.md](HISTORY.md)** for how the compiler was built.
 
 The reference compiler — parser, AST, type checker, contract verifier (Z3), WASM code generator, module system, browser runtime, and runtime contract insertion — is working. The language specification is in draft across [14 chapters](spec/).
 

diff --git a/ROADMAP.md b/ROADMAP.md
@@ -12,7 +12,7 @@ Ordering derives from the design principles ([DESIGN.md](DESIGN.md)): verificati
 
 ## Where we are
 
-13,575 tests, 253 conformance programs, 43 examples, 14 spec chapters.  [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs (burndown material rather than stage work), plus the *limitations* the stages below retire.
+13,686 tests, 253 conformance programs, 43 examples, 14 spec chapters.  [KNOWN_ISSUES.md](KNOWN_ISSUES.md) tracks the open bugs (burndown material rather than stage work), plus the *limitations* the stages below retire.
 
 ## The v0.2.0 burndown
 

diff --git a/TESTING.md b/TESTING.md
diff --git a/docs/llms-full.txt b/docs/llms-full.txt
@@ -3280,7 +3280,7 @@ The reference compiler is under active development. The current release includes
 
 - A seven-stage pipeline: parse, transform, resolve, typecheck, verify, compile, execute
 - A 14-chapter formal specification
-- 13,575 tests, including a 253-program conformance suite
+- 13,686 tests, including a 253-program conformance suite
 - 43 working example programs
 - 164 built-in functions covering strings, arrays, math, parsing, and data types
 - Four built-in abilities (Eq, Ord, Hash, Show) with constrained generics and ADT auto-derivation

diff --git a/spec/06-contracts.md b/spec/06-contracts.md
@@ -245,7 +245,7 @@ A practical implication: if a function `bad` has an implementation that doesn't
 **Opaque effect values.** A `let` whose value is an effect operation's result (`let @Int = random_int(0, 9);`) binds a fresh *opaque* constant of the value's type in the verification model, and translation of the body continues past it ([#764](https://github.com/aallan/vera/issues/764), [#1199](https://github.com/aallan/vera/issues/1199)); the same applies per-component to a tuple destructure whose source cannot be projected.  Two rules govern how obligations over an opaque value classify:
 
 - **Preconditions stay strict.**  A call precondition that cannot be proven — because the argument is opaque — is reported (**E501**), exactly as for an opaque function result: establishing the precondition is the caller's obligation, and the repair is an `assert`/`assume` on the value, whose fact flows into the check ([#804](https://github.com/aallan/vera/issues/804)).
-- **A goal that holds only from a disclosed fact is Tier 3, not Tier 1.**  A declared-type fact whose own obligation was reported as neither proved nor guarded is not a fact the run established.  A postcondition provable only once it is assumed is reported **E534** and checked at run time; a call precondition in the same position takes the E532 demotion rather than an E501 violation, since no violating model exists.  This rule is **independent of module layout** ([#1399](https://github.com/aallan/vera/issues/1399)): a disclosure made in an imported module demotes its importer exactly as an in-module one does, and transitively along the import graph, so splitting a program across files never turns a Tier-3 truth into a Tier-1 proof.  A module's disclosed set is derived from that module's own verification — the same set `vera verify <module>` reports — and read by its importers; the importer's obligation stream stays its own.
+- **A goal that holds only from a disclosed fact is Tier 3, not Tier 1.**  A declared-type fact whose own obligation was reported as neither proved nor guarded is not a fact the run established.  A postcondition provable only once it is assumed is reported **E534** and checked at run time; a call precondition in the same position takes the E532 demotion rather than an E501 violation, since no violating model exists.  Disclosure is a property of the **value**, not of the expression that names it ([#1406](https://github.com/aallan/vera/issues/1406), [#1407](https://github.com/aallan/vera/issues/1407)): the demotion is the same whether the disclosed result reaches the goal directly, through a `let` binding or a chain of them, through a projection or a destructure, joined from a branch that discloses on one arm, or taken apart and rebuilt — a value CONSTRUCTED from a disclosed component is disclosed, because the component's fact is what the reconstruction rests on.  A function whose own result is such a value is itself disclosed for its callers, however many forwarding hops separate them — recorded against the function it belongs to, so a `where` helper's disclosure is scoped to its top-level owner and never reaches a same-named helper under a different one — so a wrapper, a pipe or a `where` helper carries the fact's provenance rather than laundering it.  The rule binds every reader of the fact, not only a `match` arm's bindings ([#1413](https://github.com/aallan/vera/issues/1413)): a projected value re-narrowing into a second refinement, and a `let`-destructure's component invariant, are each Tier 3 when the goal *depends* on a fact withheld because the value they read from was disclosed — and Tier 1 still when it does not, the withheld facts being offered back only after a proof without them fails, so a goal that never needed one keeps it.  This rule is **independent of module layout** ([#1399](https://github.com/aallan/vera/issues/1399)): a disclosure made in an imported module demotes its importer exactly as an in-module one does, and transitively along the import graph, so splitting a program across files never turns a Tier-3 truth into a Tier-1 proof.  A module's disclosed set is derived from that module's own verification — the same set `vera verify <module>` reports — and read by its importers; the importer's obligation stream stays its own.
 - **An `assert` that is neither proved nor refuted says so.**  A body `assert(P)` the solver cannot settle falls to a runtime check and MUST be reported (**E535**), so the construct that moved the tier count is named — the same disclosure `requires` (E521), `ensures` (E522) and `decreases` (E525) already carry.
 - **Refutations over opaque values are not violations.**  A postcondition, refined return, or primitive-operation obligation that *fails* to prove where the goal mentions an opaque constant demotes to a runtime-checked **Tier 3** obligation (`E522` for a postcondition) rather than reporting a definite violation — a countermodel over an unconstrained stand-in says nothing about the value the effect actually produces (`random_int(1, 9)` never returns `0`, but its stand-in would "witness" a zero divisor).  A proof that *succeeds* despite the opacity is kept at Tier 1: it holds for every value the constant could take.  The demotion is per-obligation, not per-function — a genuine violation elsewhere in the same body is still reported.