v0.1.8

Added

• Vim and Neovim support (#1155, contributed by @chromy). A Vim 8+/Neovim package under editors/vim-veralang/ — ftdetect, ftplugin and syntax — ported from the VS Code TextMate grammar. It registers the filetype as veralang, not vera: Vim has shipped an unrelated vera filetype since 2005 for the Synopsys hardware verification language, and because $VIMRUNTIME precedes pack/*/start in runtimepath, claiming that name would let the built-in syntax set b:current_syntax first and this plugin's own files would then exit silently through their own guard. It is the most current of the three editor integrations: it knows all ten effects in vera effects --json, where the VS Code and TextMate grammars are four behind. The remaining drift — those two grammars, and the Eq/Hash/Ord/Show abilities that no grammar knows — is tracked in #1156.

Changed

• The ruff rule set is declared explicitly instead of inherited, and five of the rules 0.16 turned on are adopted (#1166). The project had no [tool.ruff] section, so its lint policy was whatever ruff shipped as the default — meaning any ruff release could redefine the project's standards without review. 0.16.0 did exactly that, replacing the default selection wholesale (isort, pylint, simplify, blind-except, pyupgrade, pyi, perflint, pie, tryceratops, datetimez, refurb) and taking a clean tree to 805 errors across 36 rules; the <0.16 version cap had been suppressing the symptom. E4/E7/E9/F are ruff's pre-0.16 default, verified byte-identical against seeded violations under both 0.15.21 and 0.16.0, so declaring them preserves today's behaviour rather than narrowing it. A ruff upgrade is now a tool change rather than a policy change, and the version range widens to <0.17.

  Adopted on top of that pin, each because it names a defect class the project already treats as real. Every site was triaged before the edit; none of the five was silenced with a blanket ignore:

  Rule	Sites	What the sweep found
  PLW1510	107	Every site turned out correct: each asserts returncode itself, inspects stdout for the CLI's OK: sentinel, or is a helper returning CompletedProcess for a caller to inspect. The value was the forced triage; check=False now records its result in the code.
  RUF100	28	Suppressions aimed at nothing — N802, N815, N818, SIM117, dead E402 — which would have masked the next real violation on those lines. Two carried a real justification in their prose, kept as ordinary comments.
  BLE001	32	All deliberate boundaries: a host FFI call whose every failure must become a Result.Err value, an SMT projection falling back to Tier 3, a doc-example runner that reports a failure instead of dying. Narrowing any would turn a graceful fallback into a crash, so each states its reason instead.
  RUF012	25	Read-only lookup tables — operator maps in the WASM emitters, fixture tables on pytest classes — now ClassVar, which is both the documentation the rule asks for and something mypy enforces.
  SIM115	13	All the Windows fixture pattern TESTING.md mandates (delete=False + explicit close + finally unlink, because Windows cannot reopen a held file). No handle leaks; the rule's worth is that a new unclosed open() cannot be added silently.

  Review turned two of the BLE001 sites from justifications into narrowings, which is the better answer where it is available. _parse_interp_expr in vera/transform.py caught every exception around the synthesized wrapper's parse and reported it as "Invalid expression in string interpolation" — so a compiler bug anywhere inside parse blamed the user's source for something it did not cause. parse funnels every genuine syntax failure through ParseError (its own malformed-comment diagnostics included), verified against syntax errors, unterminated block comments, null bytes and 20,000-deep nesting, so that is the only thing worth converting and anything else now propagates as itself. The two tests/test_browser.py parity tests caught bare Exception and asserted only that something was raised, which an unrelated Python-side failure would have satisfied; they now catch WasmTrapError and pin kind to contract_violation and overflow respectively. scripts/check_examples.py gained the exit-code half of its success check — the same defect class PLW1510 names, in a gate that had been reading only stdout.

  S is declared alongside them, because a command-line --select replaces the configured list rather than extending it: the security gate runs ruff check --select S vera/, so without S in the config RUF100 would read vera/'s 57 security suppressions as aimed at nothing and strip them, failing the next CI run. Declaring it means ruff check . reproduces that gate instead of depending on how CI spells its arguments; tests/ and scripts/ opt out, as they were never in its scope. The remaining ~500 findings are style and modernisation — I001 import ordering chief among them, which has no basis here while the project does not run ruff format — and #1166 records which were declined and why.

Security

• brace-expansion 5.0.7 → 5.0.8 in the VS Code extension, closing GHSA-mh99-v99m-4gvg — a high-severity denial of service where an unbounded expansion length crashes the process out of memory. Affects <= 5.0.7; 5.0.8 is the first patched version. This is a runtime dependency, not build tooling: the chain is vscode-languageclient (a root dependencies entry) → minimatch → brace-expansion, and esbuild.js bundles with external: ["vscode"] alone, so everything else is carried into the shipped dist/extension.js. The published 0.2.0 extension therefore contains the vulnerable version, so the extension is bumped to 0.2.1 — package.json, both version fields in package-lock.json, and its own CHANGELOG.md — and the fix reaches users when that build is uploaded to the Marketplace, not when this merges. The 0.2.0 section is left describing what 0.2.0 actually was, vulnerable dependency included, rather than being retroactively corrected. Whether the vulnerable path is reachable from how the language client uses minimatch was not established either way, and the fix does not depend on the answer. The dependency's node engines range narrows with the bump (18 dropped), which changes nothing here — the extension targets VS Code ^1.91.0 and both CI workflows build on Node 22. Dependabot proposed the identical lockfile change as #1167, closed in favour of this PR after confirming the two produce a byte-identical package-lock.json.

Fixed

• Only let bindings can carry compile-time provenance, enforced rather than documented (#1164). Binding.literal_str (#309) and array_len (#1160) are populated solely for let bindings; that was a comment plus discipline at one call site. For literal_str it is the E207 gate itself — probed by bypassing it and giving param bindings a literal value, after which DB.execute(@String.0, []) type-checks clean, i.e. the textbook injection is accepted. A __post_init__ guard now rejects provenance on any non-let source, placed on the dataclass rather than in TypeEnv.bind because vera/checker/control.py constructs a Binding directly for match patterns and bypasses bind entirely. ValueError, not assert: a load-bearing guard must survive -O, and the ruff --select S lint rejects asserts used this way. Covered for every binding source the checker uses, with positive controls for the "" and 0 edge values a truthiness-based guard would wrongly reject.

• E208 now follows a let chain, as E207 already did (#1160). The SQL placeholder/parameter arity check only looked at the syntax at the call site, so moving a params array into a let for readability silently dropped a compile-time check — identical array, identical static size, only an indirection differs:

  DB.query("... a = ? AND b = ?", [Some(@String.0)])        -- E208
  let @Array<Option<String>> = [Some(@String.0)];
  DB.query("... a = ? AND b = ?", @Array<Option<String>>.0)  -- accepted
  

  Binding gains an eager array_len alongside literal_str, computed at the same moment and for the same reason — in the value's own scope, before bind() shifts slot indices — and a new resolve_array_len in vera/checker/sql.py reads it. A completeness fix, not a soundness one: the mismatch already failed at run time as Result.Err, so the change only converts a runtime failure into a compile-time one. Every unresolvable shape still returns None and defers to the driver; the resolver deliberately does not fold array_concat or any other builtin, since each extra shape is another way to compute a wrong length. Spec §9.5.7, SKILL.md and AGENTS.md describe the check in those terms; the let path is what they were missing, though the wording still reads wider than the check is — a block-wrapped or if-wrapped literal array is statically sized and deliberately defers. Review also found and fixed a second instance of the same bug class introduced by the first cut of this fix: the resolvers looked bindings up through the syntactic renderer in vera/slots.py, while TypeEnv.bind keys them through the checker's alias-resolving one, so a type alias inside a type argument (@Array<Option<Txt>> where type Txt = String) missed and silently deferred. Both resolvers now take the checker's _slot_ref_key, which is also what makes the ordinary parameterised case work at all: SlotRef.type_name is only the base name — @Array<Option<String>> is "Array" — so the bare lookup the first draft used matched no binding and silently resolved to None. Conformance ch09_sql_placeholder_let_mismatch_rejected.

Documentation

• Vera Language 0.2.0 is now available from the VS Code Marketplace (#1106). The public veralang.vera-language package was downloaded and compared file-for-file with a fresh build from main, then installed successfully through VS Code's Marketplace CLI in a clean isolated profile. The installation docs now expose that verified route and distinguish the extension from the separate veralang[lsp] Python extra it launches for diagnostics, hover, slot navigation, and typed-hole completion.

• The landing page's project facts are gated against the live codebase (#528). docs/index.html states counts in prose — built-in functions, algebraic effects, spec chapters, conformance programs, worked examples — that drift silently as the codebase moves; two were stale before anyone noticed ("six algebraic effects" when there were seven, a 77-program suite when there were 80). scripts/check_doc_counts.py now checks each against its live source, and the page stays hand-edited rather than becoming a template, which is the convention for that file. Effects are checked as a count and a membership list, in both places the page enumerates them — the status paragraph and the reference card, a second hand-maintained mirror that had no gate at all. That matters because the historical drift was a name missing from a list rather than a wrong total, which a count-only check cannot see. A pattern matching nothing is itself an error, so a reworded sentence fails loudly instead of silently switching its own check off. The version string is left to scripts/check_version_sync.py, which already owns this file for it.

• Every diagnostic code now reports the release that introduced it (#1157). vera errors --json carried a since field that was null for all 145 codes — deliberately, as attribution was judged high-effort. It is not: codes are stable identifiers the registry never renames, so the version derives mechanically from the release tags — for each tag, the ERROR_CODES keys in git show <tag>:vera/errors.py; a code's since is the first tag containing it. That is more reliable than the built-in attribution it sits beside, which had to trace names through the #288 rename pass by hand. The result is cross-checked against HISTORY.md's independent record of each release: the scan attributes exactly E207/E208/E209/E217 to v0.1.7 and the E02x comment diagnostics to v0.1.6, matching what those rows say without having read them. 80 codes date to v0.0.43, which is not a floor — that release introduced error codes at all, and no error_code= call site exists before it. Unlike the built-in table this one is complete rather than best-effort, and held that way: ERROR_CODES is a closed enumeration, so a new code added without a since entry fails test_since_covers_every_code rather than silently reporting null.

• The vera/README.md module map is gated instead of hand-maintained (#1150). Its per-module line counts had drifted silently after every refactor — checker/calls.py cited 610 lines against a real 1,556 — and ten modules had no row at all, including checker/sql.py (#309) and runtime/db.py (#229), which shipped without one. scripts/check_doc_counts.py now checks the table on two independent axes: cited line counts against the tree, with the same ±10% band the KNOWN_ISSUES.md refactoring table uses (the numbers convey relative scale, so exact pinning would tax every compiler PR with a doc edit), and coverage — exact, no tolerance — that every module on disk has a row. Coverage is the half a count check cannot do: a missing row has no cited number to be wrong. A pkg/ row aggregates that package's modules, and the per-effect host-binding row pins its own ×N multiplicity, so adding an effect family trips the gate. All 54 counts refreshed, the ten missing rows added, and the runtime family row corrected from ×13 to ×14.

• Three compiler docstrings that still described the pre-v0.1.7 world are corrected (#1161). vera/runtime/db.py announced the #309 checker gate as forthcoming and the runtime ?-parameterisation as "the guarantee in force" — #309 shipped in v0.1.7, so the host now describes itself as the second layer under a compile-time one. count_placeholders in vera/checker/sql.py said its None return defers the arity check to sqlite3 at run time; vera/checker/calls.py turns that None into a hard E209, so no such program reaches run time at all, and the docstring now says None means "not countable" rather than "allowed through". TESTING.md carried the same deferral framing.

• The SQL-injection guarantee is now advertised everywhere the language is, not just implemented — the post-v0.1.7 documentation sweep found the v0.1.7 flagship (<DB> + E207) fully documented in SKILL.md and the spec but absent from every code-sample showcase and orientation surface — the landing page carried only a reference-card line, and README, FAQ, EXAMPLES, PYPI_README, TOOLCHAIN, AGENTS, and ENVIRONMENT had nothing. README gains a fourth "What Vera looks like" block (SQL injection won't compile), the landing page gains a matching showcase sample (mirrored in docs/index.md via build_index_md), FAQ gains "Is SQL injection really a compile-time error?", EXAMPLES.md gains the SQL tour stop with the real E207 diagnostic, TOOLCHAIN.md gains the VERA_DB_URL run recipe, and PYPI_README states the claim. VERA_DB_URL joins ENVIRONMENT.md (table + section — its own add-a-variable checklist had been skipped), AGENTS.md gains Essential rule 8 (literal SQL + ? placeholders, E207/E208), DESIGN.md's effects row and SKILL.md's wasi-p2 rejected-family list add the missing DB. The introspection registries were audited against their compiler sources and are current (effects/builtins derive from the live TypeEnv tables, plus the documented hand-listed Exn entry; errors has 145/145 parity incl. E207–E209/E217) — the one gap, an always-null since field on error codes, is filed as #1157. ROADMAP reconciled against the tracker: #1103, #1106, #1126, #1156, and #1157 gain rows; the closed pip-upgrade-audit item leaves. The examples/tests workaround sweep found nothing stale.

• The VeraBench results are refreshed to the current sweep, run on benchmark v0.0.16, across the website, docs/index.md, README, FAQ, and DE_BRUIJN.md. The lineup is nine models across three providers over 60 problems, and the metric is % solved (pass@1): a refusal, a compile failure, a crash and a wrong answer all count alike as not solved. Seven of the nine models write 100% correct Vera, and against Python Vera wins outright for four of the nine, draws with three and loses two. The figures these replace came from the v0.0.7 sweep — six models, 50 problems, Kimi K2.5 as the headline — and reported run_correct, which was measured only over attempts that compiled, so a model that refused or failed to compile shrank its own denominator and scored higher for answering less. The site section also gains a regenerated delta chart on a transparent background. FAQ.md drops the claim that De Bruijn slot ordering is the dominant failure mode — a v0.0.7-era finding the current report does not support — and cites the Vera-against-Aver comparison in its place: two languages absent from every training set, differing chiefly in that Aver has ordinary variable names and Vera has none. DE_BRUIJN.md likewise scopes its slot-ordering result to the early snapshot it came from, rather than asserting it as current, and cites that comparison, which tests the document's thesis directly.

• docs/index.md — the Markdown companion agents fetch instead of the landing page — carries the refreshed benchmark section. It is generated by build_index_md() in scripts/build_site.py, which holds the landing page's substance as hand-maintained prose rather than deriving it from docs/index.html, so an edit to the HTML does not propagate. check_site_assets.py cannot catch the resulting drift: it regenerates from that same function and compares, so both sides of the comparison move together and a stale generator validates as up-to-date. The benchmark block in the generator is updated to match the HTML; the structural gap is tracked in #1154.