v0.0.170

Fixed

• #727 — duplicate E501 diagnostics. A violating call site could be recorded once per translation pass: the primary body translation, the @Nat-subtraction walker's let-RHS environment rebuild, and the walker's operand discharge each re-translate the same call (a @Nat-subtraction operand in a let RHS recorded three identical E501s). The SMT layer now dedups at recording time by (call node, precondition) identity, so every topology collapses to exactly one diagnostic and one call_pre obligation per violating site — while sites that only the walker ever translates — a violating call inside a @Nat-subtraction operand in statement position, checked via the walker's operand discharge — keep their single recording rather than being suppressed. (Bare statement-position calls with no enclosing subtraction remain unchecked either way; that pre-existing gap is tracked as #730.) Translation behaviour is unchanged and the warm/cold differential oracle is untouched.
• #728 — LSP diagnostics now carry the full instruction contract. The language server's diagnostic mapping put only the description into the LSP message, so editor hovers said what broke but not how to fix it. The message now appends the rationale paragraph and the Fix: paragraph exactly as --json carries them; diagnostics without those fields map to the bare description, unchanged.
• E501 messages now speak in call-site terms. The precondition is rendered with the actual arguments substituted for the callee's parameter slots (At this call site: string_length("") > 0), and the Fix: text shows concrete code — the guard with the rendered call (if string_length("") > 0 then { classify_sentiment("") } else { ... }) and the exact requires(...) to add — instead of generic advice. Substitution honours De Bruijn most-recent-first resolution; module-qualified callees and unmappable slots keep the generic wording.

v0.0.169

Added

• LSP_SERVER.md — the language server's user manual: what an LSP server is, install (pip install -e ".[lsp]") and editor wiring, the standard feature surface (tier-annotated diagnostics, per-function verification-tier hints, hover, slot go-to-definition, typed-hole completion), the warm incremental verification core, and full request/response shapes for the four agent-facing custom methods (vera/speculativeEdit, vera/proposeEdit, vera/strengthenContract, vera/addEffect) with the typical speculate → inspect → propose loop.
• VS Code extension 0.2.0 — the extension now starts vera lsp automatically for .vera files (settings vera.lsp.enabled / vera.lsp.path, command Vera: Restart Language Server), degrading gracefully to syntax-highlighting-only when the binary or the npm install is absent. Binary resolution prefers an explicit vera.lsp.path, then a workspace-local venv (.venv/bin/vera — GUI-launched VS Code does not inherit a shell PATH, so a from-source clone works with zero configuration), then PATH; spawn failure surfaces one warning with an Open Settings action. Requires VS Code 1.82+.

Changed

• veralang.dev — the landing page's audience-addressed sections both gain the language server: §06 Get Started (the VS Code row starts vera lsp automatically; the [lsp] install path) and §07 for machines, reframed around read vs interrogate — the markdown set is how machines read Vera, the server is how they interrogate it, with a fourth agent-card and a speculativeEdit proof-delta sample. LSP_SERVER.md is indexed in llms.txt and embedded in full in llms-full.txt.
• Documentation sweep after #222: vera lsp joins the command lists in README/CLAUDE/AGENTS/SKILL; README's editor-support section, feature list, install notes, and project tree now cover the language server, vera/obligations/, and vera/lsp/; AGENTS.md gains an agent-facing section on the custom proof-delta methods; KNOWN_ISSUES drops the stale "LSP server" limitation row (shipped v0.0.161–v0.0.168) and gains three real ones — the single-file editor model (#724), parameter-only slot go-to-definition (#181), and handler-unaware vera/addEffect propagation (#725); llms.txt indexes LSP_SERVER.md; the compiler README module map's lsp/ line count is corrected (a v0.0.168 update had silently failed); the release-count figures in README and the HISTORY footer now reflect the actual tag count (the v0.0.24.1 hotfix made releases = version + 1, uncounted since then).

v0.0.168

Added

• #222 Phase F3 — vera/addEffect, the multi-site workflow that completes the skill layer: {uri, fn, effect} computes the transitive-caller closure over the Phase B call walker (plain calls only — module-qualified calls never propagate across the file boundary), rewrites every affected effects(...) clause by span (pure → <E>; <A> → <A, E> appending after the original source verbatim; functions already naming the effect are skipped, with identity the base name before type arguments so State<Int> is not added next to State<Bool>), and runs ONE candidate through the proposeEdit pipeline. The response lists rewritten functions in declaration order; a row state that is already satisfied short-circuits to the documented no-op shape without touching the verifier. Propagation is handler-unaware by design — a caller that handles the effect in a handle[E] block is still rewritten; bounding the closure at handlers is noted as a refinement. This closes the #222 LSP arc: the three skill-layer methods (proposeEdit, strengthenContract, addEffect) shipped in v0.0.166–v0.0.168 on the obligation core and proof-delta machinery from v0.0.161–v0.0.165.

