v0.1.1

Added

• The documentation now carries a hand-authored SVG diagram set — thirty-three figures across the spec, the compiler README, and the top-level docs (assets/diagrams/). The second wave adds the subtyping and effect-row lattices (§2.8, §7.8), module resolution with the transitive-visibility rule (§8.6), the async model and the vera serve request lifecycle (§9.5), closure layout + call_indirect dispatch (§11.10), browser import introspection (§12.9.1), the WASI arena and server-world sequence (§13.3, §13.7), the FAQ's three verification layers, contract-driven-testing loop, and Dafny/Lean/Koka/F* comparison matrix, the CONTRIBUTING gate pipeline, the DE_BRUIJN binding-stack timeline, and the host-binding-families map (vera/README.md). The headline is the overall compiler architecture diagram vera/README.md lacked entirely; alongside it: the spec §11.1 pipeline, the §12.5 memory layout and a new $alloc/mark-sweep GC flow, the §13.2 WASI component + dispatch table, the §6.8 three-tier verification decision flow, the §7.5.2 effect-handler suspend/resume sequence, the wasmtime embedding chain, the checker's three passes, Z3 proof-by-refutation, De Bruijn slot resolution (two figures, shared with DE_BRUIJN.md), the Diagnostic record, the CLI↔pipeline map (TOOLCHAIN.md), the three-layer/four-level testing model (TESTING.md), the LSP proof-delta session (LSP_SERVER.md), a by-the-numbers growth chart (HISTORY.md), and a workflow hero + the architecture in README.md. Every diagram that replaced an ASCII original keeps the text in a collapsed <details> block tagged text — the docs feed llms-full.txt and agents reading files in a terminal, and images are invisible to both — and no diagram carries live counts (they drift outside check_doc_counts.py's reach; the one exception, the growth chart, plots the historical release columns and says so). The architecture and pipeline figures draw the check → {verify | compile} fork truthfully — vera compile does not consume verify results and contract guards are always emitted — where the replaced ASCII's "runtime contract insertion for Tier 3" caption echoed the spec drift tracked in #958. The landing page gains its own figure in the site's bolder design language — docs/loop-web.svg, the write → prove → ship loop with the diagnostics return, embedded in docs/index.html §Why and mirrored into the generated index.md. The set's design system, conventions, and inventory are documented in assets/diagrams/README.md; the README.md project-structure tree's stale module counts (11 → 13 codegen, 9 → 19 wasm) ride along.
• The canonical E001 diagnostic is now guarded against drift in all five of its documentation mirrors (#829). TestErrorDisplaySync already compared README.md, docs/index.html and spec/00-introduction.md against the diagnostic generated from vera/errors.py, but two mirrors were unguarded — AGENTS.md's example --json block, and the hardcoded example in scripts/build_site.py that generates docs/index.md — and #826 had already drifted the ungated pair. Both are now compared. AGENTS.md's error_code / spec_ref / fix are matched exactly (the extractor json.loads the block, so the escaping is resolved and every field is directly comparable) and its ellipsis-truncated description / rationale are prefix-compared; build_site.py's block is extracted by anchoring on the closing code fence rather than on the spec_ref text, so a spec_ref drift yields a precise Expected/Got diff instead of an opaque "block not found". Every guard is mutation-validated — drifting any mirror, or the canonical diagnostic, turns the corresponding test RED. The example is still hand-duplicated across the five mirrors; single-sourcing it so nothing can drift is tracked in #954. External contribution by @chethanuk.

Changed

• ROADMAP.md is reworked into a staged sprint plan. The tier/milestone mix is replaced by six themed stages continuing HISTORY.md's numbering — Stage 19 verification completeness, 20 single-source, 21 effect hardening, 22 the verified tool server, 23 agent experience, 24 browser — each with a rationale, an exit criterion, and an issue table, ordered from the design principles (verification truth first, then structural drift-proofing, then the flagship's capabilities, then the experience around them). The Stage 17 burndown set the model: a stage is a concentrated sprint over a coherent issue class, and it moves to HISTORY.md when its table empties. All 100 open issues are placed exactly once (staged, horizon-arc, ongoing, not-doing-now, or speculative; verified mechanically), pulling in the verification-limitation family that previously lived only in KNOWN_ISSUES.md; the browser sync-XHR fix (#355) moves from Http hardening to the browser sprint since every fix option shares the JSPI suspend machinery. Rides along: DESIGN.md's module row claimed "explicit re-exports", which don't exist (#127 is open) — it now says public/private visibility and points at #127.

Fixed

• A six-auditor documentation-consistency sweep reconciled every stale claim it could verify against the tree, the registry, and the tracker. The one behavioural-claim error: vera/README.md §Runtime contracts still described the pre-#957 world — codegen "classifies contracts using the verifier's tier results" and omits Tier-1 guards — contradicting the architecture diagram above it; it now states the truth (compile never consults the verifier; guards are always emitted; the §11.8 aspiration stays tracked in #958). The rest is drift, each verified before fixing: SKILL.md's conformance count (103 → 143) and its spec table gaining the Chapter 13 row; the CLAUDE.md/AGENTS.md pipeline gaining the resolve stage; FAQ's feature bullets gaining IO.read_char and the Exn<T> effect; README's "three-tier verification" delivered-claim scoped to the two implemented tiers; DESIGN.md's effect lists gaining HttpServer (and Random/Diverge rows) on a list that claims to mirror vera effects --json, its Tier-1 coverage sentence aligned to spec §6.8, and the tiers + effect-row diagrams embedded; KNOWN_ISSUES gaining rows for the open #439 and #770 limitations; HISTORY's stage index gaining Stages 16–17 and the intro catching up to 94 development days; vera/README.md's module-map line counts regenerated from disk (worst drift: verifier.py listed at 1,005 lines, actually 6,582); spec §12's Random prose no longer citing the closed #465 as a tracker and the heap-growth wording unified to "toward higher addresses"; and build_site.py now rewrites image embeds to raw URLs (a blob/ page is not image bytes), fixing the four diagrams inlined into llms-full.txt. Examples and conformance fixtures came back clean — no workaround shapes for fixed bugs survive there.

• Five stale bug-era annotations are retired from the test suite, each verified by running the affected tests before and after — found by the sweep's test auditors: the #869 table-forcing array_fold is removed from the monomorphize fixture (the fixture itself is now the regression pin, sum unchanged); the #570-era "1,000 elements to stay under the bug threshold" GC graph is promoted to the true 5,000-element Array<Box> wide graph its docstring always intended; the #516 module docstring no longer defers "Stage 2 (source mapping) and Stage 3 (Fix: paragraphs)" as future work — both shipped (v0.0.124/v0.0.125) and are exercised throughout the file; ch09_decimal now exercises decimal_compare through a three-arm Ordering match (the "not yet supported in codegen" note was disproven by running it); and the #773 scalar-only-Eq parenthetical speaks in the past tense.

• The verifier no longer proves false postconditions: a callee's ensures is now assumed only on the paths that establish it (#957). _translate_call_with_info (vera/smt.py) assumed each callee ensures — and each refined return's predicate — with a bare self.solver.add(...), which lands on the solver's base assertion stack. check_valid folds _path_conditions around the goal only, so a fact learned inside an if outlived the branch and became an unconditional fact about the caller's own slots (_build_callee_env binds the callee's parameters to the caller's terms). The escaped fact is circular: dec5 requires(@Nat.0 >= 5) ensures(@Nat.result == @Nat.0 - 5) injects ret == @Nat.0 - 5, which with @Nat's implicit ret >= 0 entails @Nat.0 >= 5 — the very precondition the branch guard existed to establish. A caller's false ensures(@Nat.0 >= 5) then discharged, and vera verify printed OK / 6 verified (Tier 1) with no diagnostic for a program that vera run traps on. Worse, two calls in mutually-exclusive arms inject contradictory facts, the base solver goes UNSAT, and every obligation discharges vacuously — silently deleting real E501 diagnostics, including the ones the #776 fix above adds. Each injected fact is now wrapped by _guard_fact in z3.Implies(z3.And(*self._path_conditions), fact), matching the idiom _translate_match already used; the call translator was the only site that did not. Same soundness as discarding the facts, strictly more precision. Behaviour-neutral across all 143 conformance programs and 37 examples (tier1 1,464 → 1,464, tier3 594 → 594, no diagnostic changes) and a legitimately branch-guarded call is not over-rejected. Note that the compiled program was never affected: vera compile does not consult the verifier, so the runtime contract_fail guard is emitted regardless of tier — the break was in vera verify's claim. That mitigation is accidental rather than designed, and spec/11-compilation.md §11.8 (which promises Tier-1 contracts are omitted) is tracked as the drift it is in #958. Found by the adversarial review of #953.

• A call's precondition is now statically checked (E501) even when the call sits inside an effect-operation argument (e.g. IO.print(need_pos(...))) (#776). translate_expr (vera/smt.py) had no QualifiedCall branch, so an effect op (Module.op(args)) fell through to return None without recursing into its arguments — a precondition-bearing call passed as an argument was never visited, and no E501 fired for a violated requires(...). A QualifiedCall branch now walks each argument via translate_expr for the E501 precondition side effect (the #727 span-keyed dedup keeps it duplicate-free) and returns None — the effect op itself is still not Z3-translated, since its result is chosen by the handler and translating an effect in a contract would be unsound (pinned by test_effect_op_never_becomes_a_z3_term: returning an argument's term instead makes the verifier prove a postcondition only the handler could satisfy, reporting verified where it should report tier3). Translating a FnCall argument does more than record its E501: it also assumes the callee's ensures. That assumption is scoped to the branch it was learned in by the new _guard_fact (see the next entry) — without it, routing effect-op arguments into the call translator would have converted programs main correctly rejected into programs it silently accepted. Mirrors the #730 statement-position (ExprStmt) handling, whose walk reaches the same unguarded assumption and is tracked separately.

• The diagnostic-fields gate's plumbing-skip no longer swallows a stray Diagnostic (#827). scripts/check_diagnostic_fields.py exempted every Diagnostic(...) lexically inside any function named _error / _warning, on the premise that such a construction is the helper's own plumbing. The name alone is not enough: a second, under-tagged ctor in the same helper (say, in an else branch), or a module-level function coincidentally named _error, escaped all three of the field-presence, spec_ref-validity and error_code-registration passes — #826 had propagated the same name-based skip into the latter two. Latent rather than live (all five real helpers in vera/ construct exactly one Diagnostic each, so nothing escaped in practice), but a blind spot in the gate that exists to close exactly this class of silent under-reporting. A ctor is now skipped only when its enclosing function is a genuine helper method — a class member with a self receiver, so a module-level or @staticmethod look-alike is inspected, not exempted — and it is that method's sole own-scope construction, counted without descending into nested def / lambda / class scopes. A helper holding two constructions is ambiguous: neither is skipped, and both are inspected. Counting every own-scope construction (rather than only the one structurally returned or .append(...)-ed) is what makes the rule sound — a helper that binds its real diagnostic to a local first (d = Diagnostic(...), then self.errors.append(d)) would otherwise leave a stray direct ctor as the only recognised construction, which would then be elected as the helper's own and skipped. It also means an ordinary hoist-to-a-local refactor no longer trips the gate on spec_ref is not a string literal. "Own scope" is the helper's body: a Diagnostic(...) written in a decorator argument, a parameter default, or a return annotation is evaluated in the enclosing scope, is never the helper's plumbing, and is always inspected — counting those would let one be elected as the helper's sole construction and skipped, which is the escape this gate exists to prevent. Every exemption therefore lies inside a function span the previous rule already exempted, so the exempt set can only shrink and the change cannot open an escape; on vera/ it resolves to the same five plumbing ctors as before. External contribution by @chethanuk.

• The landing page's loop figure is rebalanced and its claims audited against the tree. docs/loop-web.svg carried 70 canvas-units of dead space above the drawing and 166 to its right (vs 30 left / 18 below), so the embed rendered top-heavy and visually left-shifted; the viewBox is recropped symmetric (12 units each side, browser-measured) and the embed's margins equalised — 48px of air above and below. The audit that rode along, every claim verified against the registry or a live run: the effect enumeration gains Diverge and its count corrects to nine (vera effects --json; the same one-word gap in README.md rides along); the Inference provider list gains Mistral (vera/runtime/inference.py detects four keys, both here and in the generated index.md); the three-tier feature card is scoped to what shipped, mirroring README's phrasing (the Z3-guided middle tier is specified, not implemented); the WASI showcase block now shows vera compile --target wasi-p2 --world server's actual output line and a consistent examples/http_server.wasm artifact path (previous text was a paraphrase; the wasmtime serve banner was verified against a real run); and the safe_divide / classify_sentiment samples link their examples/ counterparts the way the fizzbuzz sample always did — with the fizzbuzz link itself backfilled into the generated index.md, which had never carried it.

Security

• The wasmtime runtime floor is raised to >=46.0.1, off a release affected by GHSA-4ch3-9j33-3pmj (medium; #949). The advisory is a wasmtime-wasi FilePerms bypass on hard-link and rename destinations; its affected range includes 45.0.0, which uv.lock had pinned. The upstream core backport is 45.0.3, but the wasmtime-py binding never tagged a 45.0.x patch — 46.0.1 is the only patched binding release, so the floor moves up a major rather than sideways. Vera's own WASI host (vera/runtime/wasi_host.py) is not exploitable: it preopens with the default READ_WRITE FilePerms, so there is no restricted permission for a link/rename to bypass. CI already resolved the unbounded floor to 46.0.1; this pins the lockfile and the declared floor off the affected release for minimum-version resolvers (uv sync, distro packagers, pre-existing venvs).