v0.1.7

Fixed

• A bare (unqualified) effect-operation call the WASM backend cannot route is now a clean checker error (#1148). An effect op called without its qualifier — query("SELECT ...", []), print("hi") — type-checked but failed vera compile with a confusing Function 'query' is not defined in this module, a check-green→codegen-fail disagreement. Codegen routes a bare op call only for the built-in State / Exn ops (get / put / throw, backed by host cells) or when the effect is handled by an enclosing handle block; every other bare op — IO / DB / Http / Inference / Random and user effects — has no bare route. The checker now rejects the unroutable case at check time (E217, the safe direction of the disagreement), steering to the qualified Effect.op(...) spelling or a handle[Effect] block, via a handled-effect stack in _check_handle that mirrors codegen's routing capability. The State/Exn carve-out keys on the op name as well as the effect name, so a user effect State / effect Exn shadow declaring some other op is still rejected rather than silently miscompiled. Surfaced by the #309 adversarial reviews. Spec §7.4.

• A guest-controlled out-of-bounds (ptr, len) no longer crashes the host with SIGBUS (#1145). _read_wasm_string — the reader behind every host import that takes a String argument (42 call sites across 12 runtime modules) — sliced WASM linear memory through a raw ctypes pointer (bytes(buf[ptr:ptr + length])) with no bounds check, so an out-of-range pair (from a codegen bug, or a program that computes a bad (ptr, len)) read past the memory region into wasmtime's guard page and killed the whole process with SIGBUS / KERN_PROTECTION_FAILURE. The safe_utf8_decode contract (#589 / #592) did not cover it: the crash happens inside bytes(buf[...]), before decoding is ever reached. _read_wasm_string now bounds-checks (ptr, len) against the live memory size — as its post-run sibling _read_string_export already did — and raises a wasmtime.WasmtimeError carrying the out of bounds memory access reason, which execute() classifies as a clean out_of_bounds trap (backtrace, Fix: paragraph, buffered output preserved) identical to a native guest OOB, rather than a host crash.

• The @Float64 FP-soundness regression tests no longer flake on a slow CI runner (#1121). test_rounding_relation_not_proved and its reflexive-equality sibling asserted the obligation came back exactly violated, but the docstring — and the soundness property they exist to guard — only require that a false FP property is not proved. When Z3 exhausted its budget on the slowest matrix cell and the obligation fell to the conservative Tier-3 runtime check (timeout), the assertion failed spuriously and red-flagged unrelated PRs. Widened to status != "verified" (proving a false property remains a hard failure), with a guard that stubs the validity query to unknown — pinning the Tier-3 branch deterministically, without depending on solver latency — so the accept-set cannot silently narrow back.

• SKILL.md no longer teaches the pre-#1003 State-handler with idiom (#1141). The sum_with_state example and the handler-syntax reference block showed put(@Int) -> { resume(()) } with @Int = @Int.0; post-#1003 (spec §7.5.2) the state slot in a put clause is the value before the store, so with @Int = @Int.0 overrides the store back to the old state — a with that silently undoes the put. SKILL.md is fetched live as the reference LLMs get at benchmark time, so a model copying the idiom into a direct handled-body put produced code that checks, verifies, and computes the wrong answer. The canonical put(@Int) -> { resume(()) } (intrinsic store) is now shown throughout, and the reference block documents with as a store override for transforming the written value (@T.0 = pre-store state, @T.1 = the argument; example with @Int = @Int.1 * 2).

• vera fmt --check and the corpus gate agree on line endings. --check read files with universal-newline translation, so a CRLF file compared equal to its LF formatting and was reported canonical while the byte-reading corpus gate rejected it. cmd_fmt now reads bytes and treats any carriage return as non-canonical (spec §1.8 rule 10, which now names LF explicitly). A .gitattributes marks *.vera as eol=lf so a Windows checkout does not arrive as CRLF and fail the pre-commit gate. Spec §1.8 rule 2's scope sentence is corrected: the rule is stated for statement, block-result, arm-body and binding-value positions, with sub-expression flattening tracked as #1139 rather than claimed as already unconditional.

• vera fmt refuses to emit output that breaks its own contract — format_source now checks three postconditions on every call and raises a FormatterPostconditionError naming the violated invariant instead of returning corrupt output: the output re-parses, the comment-content multiset is conserved, and a second pass is a fixed point (DESIGN principle 5 applied to the toolchain itself; measured ~3.5 ms per file over the 209-program corpus). A structural backstop makes comment deletion impossible by construction: any comment bucket no emitter consumed is emitted at the end of its enclosing declaration, rule 11's sanctioned fallback, rather than being dropped.

• vera fmt no longer deletes own-line comments in value position — a comment between let @T = and a multi-line match/if/handle value, inside a flattened redundant block, or inside a flattened match-arm block was silently discarded; a statement-bearing block as a let value additionally produced output that failed to parse. All value paths now flush the construct's comment bucket before emission, and if/handle gained the span self-anchors match already had, so a comment above any of the three binds to the construct rather than drifting into its interior. Comments above a next-line plain arm body and inside multi-line handler-clause bodies now attach to their own arm and clause.

• vera fmt emits floats the lexer can read — values below 1e-4 or at/above 1e16 were emitted in Python scientific notation, which FLOAT_LIT cannot lex, so a check-clean program stopped parsing after formatting. Exponents are expanded to positional decimal form with round-trip value equality.

• vera fmt parenthesizes an indexed collection when precedence demands it — (x |> f())[0] reformatted to x |> f()[0], a different program. Collections outside the postfix-safe set are re-parenthesized, and a block in sub-expression position keeps its braces instead of silently changing evaluation.

• blank_source_lines ignores blank lines inside block comments, so a {- -} spanning an empty line no longer manufactures a phantom paragraph break, and format_source formats the source it was passed (the file argument is a diagnostic label only). FnDecl.where_span now follows the span-field convention — excluded from equality and repr, serialized as a structured span in ast --json.

• The corpus gate rejects CRLF and bare-CR line endings (canonical form is LF) and reports unreadable files — invalid UTF-8, dangling symlinks — in its broken-file list instead of aborting the sweep with a traceback.

• vera fmt keeps own-line comments above the construct they document (#1136). A comment was bound to the innermost construct whose span contained it rather than to the construct that followed it, so the three positions with no anchor of their own — contract and effects clauses, where blocks, and match arms — sent their comments to the enclosing declaration's backstop, which re-emitted them at the top of the function body. data, effect and ability declarations already anchored their members, which is why those positions looked safe. Contract, effect, arm and where spans are now anchors (where needed a new FnDecl.where_span, since the keyword had no span at all), and a blank line separating a comment block from what it documents survives instead of being swallowed. Spec §1.8 rule 11 now states leading-comment attachment explicitly; the blank-line half of it is rule 13.

• vera fmt preserves the blank lines between statements (new §1.8 rule 13). Only the gap under a comment block survived the fix above, which left the formatter inconsistent: it kept a paragraph break below a comment and deleted one between two plain statements. examples/file_io.vera lost the break before its trailing () and examples/io_operations.vera lost two. The AST records no separation at all — two statements written a page apart parse to the tree two written back to back do — so neither keeping every gap nor discarding every one is recoverable after the fact. The formatter now reads the source's blank lines directly and reproduces exactly one wherever there was one or more: between statements in a block, before a block's trailing result expression, and above an own-line comment. A gap the source did not have is never introduced, and one held against a brace is dropped, since rule 2 already gives the brace its own line. The comment-adjacent case is no longer special-cased: Comment.blank_after is gone and both halves read the same source map, so a single source gap cannot be reproduced twice.

• vera fmt no longer flattens a nested or statement-position match against §1.8 rule 2. The multi-line branch keyed on arm.body.statements being non-empty, but a block whose whole content is a single trailing expression keeps it in expr with statements empty — so { match ... } read as empty and the entire construct collapsed onto one line, closing brace and all. Statement position had the same hole. examples/file_io.vera went from 21 lines to 11 under the old formatter; a 150-character line carrying three brace pairs is now properly nested.

• vera fmt escapes characters that cannot be read in source (new §1.8 rule 12). Only six characters were re-encoded, so a parsed \u{200B} re-emitted as an invisible zero-width space. Unicode categories Cc, Cf, Cs, Co, Cn, Zl, Zp and non-ASCII Zs now emit as \u{...}; printable non-ASCII stays literal, so café 😀 is unchanged. A bidirectional override or zero-width joiner can no longer hide in a program.

• vera fmt no longer destroys a handle in sub-expression position. _fmt_handle_inline was a stub returning a literal handle[E] { ... } — the state initialiser, every clause and the in body deleted, and the output no longer parsed ([E005]). It carried # pragma: no cover on the belief the path was unreachable, but handle_expr is a bare alternative of primary_expr, so it is reachable from every operand, argument and element position. The renderer now reads the node, and the clause and state renderings are shared with the multi-line emitter so the two cannot drift apart again. Its braces share a line, which rule 2 would not choose: unparseable output is strictly worse than badly-shaped output, and giving nested constructs a multi-line path so this renderer is never reached is tracked separately.

• vera fmt applies §1.8 rule 2 in value position, not only in statement position. A match, if or handle bound by a let was flattened onto one line with its braces sharing it, while the identical construct written as a statement, as a block's result, or as a match-arm body expanded over its own lines. LetStmt and LetDestruct rendered their value through the single-line _fmt_expr path, so position — not the construct — decided which of two textual forms came out, and examples/array_utilities.vera held both a five-line if and a flat one. One construct with two textual representations is what DESIGN.md principle 3 ("every construct has exactly one textual representation") and its technical-decisions row ("no equivalent alternatives") exist to rule out, and a position-dependent form also obliges a generator to decide per site which to emit rather than applying one rule everywhere (principle 6). The expanded form is longer, which is not an argument against it: principle 2 ranks explicitness over convenience. All three statement kinds now share one rule-2 path, with the binding text (let @Int = ) on the opening line and the ; riding the closing brace; §1.8 rule 2 states the scope explicitly so it no longer has to be inferred. Separately, the comment-anchor walk now descends into a statement's value: only the statement's own start line was an anchor, so a comment written above an arm of a let-bound or statement-position match fell through to the next statement and silently documented something it was not written for. Expanding let values turns those arms into real lines, which makes the misattribution visible rather than latent. Re-canonicalising the corpus replaces 32 flattened lines with 160 across 11 programs, all of which still check and verify unchanged.

Added

• SQL injection is a compile-time error (#309). The SQL argument of DB.query / DB.execute must be literal-provenance — a string literal, a string_concat of literals, or a let chain of those. A SQL string assembled from a runtime value (a slot, a function result, or a \(expr) interpolation) is the SQL injection vector, so the checker rejects it with E207. The guarantee is a deterministic type error, not an SMT obligation: no solver, immune to timeout flakes, and effective even inside handled code where solver-based claims cannot reach. The gate keys on the effect qualifier — the same axis codegen routes a call to the host database on — so it also holds for a user-declared effect DB { ... } (the idiomatic way to use a host effect, as with effect IO), which still reaches the host and must not bypass the check. Runtime data flows only through the ? placeholders and the Array<Option<String>> params array; when both the SQL and that array are statically sized, a placeholder/parameter count mismatch is also caught at compile time (E208), while a dynamically-sized array defers the arity check to the driver. Implemented as a new leaf checker vera/checker/sql.py (resolve_literal_string — conservative-reject on every unhandled expression shape, so it can only false-reject, never wrong-accept — plus a quote-aware count_placeholders pinned differentially against sqlite3). Only anonymous ? placeholders are accepted; a numbered (?NNN) or named (:name / @name / $name) form is a compile-time error (E209), since parameters bind positionally — and placeholder detection follows sqlite3's own identifier rule, so a named parameter whose first character is non-ASCII or $ (:€x, $$x) is caught too. The gate runs on codegen's host-routing axis alone — the DB.query / DB.execute spelling codegen marshals to the host, independent of the argument's static type — so a runtime string laundered through a generic @T parameter, a user effect DB shadow declaring a non-String param, a generic effect DB<T> at unbound arity, and an imported library body carrying a non-literal query all reach the same E207: every path a runtime string could take to the database. Hardened under three external adversarial reviews (CodeRabbit, Kimi K3, Cortex) and a self-authored adversarial workflow that found and closed a generic-parameter injection bypass. No mainstream language prevents SQL injection at compile time this way. Spec §9.5.7; conformance ch09_sql_injection_rejected (E207), ch09_sql_placeholder_mismatch_rejected (E208), and ch09_sql_numbered_placeholder_rejected (E209).

• A built-in <DB> effect for SQL database access (#229). DB.execute(sql, params) runs writes (CREATE/INSERT/UPDATE/DELETE) and returns the affected-row count; DB.query(sql, params) runs a SELECT and returns the result grid. Both return Result<_, String>, so a driver error — malformed SQL, a constraint violation, an unreachable database — is the Err arm rather than a trap, so callers either propagate the Result or match its arms. A row grid marshals as Array<Array<Option<String>>>: a cell is Some(text), or None for SQL NULL, so NULL and "" stay distinct (DESIGN principle 2, no implicit behaviour). Parameters are the Array<Option<String>> second argument, bound positionally to the ? placeholders (Some(v) a value, None a NULL), so data is never spliced into the SQL text. The host reader bounds-checks every guest-controlled pointer in a parameter array — the outer array, each element pointer, and the full Some(String) cell — before it is dereferenced, so a malformed array surfaces as a clean out-of-bounds trap rather than a host SIGBUS (the #1145 class, one level deeper than the string reader). The effect is host-backed on Python's sqlite3; VERA_DB_URL selects the connection (sqlite::memory: by default, or sqlite:///path). Phase 1 is SQLite-only, single-connection, and stringly-typed — named columns and typed cells are tracked in #1143. handle[DB] is not yet available (host effects are un-mockable, #372); the browser runtime returns Err for every DB operation, and vera compile --target wasi-p2 rejects <DB> at compile time. Spec §7.7.7 and §9.5.7; examples examples/database.vera (in-memory) and examples/sqlitedb.vera (a committed on-disk SQLite file).

• The corpus is gated on canonical form (#1124). scripts/check_corpus_canonical.py compares all 209 programs (recursively) in examples/ and tests/conformance/ against vera fmt, wired into the CI lint job and pre-commit. Nothing ran vera fmt --check over the corpus before, which is how #1112 and #1123 stayed invisible — a regression that deleted every inline comment in the language passed the whole gate. A comment-count sweep cannot replace it: counting cannot see a comment that moved, and formatting reaches a fixed point either way, so both invariants stay green while a comment drifts out of the construct it documents.

• npm run check:package pins what ships inside the built VSIX (editors/vscode/check-package-contents.js, wired into the VS Code extension workflow after the packaging step). It reads the archive's own zip central directory rather than vsce ls: the two differ, because vsce synthesises extension.vsixmanifest and [Content_Types].xml, renames README/CHANGELOG/LICENSE on the way in, and re-runs vscode:prepublish while packaging — so a check run against the working tree grades a directory that no longer exists once the artifact is built. Three assertions, none derived from another: the archive's entries must match an explicit list exactly; every entry's extension must be on an allowlist, so an unrecognised type fails rather than passes; and no entry may carry an executable mode bit, which vsce preserves into the archive. The last is the only one that can see a file with a wholly inert extension arriving as mode 0755. Covered by npm test (node --test, no new dependencies) over the failure cases, since a guard that only ever passes is indistinguishable from no guard.

• An npm ecosystem entry in .github/dependabot.yml, and an npm audit step in CI — the VS Code extension's dependencies were previously monitored by neither. Neither existed: Dependabot covered only uv and github-actions, and nothing audited npm at all (dependency-audit in CI is pip-audit, Python-only). Security updates fire off GitHub's advisory database regardless of configuration, so the tree was not unwatched — but version updates need the entry, which is why a vscode-languageclient major bump first arrived bundled into a CVE fix rather than as a routine bump months earlier. The audit is scoped to production dependencies, which are what esbuild bundles into the VSIX: an advisory against a build-only package is worth knowing about but should not block an unrelated PR, since the fix is rarely ours to make. Checked in both directions — the scoped gate passes on the current tree, where the one open advisory is dev-only, and fails on the lockfile as it stood before #1129, where brace-expansion was a runtime transitive.

Documentation

• The README's licence table covers everything Vera redistributes, and its project structure names every pipeline stage. The table listed only the three Python runtime dependencies, omitting the [lsp] extra (pygls, Apache-2.0; lsprotocol, MIT) and the npm packages bundled into the .vsix — where minimatch is BlueOak-1.0.0 and semver is ISC, so the previous claim that all dependencies were "MIT or Apache-2.0" did not hold for the shipped extension. "Licence compliance is enforced by CI" also overstated: scripts/check_licenses.py runs pip-licenses and has no npm coverage at all, which the text now says. The note about chardet arriving under LGPL via cyclonedx-bom was stale in a way worth spelling out — cyclonedx-bom is not a Vera dependency and appears in no manifest; it is installed ad hoc by the separate sbom CI job, which is not the job the licence gate runs in, so neither package has ever been in the environment being checked. The same claim inside check_licenses.py is corrected. wasmtime is Apache-2.0 WITH LLVM-exception. Separately, the project-structure listing sat directly beneath the words "seven-stage pipeline" while naming six of the seven stages: resolver.py is now among them.
• v0.1.7 release documentation sweep. Aligned the spec §9.5 built-in-effects summary with the shipped set — Async, Inference, HttpServer, and DB, replacing the stale "future effects for concurrency and LLM inference" wording — removed the now-shipped #309 (contract-verified SQL) from the ROADMAP standard-library horizon, and dropped the fixed #1121 row from the KNOWN_ISSUES bugs table. The drifted, ungated vera/README module-map line counts are tracked as #1150.

Changed

• The VS Code extension moves to vscode-languageclient 10, and the packaged VSIX no longer contains a shell script (#1130). Version 10 declares an exports map that exposes only ., ./node, ./browser and ./$test/common/*, which makes every other subpath unreachable; editors/vscode/esbuild.js resolved lib/node/terminateProcess.sh out of node_modules, copied it into dist/ and marked it 0755, so a plain dependency bump failed with ERR_PACKAGE_PATH_NOT_EXPORTED before esbuild ran. Separately, and not the cause of that failure, v10 also removed the helper: termination is unchanged in substance, because v10 holds the same recursive pgrep / kill -9 process-tree walk as a string in lib/node/processes.js and pipes it to /bin/sh, with a pid regex guard added, and Windows still uses taskkill /T /F. The extension source needs no changes — LanguageClient, start(), stop(), documentSelector and outputChannelName are unchanged. The packaged artifact drops from 11 entries to 10 — JSON, JavaScript, Markdown, XML manifests and a PNG, none of them executable — which bears on the Marketplace rejection tracked in #1106 without being established as its cause. The extension's VS Code floor rises to 1.91 (from 1.82), v10's own requirement.

Security

• brace-expansion raised to 2.1.2 in the VS Code extension lockfile, off the range affected by GHSA-3jxr-9vmj-r5cp (CVE-2026-13149; GitHub severity high, CVSS 3.1 base 5.3 — availability only, AV:N/AC:L/PR:N/UI:N/S:U/C:N/I:N/A:L). The advisory is exponential-time expansion of consecutive non-expanding {} groups, reachable only by whoever supplies the glob pattern. It arrived as a runtime transitive of the language client — vscode-languageclient@9.0.1 → minimatch@5.1.9 → brace-expansion@2.1.1 — so it ships inside the VSIX, but every pattern reaching that minimatch is a document selector written in the extension's own source rather than anything a workspace or document can influence; practical exposure is correspondingly low. minimatch@5.1.9 already declares brace-expansion: ^2.0.1, which admits the patched 2.1.2, so the immediate fix was a three-field lockfile bump. The vscode-languageclient 10 upgrade in this same release then carried the dependency further still, to brace-expansion 5.0.7 by way of minimatch 10 — which is the version the shipped lockfile records.