v0.0.167

Added

• #222 Phase F2 — vera/strengthenContract, the contract-change workflow with a call-site audit: {uri, fn, kind: requires|ensures, expr} locates the first clause of that kind on the named top-level function, splices the new expression over the clause's span in the canonical document, and runs the candidate through the proposeEdit pipeline. The audit is the proof delta itself — a tightened precondition some caller no longer satisfies surfaces as newly_undischarged call_pre items at the call sites (Phase A keys obligations by call-site span precisely for this) and the gate refuses; a strengthened postcondition the body proves discharges and applies. No force parameter — the dedicated workflow exists to make the audited path the easy one (an agent that wants to push through a breaking change can construct the full text and call vera/proposeEdit with force explicitly). Requests that cannot name a splice target (unknown function, unopened or unparseable document, bad kind) refuse with JSON-RPC InvalidParams at the boundary.

v0.0.166

Added

• #222 Phase F1 — vera/proposeEdit, the first skill-layer workflow: the whole edit → verify → apply sequence as one LSP method, so an agent cannot apply an unverified edit — applying is the final step of verifying. The proposed text runs through the Phase E speculative verify; the gate applies it iff the proof delta has no newly_undischarged obligations and the proposed state has no error diagnostics (force: true overrides both, loudly — the delta still reports the damage). On apply: a workspace/applyEdit request (the client owns the buffer, so the server round-trips the edit rather than silently diverging), the canonical DocumentStore updates, and diagnostics republish — the client's echoed didChange then replays from the warm discharge cache. On refuse, canonical state is untouched, same isolation as vera/speculativeEdit. New vera/lsp/workflows.py with the pure decision function separated from the effectful orchestration; ROADMAP regains a Phase F row while the reopened #222 is in flight.

v0.0.165 — vera/speculativeEdit proof-delta: the LSP server is complete (#222)

Added

• #222 Phase E — vera/speculativeEdit, the one custom LSP method and the reason the obligation core was built first: apply an edit in memory, re-verify on the warm incremental session, and return a proof_delta — newly_discharged / newly_undischarged / timed_out / removed / unchanged, each item carrying the obligation's function, kind, expression, position, and before/after status. An agent proposing an edit learns whether it keeps, breaks, or strengthens the program's proofs before committing it. Speculative runs share the warm session and discharge cache (pre-warming by design) under the same lock, but never touch the canonical per-URI analyses or published diagnostics. Parse/type errors in the speculative state report ok: false with the error count. This completes the #222 plan: Phases A (reified obligations + warm Z3), B (incremental invalidation + discharge cache), C (stdio transport + coordinate layer), D (diagnostics/hover/goto/completion), and E shipped across v0.0.161–v0.0.165; the "No LSP server" row leaves the compiler limitation table and the ROADMAP.

v0.0.164 — LSP language features over the obligation core (#222 Phase D)

Added

• #222 Phase D — vera lsp now serves language features over the obligation core: publishDiagnostics on open/change (parse, type-check, and verification diagnostics, plus a synthesised per-function verification-tier Hint — "Tier 1 — all contracts proven by Z3" / "Tier 3 — N of M obligations fall back to runtime checks" — computed from the obligation stream and suppressed for functions with violated obligations); hover showing the type of the smallest expression span under the cursor; go-to-definition on @T.n jumping to the parameter it names (De Bruijn most-recent-first via slots.slot_table; references binding through let/match return no definition — signature-level scope, with full binding resolution tracked by #181); and typed-hole completion listing the in-scope bindings with their types. All verification is serialised through one warm VerificationSession under a lock. The checker gains opt-in artifact collection (typecheck_with_artifacts: a Span→type side-table recorded by a thin _synth_expr wrapper, and structured HoleSite records factored out of the W001 hole diagnostic) at zero cost to existing callers. Diagnostic gains an optional tier field (surfaced in --json only when set); the verifier's six Tier-3 fallback warnings (E520–E525) now carry tier=3.

v0.0.163 — vera lsp: transport skeleton + coordinate layer (#222 Phase C)

Added

• #222 Phase C — vera lsp serves the Language Server Protocol over stdio: handshake with serverInfo, full-text document sync into an in-memory DocumentStore (the source of truth for open files — features never read disk), and the coordinate-conversion layer in vera/lsp/convert.py where the three coordinate systems meet (Vera Span: 1-based line + 1-based code-point column with exclusive end; SourceLocation: 1-based line but 0-based column; LSP: 0-based line + UTF-16 code units, with astral-plane transcoding and surrogate-pair snapping per the spec). Deliberately featureless — Phase D wires diagnostics/hover/completion onto this transport so the advertised capability surface never promises something unimplemented. The transport dependencies live in a new optional [lsp] extra (pygls>=2.0, lsprotocol; both pure-Python, mirrored into [dev] for CI) so the base install is unchanged; vera lsp without the extra prints an actionable install message.

v0.0.162 — Incremental verification: discharge cache + invalidation (#222 Phase B)

Added

• #222 Phase B — incremental verification: VerificationSession now caches each top-level function's verification output (obligations, diagnostics, summary deltas) under an invalidation key covering everything its verification reads, and replays unchanged functions instead of re-entering Z3. The soundness model (documented in the new vera/obligations/cache.py): a callee contract or signature change invalidates its callers (call sites check preconditions and assume postconditions); a callee body change does not (bodies are never read across the call boundary); span shifts, ADT / type-alias / effect / import / timeout changes invalidate conservatively. Functions whose output contains a solver-timeout obligation are never cached. SessionRunStats (replayed vs verified counts) added for cache observability. Pinned by the corpus-wide differential oracle (replay == re-verify == cold verify() across all 35 examples and every verify/run-level conformance program) plus targeted invalidation-rule tests, including a span-shift test that caught the structural hash being position-blind (Node.span is repr=False) before it shipped.

v0.0.161 — Proof obligations reified + warm Z3 session (#222 Phase A)

Added

• #222 Phase A — proof obligations are now first-class: new vera/obligations/ package with a ProofObligation record (owning function, kind, expression text, source span, stable content_key() digest, discharge outcome with counterexample) and a VerificationSession daemon that re-verifies full programs on one long-lived Z3 solver via the previously-unused SmtContext.reset() warm path. VerifyResult gains an obligations field (default-empty, source-compatible); ContractVerifier gains a shared_smt hook (the cold path is unchanged: fresh context per function). Obligation kinds cover requires / ensures / decreases / @Nat-subtraction sites / call-site preconditions (the latter recorded on violation only in Phase A — successful call-site checks discharge inside the SMT layer and are enumerated in Phase B). Reification is observational: records are created at the existing discharge sites in discharge order, never altering solver state. Behaviour is pinned by a 250-test differential oracle (tests/test_obligations.py): warm session == cold verify() on diagnostics, summary, and the obligation stream — plus warm-twice determinism — across all 35 examples and every verify/run-level conformance program. This is the semantic core the #222 LSP server builds on; Phase B (incremental invalidation + discharge cache) slots in behind the same API.

Fixed

• SmtContext.reset() warm-reuse staleness — reset() (previously dead code) kept _length_fns / _index_fns / _array_element_sorts / _path_conditions across solver resets. get_rank_fn asserts its ForAll rank(x) >= 0 axiom only at dict-miss, so a surviving cache entry after solver.reset() silently skipped re-asserting the axiom and ADT-measure decreases checks would diverge from a fresh context. reset() now clears all four (re-seeding the Int length function) and re-applies the solver timeout. Latent-only before this release — nothing called reset(); the new warm session is its first caller, and the differential oracle now pins the equivalence.

Security

• #712 — SHA-pinned codecov/codecov-action to a commit (e79a696 = v6.0.1) instead of the floating @v6 tag, as targeted supply-chain hardening following the Codecov → Harness acquisition (announced 2026-06-02). An ownership change is the canonical scenario where a major-version tag could be repointed by the new owner and silently flow into CI; pinning to a reviewed commit closes that, while Dependabot continues to propose bumps under review. Coverage is unaffected either way — the 80% gate is the on-runner pytest --cov-fail-under=80 and the upload is fail_ci_if_error: false. Also corrected a stale SECURITY.md cross-reference that attributed action SHA-pinning to #390 (a closed Python dependency-lockfile issue).