ci: add ubuntu-24.04-arm to the test matrix

[chethanuk]

User description

Pre-flight validation ahead of aallan#702.

Summary

• Adds one ubuntu-24.04-arm × Python 3.12 job to the test matrix via include (platform coverage, not python-version coverage, so it isn't cross-multiplied against all three Python versions).
• Verified no if: condition in the job keys off matrix.os against anything other than the literal 'ubuntu-latest' string, so the new value correctly runs the plain test step and is excluded from the coverage-upload step.
• z3-solver, wasmtime, and lark all resolve prebuilt manylinux_2_38_aarch64 wheels for Python 3.12 today (verified independently, not assumed).

Known gap (out of scope for this PR)

scripts/check_wheel_availability.py's SUPPORTED table has zero Linux aarch64 rows despite README documenting it as supported — the wheel pre-flight gate gives no signal for aarch64 dependency drift. Leaving as a fast-follow rather than folding into this PR, to keep the diff matching this issue's stated scope.

Test plan

• yaml.safe_load parses clean.
• Full pre-commit run --all-files green.
• Watch the new ubuntu-24.04-arm × 3.12 job actually execute and pass in this PR's CI run (not just parse) — existing 12-job matrix must stay green too.

---

CodeAnt-AI Description

Add arm64 CI coverage and raise the wasmtime minimum version

What Changed

• CI now runs one real test job on ubuntu-24.04-arm with Python 3.12, adding Linux arm64 coverage without expanding the whole matrix.
• The wasmtime minimum version is raised to >=46.0.1, keeping installs off a release affected by a known security issue.
• The changelog now records the wasmtime security update.
• The build tool requirement is also bumped to a newer setuptools release.

Impact

✅ Real Linux arm64 test coverage
✅ Safer installs for embedders using wasmtime
✅ Clearer release notes for the security update

💡 Usage Guide

Checking Your Pull Request

Every time you make a pull request, our system automatically looks through it. We check for security issues, mistakes in how you're setting up your infrastructure, and common code problems. We do this to make sure your changes are solid and won't cause any trouble later.

Talking to CodeAnt AI

Got a question or need a hand with something in your pull request? You can easily get in touch with CodeAnt AI right here. Just type the following in a comment on your pull request, and replace "Your question here" with whatever you want to ask:

@codeant-ai ask: Your question here

This lets you have a chat with CodeAnt AI about your pull request, making it easier to understand and improve your code.

Example

@codeant-ai ask: Can you suggest a safer alternative to storing this secret?

Preserve Org Learnings with CodeAnt

You can record team preferences so CodeAnt AI applies them in future reviews. Reply directly to the specific CodeAnt AI suggestion (in the same thread) and replace "Your feedback here" with your input:

@codeant-ai: Your feedback here

This helps CodeAnt AI learn and adapt to your team's coding style and standards.

Example

@codeant-ai: Do not flag unused imports.

Retrigger review

Ask CodeAnt AI to review the PR again, by typing:

@codeant-ai: review

Check Your Repository Health

To analyze the health of your code repository, visit our dashboard at https://app.codeant.ai. This tool helps you identify potential issues and areas for improvement in your codebase, ensuring your repository maintains high standards of code health.

Summary by CodeRabbit

• New Features

  • Added a scheduled check for drift between documented limitation tables and live issue states, with tracking for failures.
  • Expanded Linux ARM coverage in the CI test matrix.
  • Added several new diagrams and updated product docs to better explain workflows, verification, effects, runtime, and WASI support.

• Bug Fixes

  • Improved handling of unknown issue states so limitation checks fail clearly instead of passing silently.
  • Updated tests and coverage figures to reflect the latest behaviour and platform support.

[codeant-ai]

CodeAnt AI is reviewing your PR.

[codeant-ai]

---

Thanks for using CodeAnt! 🎉

We're free for open-source projects. if you're enjoying it, help us grow by sharing.

Share on X ·
Reddit ·
LinkedIn

[coderabbitai]

📝 Walkthrough

Walkthrough

This PR updates Vera to version 0.1.1: adds an advisory ubuntu-24.04-arm CI lane and wheel-availability checks, introduces a scheduled limitations-drift-sync workflow, hardens the sync script's state-check error handling, raises wasmtime/setuptools minimum versions, adds a resolve pipeline stage to documentation, and adds extensive SVG diagrams across specs and READMEs. Several test fixtures and documentation figures were also updated.

Changes

CI Infrastructure and Limitations Sync

Layer / File(s)	Summary
aarch64 CI matrix and wheel coverage .github/workflows/ci.yml, scripts/check_wheel_availability.py, CLAUDE.md, README.md, TESTING.md	Adds an advisory ubuntu-24.04-arm/Python 3.12 matrix entry and manylinux_2_38_aarch64 wheel checks, with docs updated to reflect 13 matrix combinations.
Limitations drift sync workflow and state-check hardening .github/workflows/limitations-sync.yml, scripts/check_limitations_sync.py, tests/test_check_limitations_sync.py	Adds a scheduled/manual workflow that runs a state-check script and files/updates a limitations-drift tracking issue on failure; the script now errors on UNKNOWN issue states, backed by a new subprocess-based test.

Estimated code review effort: 3 (Moderate) | ~25 minutes

Release version bump and dependency updates

Layer / File(s)	Summary
Version bump, dependency floors, and changelog pyproject.toml, vera/__init__.py, CHANGELOG.md	Bumps package version to 0.1.1, raises wasmtime and setuptools minimum versions with updated rationale, and updates changelog entries/compare links.

Documentation and diagram overhaul

Layer / File(s)	Summary
Compiler pipeline resolve stage documentation AGENTS.md, CLAUDE.md, README.md	Documents a new resolve (resolver.py) stage between transform and typecheck.
Diagram asset inventory and design system assets/diagrams/README.md	Adds documentation for diagram embedding conventions, the shared design system, and an SVG inventory.
Specification diagrams spec/02-types.md, spec/06-contracts.md, spec/07-effects.md, spec/08-modules.md, spec/09-standard-library.md, spec/11-compilation.md, spec/12-runtime.md, spec/13-wasi.md	Embeds SVG diagrams illustrating subtyping, verification tiers, effect handling, module resolution, async/server flow, memory layout, GC, and WASI component architecture.
vera/README.md architecture documentation rewrite vera/README.md	Replaces ASCII diagrams with linked SVGs, wraps text versions in <details> blocks, updates module counts, and rewrites the verifier-tier vs codegen relationship description.
Narrative guides, roadmap, and history updates DESIGN.md, DE_BRUIJN.md, FAQ.md, LSP_SERVER.md, CONTRIBUTING.md, TOOLCHAIN.md, README.md, SKILL.md, KNOWN_ISSUES.md, HISTORY.md, ROADMAP.md	Adds diagrams, new effect/limitation entries, stage history updates, and a reworked forward-looking roadmap of stages 19–24 plus horizon arcs.
Testing metrics and generated site content TESTING.md, scripts/build_site.py	Updates coverage figures/matrix counts and revises generated landing-page images, example links, feature wording, and WASI output banner.

Estimated code review effort: 2 (Simple) | ~12 minutes

Compiler test fixture updates

Layer / File(s)	Summary
Codegen and conformance test fixture adjustments tests/test_codegen_data_types.py, tests/test_codegen_gc_alloc.py, tests/test_codegen_monomorphize.py, tests/test_runtime_traps.py, tests/conformance/manifest.json	Widens the GC worklist-overflow fixture to 5000 elements with updated expected sums, removes an obsolete workaround from a monomorphization fixture, updates a rejection-test comment and runtime-traps docstring, and adds a decimal_compare feature to the conformance manifest.

Estimated code review effort: 2 (Simple) | ~15 minutes

Suggested labels: compiler, ci, docs

🚥 Pre-merge checks | ✅ 7 | ❌ 1

❌ Failed checks (1 warning)

Check name	Status	Explanation	Resolution
Docstring Coverage	⚠️ Warning	Docstring coverage is 62.50% which is insufficient. The required threshold is 80.00%.	Write docstrings for the functions missing them to satisfy the coverage threshold.

✅ Passed checks (7 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title clearly identifies the main change: adding ubuntu-24.04-arm to the CI test matrix.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Changelog Covers Public-Surface Changes	✅ Passed	CHANGELOG.md’s Unreleased/0.1.1 entries explicitly cover the spec/docs diagram set, README/ROADMAP/TESTING updates, and the new CI lanes, matching the public-surface changes.
Spec And Implementation Move Together	✅ Passed	No files under vera/ or spec/ changed in this PR diff, so there is no spec/implementation drift to flag.
Diagnostics Carry An Error Code	✅ Passed	No Vera compiler diagnostic definitions changed; the only new error text is in a CI helper script, not the stable E/W diagnostic family.

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch fix/issue-702-ci-arm64-matrix

Warning

Review ran into problems

🔥 Problems

Linked repositories: Public OSS repositories can only analyze public repositories installed in this organization. No linked repositories were analyzed; skipped aallan/vera-bench.

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[codeant-ai]

CodeAnt AI finished reviewing your PR.

[gemini-code-assist]

Code Review

This pull request updates the wasmtime dependency floor to >=46.0.1 in pyproject.toml and uv.lock to address the GHSA-4ch3-9j33-3pmj security vulnerability, with corresponding updates made to CHANGELOG.md. It also bumps the setuptools build-system requirement to >=83.0.0. Feedback on this PR points out that the CI workflow configuration changes (e.g., for adding ubuntu-24.04-arm to the test matrix) appear to be missing from the changes.

Important

The consumer version of Gemini Code Assist on GitHub is being sunset. Starting June 18, 2026, new organization installations will be blocked, and all code review activity will officially cease on July 17, 2026.
For more details on the timeline and next steps, please review the Help Documentation.

[gemini-code-assist]

The PR title and description indicate that this PR adds ubuntu-24.04-arm to the test matrix. However, the actual CI workflow configuration file (e.g., .github/workflows/test.yml) is missing from the changes. Please add the missing workflow file changes to this pull request.

[coderabbitai]

Actionable comments posted: 14

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@DESIGN.md`:
- Around line 31-32: The collections guidance in DESIGN.md uses shortened helper
names that do not match the built-ins; update the references in the Collections
and Standard library descriptions to use the full array helper names. Replace
the generic mentions of `filter`, `fold`, and `slice` with `array_filter`,
`array_fold`, and `array_slice` so the documentation aligns with the actual
function names and symbols used elsewhere.

In `@README.md`:
- Around line 227-233: The test totals in the project status docs are out of
sync, so update the README status blurb to match the latest count reported in
TESTING.md and any related doc-count gate text. Check the “active development”
summary in README.md and the corresponding overview/status entries in ROADMAP.md
and TESTING.md so the same total is used everywhere, especially after the new
test added in this PR. Refer to the README status paragraph and the doc-count
summary sections in TESTING.md and ROADMAP.md when making the correction.

In `@scripts/build_site.py`:
- Around line 416-417: The new loop diagram reference is not aligned with the
diagram inventory, because `loop-web.svg` is used in the site content but not
listed in `assets/diagrams/README.md`. Update `scripts/build_site.py` to either
point to an already-documented diagram name or add `loop-web.svg` to the
inventory so the generated site stays single-sourced and consistent with the
documented assets.
- Around line 555-560: Update the generated docs text in the site builder to
match the language surface: replace the non-canonical “Exceptions” effect name
with “Exn<E>” in the relevant content emitted by the docs generation logic, and
soften the `Inference` description so `Inference.complete` is described only as
typed and contract-verifiable without claiming it is fully mockable or broadly
supported by user-defined handlers. Locate the affected strings in the site
generation path around the bullet list and any mirrored copy elsewhere, and keep
both mentions consistent.

In `@scripts/check_limitations_sync.py`:
- Around line 311-320: The issue is that check_issue_states emits one nearly
identical UNKNOWN error per issue when gh is unavailable, creating noisy
duplicate output. Update check_issue_states in scripts/check_limitations_sync.py
to detect the “all issues are UNKNOWN because gh is missing/unauthenticated”
case once and append a single aggregate error message instead of per-issue
lines. Keep the existing UNKNOWN handling for mixed cases, and adjust
test_unknown_state_is_an_error so it matches the new aggregate message.

In `@spec/02-types.md`:
- Around line 318-319: The diagram embed in spec/02-types.md is missing the
required collapsed text fallback. Update the markdown near the subtyping lattice
image so it follows the documented diagram embed convention by adding the
matching details/summary text version block alongside the existing SVG
reference, using the same wording and structure as other embeds in this spec.

In `@spec/06-contracts.md`:
- Around line 373-374: The figure embed in the contracts spec is missing its
required text fallback. Update the documentation around the existing diagram
reference so it includes the matching collapsed <details><summary>Text
version…</summary> block alongside the current image embed, keeping the fallback
text aligned with the Three-tier verification diagram content and consistent
with the pattern used for other embeds.

In `@spec/07-effects.md`:
- Around line 179-180: Add collapsed text fallbacks for both diagram embeds in
the effects spec: the handler-dispatch figure and the effect-subtyping figure
currently only include the SVG, so insert matching <details><summary>Text
version…</summary> blocks beside each image as required by the diagram embed
convention. Update the nearby figure markup in the same section so each visual
embed has an equivalent text description, using the existing figure labels and
surrounding prose to keep the fallback aligned with the handler-dispatch and
effect-subtyping content.

In `@spec/08-modules.md`:
- Around line 209-210: The module-resolution diagram currently includes only the
SVG embed, but it also needs the matching collapsed text fallback to stay
consistent with the other diagram embeds. Update the markdown in the spec
section where this image is referenced so it includes the corresponding
<details><summary>Text version…</summary> block alongside the existing diagram,
matching the pattern used for other SVG inserts and keeping the fallback text
next to the diagram reference.

In `@spec/09-standard-library.md`:
- Around line 517-518: Add the missing collapsed text fallbacks for the two
diagram embeds in the standard library spec. The async figure currently only
inserts the SVG, so pair it with a matching details/summary text version block
that describes the async(e), commutative effect-row, host worker thread, and
W002 eager-evaluation behavior; do the same for the vera serve figure. Keep the
fallback immediately beside each SVG embed to follow the diagram-set convention
and make both figures accessible without relying on the image.

In `@spec/11-compilation.md`:
- Around line 392-393: The closure diagram figure is missing its required
collapsed text fallback. In the section containing the `closure-layout.svg`
image, add the matching `<details><summary>Text version…</summary>` block
immediately alongside the SVG so it follows the diagram-set convention and
provides the alternate text version for the same closure-layout content.

In `@spec/12-runtime.md`:
- Around line 498-499: Add collapsed text fallbacks next to both SVG embeds in
the runtime spec, since the diagram inserts currently only reference the image
and miss the required readable alternative. Update the GC-cycle and
browser-runtime figure sections in the same style as other embeds, using
matching <details><summary>Text version…</summary> blocks so they can be located
by the existing diagram references and the surrounding figure content.

In `@TOOLCHAIN.md`:
- Around line 20-31: The toolchain diagram and text version currently place test
under the code-generation branch, but `vera test` belongs on the execution path
alongside `run` and `serve`. Update the diagram source and the text block in the
toolchain docs so the branch boundary after `compile` flows into execution, and
move `test` to that execution branch while keeping `compile` as the
code-generation step. Use the existing `toolchain.svg`/text version content as
the target to keep both representations aligned with the command behavior.

In `@vera/README.md`:
- Line 725: Update the test-suite count in README.md so it matches ROADMAP.md;
the current “6,821 tests” value is stale and should be changed to the new suite
size reported by the roadmap. Locate the testing overview text in the README and
keep the surrounding description of the pytest suite, conformance suite, and
example programs unchanged while correcting only the numeric count.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro

Run ID: c83e804d-2227-4fe0-bf57-5f28b9df09ee

📥 Commits

Reviewing files that changed from the base of the PR and between 5787fa4 and 758b276.

⛔ Files ignored due to path filters (41)

• assets/diagrams/architecture.svg is excluded by !**/*.svg
• assets/diagrams/async-model.svg is excluded by !**/*.svg
• assets/diagrams/browser-bindings.svg is excluded by !**/*.svg
• assets/diagrams/checker-passes.svg is excluded by !**/*.svg
• assets/diagrams/ci-gates.svg is excluded by !**/*.svg
• assets/diagrams/closure-layout.svg is excluded by !**/*.svg
• assets/diagrams/contract-testing.svg is excluded by !**/*.svg
• assets/diagrams/diagnostic-card.svg is excluded by !**/*.svg
• assets/diagrams/effect-handlers.svg is excluded by !**/*.svg
• assets/diagrams/effect-row-lattice.svg is excluded by !**/*.svg
• assets/diagrams/faq-layers.svg is excluded by !**/*.svg
• assets/diagrams/gc-cycle.svg is excluded by !**/*.svg
• assets/diagrams/history-growth.svg is excluded by !**/*.svg
• assets/diagrams/host-families.svg is excluded by !**/*.svg
• assets/diagrams/httpserver-lifecycle.svg is excluded by !**/*.svg
• assets/diagrams/language-comparison.svg is excluded by !**/*.svg
• assets/diagrams/lsp-session.svg is excluded by !**/*.svg
• assets/diagrams/memory-layout.svg is excluded by !**/*.svg
• assets/diagrams/module-resolution.svg is excluded by !**/*.svg
• assets/diagrams/pipeline.svg is excluded by !**/*.svg
• assets/diagrams/server-world.svg is excluded by !**/*.svg
• assets/diagrams/slot-evolution.svg is excluded by !**/*.svg
• assets/diagrams/slot-numbering.svg is excluded by !**/*.svg
• assets/diagrams/slot-scopes.svg is excluded by !**/*.svg
• assets/diagrams/subtyping-lattice.svg is excluded by !**/*.svg
• assets/diagrams/testing-layers.svg is excluded by !**/*.svg
• assets/diagrams/tiers.svg is excluded by !**/*.svg
• assets/diagrams/toolchain.svg is excluded by !**/*.svg
• assets/diagrams/wasi-arena.svg is excluded by !**/*.svg
• assets/diagrams/wasi-component.svg is excluded by !**/*.svg
• assets/diagrams/wasmtime-embedding.svg is excluded by !**/*.svg
• assets/diagrams/workflow.svg is excluded by !**/*.svg
• assets/diagrams/z3-refutation.svg is excluded by !**/*.svg
• docs/SKILL.md is excluded by !docs/**
• docs/index.html is excluded by !docs/**
• docs/index.md is excluded by !docs/**
• docs/llms-full.txt is excluded by !docs/**
• docs/llms.txt is excluded by !docs/**
• docs/loop-web.svg is excluded by !**/*.svg, !docs/**
• tests/conformance/ch09_decimal.vera is excluded by !**/*.vera
• uv.lock is excluded by !**/*.lock, !uv.lock

📒 Files selected for processing (38)

• .github/workflows/ci.yml
• .github/workflows/limitations-sync.yml
• AGENTS.md
• CHANGELOG.md
• CLAUDE.md
• CONTRIBUTING.md
• DESIGN.md
• DE_BRUIJN.md
• FAQ.md
• HISTORY.md
• KNOWN_ISSUES.md
• LSP_SERVER.md
• README.md
• ROADMAP.md
• SKILL.md
• TESTING.md
• TOOLCHAIN.md
• assets/diagrams/README.md
• pyproject.toml
• scripts/build_site.py
• scripts/check_limitations_sync.py
• scripts/check_wheel_availability.py
• spec/02-types.md
• spec/06-contracts.md
• spec/07-effects.md
• spec/08-modules.md
• spec/09-standard-library.md
• spec/11-compilation.md
• spec/12-runtime.md
• spec/13-wasi.md
• tests/conformance/manifest.json
• tests/test_check_limitations_sync.py
• tests/test_codegen_data_types.py
• tests/test_codegen_gc_alloc.py
• tests/test_codegen_monomorphize.py
• tests/test_runtime_traps.py
• vera/README.md
• vera/__init__.py

[coderabbitai]

📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

set -euo pipefail
printf '\n== DESIGN.md excerpt ==\n'
cat -n DESIGN.md | sed -n '20,40p'
printf '\n== Array helper names in docs/code ==\n'
rg -n "array_(filter|fold|slice|map|mapi|any|all|find|sort_by)|filter` / `fold` / `slice`|no loops" -S README.md SKILL.md AGENTS.md DESIGN.md vera tests examples spec | sed -n '1,200p'
printf '\n== Random effect/runtime references ==\n'
rg -n "Random\.random_(int|float|bool)|Math\.random|random_int|random_float|random_bool|random" -S vera tests examples README.md SKILL.md AGENTS.md DESIGN.md | sed -n '1,240p'

Repository: chethanuk/vera

Length of output: 3867

---

🏁 Script executed:

set -euo pipefail

printf '\n== DESIGN.md array row ==\n'
cat -n DESIGN.md | sed -n '29,32p'

printf '\n== Canonical array helper names elsewhere ==\n'
rg -n 'array_(filter|fold|slice|map|mapi|reverse|find|any|all|flatten|sort_by)|array_length|array_append|array_concat' README.md SKILL.md AGENTS.md vera tests examples spec DESIGN.md | sed -n '1,240p'

Repository: chethanuk/vera

Length of output: 25854

---

Use the full array helper names in DESIGN.md:31
filter / fold / slice should be array_filter / array_fold / array_slice here, to match the actual built-ins and avoid pointing readers at non-existent functions.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@DESIGN.md` around lines 31 - 32, The collections guidance in DESIGN.md uses
shortened helper names that do not match the built-ins; update the references in
the Collections and Standard library descriptions to use the full array helper
names. Replace the generic mentions of `filter`, `fold`, and `slice` with
`array_filter`, `array_fold`, and `array_slice` so the documentation aligns with
the actual function names and symbols used elsewhere.

Source: Path instructions

[coderabbitai]

🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win

Test count drifted from TESTING.md.

This hunk states "6,821 tests", but TESTING.md's own Overview row (also updated in this PR) reports 6,822 (6,733 passed + 26 stress, 63 skipped = 6,822). One of these two is stale — most likely this line, since TESTING.md's per-file row for test_check_limitations_sync.py was bumped to 6 tests/107 lines to reflect the new TestCheckStatesFailsLoud test added in this same PR.

📝 Suggested fix

-Vera is in **active development** at v0.1.1, with **no known bugs**: 1,900+ commits, 199 releases, 6,821 tests, 91% code coverage, 143 conformance programs, 37 examples, and a 14-chapter specification.
+Vera is in **active development** at v0.1.1, with **no known bugs**: 1,900+ commits, 199 releases, 6,822 tests, 91% code coverage, 143 conformance programs, 37 examples, and a 14-chapter specification.

Worth double-checking ROADMAP.md's "Where we are" line too, since the same doc-count gate covers it.

As per coding guidelines, "any PR that adds tests will trip scripts/check_doc_counts.py if it doesn't also update the test counts in TESTING.md (per-file rows + overall total), ROADMAP.md (the "Where we are" line), and README.md (project-status line)." As per path instructions, "Review Markdown files for factual accuracy against the codebase, broken links, and outdated information."

📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change

	Vera is in **active development** at v0.1.1, with **no known bugs**: 1,900+ commits, 199 releases, 6,821 tests, 91% code coverage, 143 conformance programs, 37 examples, and a 14-chapter specification. 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/).
	**Key features delivered:** [typed De Bruijn indices](DE_BRUIJN.md) (`@T.n`), mandatory contracts, algebraic effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, Random), refinement types, constrained generics (Eq, Ord, Hash, Show), algebraic data types, pattern matching, modules, 164 built-in functions (strings, arrays, maps, sets, decimals, math, JSON, HTML, Markdown, regex, base64, URL), contract-driven testing, canonical formatter, browser runtime, three-tier verification (Z3 static, guided, runtime fallback), a [language server](LSP_SERVER.md) with warm incremental verification and agent-facing proof-delta methods, and contract-verified HTTP handlers served natively (`vera serve`) or as wasi:http components for stock `wasmtime serve` (`--target wasi-p2 --world server`).
	**Key features delivered:** [typed De Bruijn indices](DE_BRUIJN.md) (`@T.n`), mandatory contracts, algebraic effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, Random, Diverge), refinement types, constrained generics (Eq, Ord, Hash, Show), algebraic data types, pattern matching, modules, 164 built-in functions (strings, arrays, maps, sets, decimals, math, JSON, HTML, Markdown, regex, base64, URL), contract-driven testing, canonical formatter, browser runtime, three-tier verification design (Z3 static and runtime fallback shipped; the Z3-guided tier is specified, not yet implemented), a [language server](LSP_SERVER.md) with warm incremental verification and agent-facing proof-delta methods, and contract-verified HTTP handlers served natively (`vera serve`) or as wasi:http components for stock `wasmtime serve` (`--target wasi-p2 --world server`).
	**What's next:** the path from "working language" to "the language agents actually use" — see **[ROADMAP.md](ROADMAP.md)** for the four strategic milestones. The flagship goal is a verified MCP tool server where contracts guarantee tool schemas at compile time. **[VeraBench](https://github.com/aallan/vera-bench)** — a 50-problem benchmark across 5 difficulty tiers — now covers 6 models across 3 providers (v0.0.7). The headline result: Kimi K2.5 achieves 100% run_correct on Vera, beating both Python (86%) and TypeScript (91%). Three models beat TypeScript on Vera; the flagship tier averages 93% Vera vs 93% Python — essentially parity. These are single-run results with high variance — see the [full report](https://github.com/aallan/vera-bench) for details.
	Vera is in **active development** at v0.1.1, with **no known bugs**: 1,900+ commits, 199 releases, 6,822 tests, 91% code coverage, 143 conformance programs, 37 examples, and a 14-chapter specification. 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/).
	**Key features delivered:** [typed De Bruijn indices](DE_BRUIJN.md) (`@T.n`), mandatory contracts, algebraic effects (IO, Http, HttpServer, State, Exceptions, Async, Inference, Random, Diverge), refinement types, constrained generics (Eq, Ord, Hash, Show), algebraic data types, pattern matching, modules, 164 built-in functions (strings, arrays, maps, sets, decimals, math, JSON, HTML, Markdown, regex, base64, URL), contract-driven testing, canonical formatter, browser runtime, three-tier verification design (Z3 static and runtime fallback shipped; the Z3-guided tier is specified, not yet implemented), a [language server](LSP_SERVER.md) with warm incremental verification and agent-facing proof-delta methods, and contract-verified HTTP handlers served natively (`vera serve`) or as wasi:http components for stock `wasmtime serve` (`--target wasi-p2 --world server`).
	**What's next:** the path from "working language" to "the language agents actually use" — see **[ROADMAP.md](ROADMAP.md)** for the four strategic milestones. The flagship goal is a verified MCP tool server where contracts guarantee tool schemas at compile time. **[VeraBench](https://github.com/aallan/vera-bench)** — a 50-problem benchmark across 5 difficulty tiers — now covers 6 models across 3 providers (v0.0.7). The headline result: Kimi K2.5 achieves 100% run_correct on Vera, beating both Python (86%) and TypeScript (91%). Three models beat TypeScript on Vera; the flagship tier averages 93% Vera vs 93% Python — essentially parity. These are single-run results with high variance — see the [full report](https://github.com/aallan/vera-bench) for details.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@README.md` around lines 227 - 233, The test totals in the project status docs
are out of sync, so update the README status blurb to match the latest count
reported in TESTING.md and any related doc-count gate text. Check the “active
development” summary in README.md and the corresponding overview/status entries
in ROADMAP.md and TESTING.md so the same total is used everywhere, especially
after the new test added in this PR. Refer to the README status paragraph and
the doc-count summary sections in TESTING.md and ROADMAP.md when making the
correction.

Sources: Coding guidelines, Path instructions

[coderabbitai]

📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

Keep the diagram inventory single-sourced.

This introduces loop-web.svg, but assets/diagrams/README.md does not list that SVG yet. Either add the asset there or reuse the documented diagram name so the site build stays aligned with the inventory.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@scripts/build_site.py` around lines 416 - 417, The new loop diagram reference
is not aligned with the diagram inventory, because `loop-web.svg` is used in the
site content but not listed in `assets/diagrams/README.md`. Update
`scripts/build_site.py` to either point to an already-documented diagram name or
add `loop-web.svg` to the inventory so the generated site stays single-sourced
and consistent with the documented assets.

[coderabbitai]

📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

Use the canonical effect name and do not overstate Inference.

The generated docs still say Exceptions, but the language docs use Exn<E>. They also call Inference mockable, which is broader than the current implementation because user-defined handlers are still unsupported. Please tighten both occurrences so the site matches the language surface.

Also applies to: 647-647

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@scripts/build_site.py` around lines 555 - 560, Update the generated docs text
in the site builder to match the language surface: replace the non-canonical
“Exceptions” effect name with “Exn<E>” in the relevant content emitted by the
docs generation logic, and soften the `Inference` description so
`Inference.complete` is described only as typed and contract-verifiable without
claiming it is fully mockable or broadly supported by user-defined handlers.
Locate the affected strings in the site generation path around the bullet list
and any mirrored copy elsewhere, and keep both mentions consistent.

[coderabbitai]

📐 Maintainability & Code Quality | 🔵 Trivial | ⚡ Quick win

Correct fix, but consider a single aggregate message when gh is entirely unavailable.

The UNKNOWN branch is correct and matches the new test's expectation. However, check_issue_states is called against all_issues (potentially several dozen tracked numbers across five doc tiers) — if gh itself is missing/unauthenticated, every single one degrades to UNKNOWN and this loop emits one near-identical error line per issue, which will flood the scheduled workflow's tracking-issue body with repetitive noise for what is really one root cause (tool unavailable).

♻️ Optional: detect the "all unknown" case once

     if do_check_states:
         all_issues = (
             readme_issues
             | vera_readme_open
             | all_spec_issues
             | skill_issues
             | lsp_issues
         )
         if all_issues:
             states = check_issue_states(all_issues)
+            if all(v == "UNKNOWN" for v in states.values()):
+                errors.append(
+                    "gh CLI state check failed for all "
+                    f"{len(all_issues)} tracked issues (missing/auth/"
+                    "timeout); --check-states cannot verify the limitation "
+                    "tables"
+                )
             for num in sorted(all_issues):
                 state = states.get(num, "UNKNOWN")
                 if state == "CLOSED":
                     ...
-                elif state == "UNKNOWN":
-                    errors.append(
-                        f"Issue #{num} state could not be determined "
-                        "(gh CLI missing, auth failure, or timeout); "
-                        "--check-states cannot verify the limitation tables"
-                    )
+                elif state == "UNKNOWN" and not all(
+                    v == "UNKNOWN" for v in states.values()
+                ):
+                    errors.append(
+                        f"Issue #{num} state could not be determined "
+                        "(gh CLI missing, auth failure, or timeout); "
+                        "--check-states cannot verify the limitation tables"
+                    )

Note: this would require updating test_unknown_state_is_an_error to still match the new aggregate message.

📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change

	elif state == "UNKNOWN":
	# A state that cannot be determined (gh CLI missing,
	# auth failure, rate limit, timeout) must be loud: a
	# silent pass here would leave the scheduled #852
	# workflow green while checking nothing.
	errors.append(
	f"Issue #{num} state could not be determined "
	"(gh CLI missing, auth failure, or timeout); "
	"--check-states cannot verify the limitation tables"
	)
	if all_issues:
	states = check_issue_states(all_issues)
	if all(v == "UNKNOWN" for v in states.values()):
	errors.append(
	"gh CLI state check failed for all "
	f"{len(all_issues)} tracked issues (missing/auth/"
	"timeout); --check-states cannot verify the limitation "
	"tables"
	)
	for num in sorted(all_issues):
	state = states.get(num, "UNKNOWN")
	if state == "UNKNOWN" and not all(
	v == "UNKNOWN" for v in states.values()
	):
	# A state that cannot be determined (gh CLI missing,
	# auth failure, rate limit, timeout) must be loud: a
	# silent pass here would leave the scheduled `#852`
	# workflow green while checking nothing.
	errors.append(
	f"Issue #{num} state could not be determined "
	"(gh CLI missing, auth failure, or timeout); "
	"--check-states cannot verify the limitation tables"
	)

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@scripts/check_limitations_sync.py` around lines 311 - 320, The issue is that
check_issue_states emits one nearly identical UNKNOWN error per issue when gh is
unavailable, creating noisy duplicate output. Update check_issue_states in
scripts/check_limitations_sync.py to detect the “all issues are UNKNOWN because
gh is missing/unauthenticated” case once and append a single aggregate error
message instead of per-issue lines. Keep the existing UNKNOWN handling for mixed
cases, and adjust test_unknown_state_is_an_error so it matches the new aggregate
message.

[coderabbitai]

📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

Add text fallbacks for both figures.

Both inserts only add the SVG. The diagram-set convention requires a collapsed text version beside each embed, so please add the matching <details><summary>Text version…</summary> blocks for the async and vera serve figures.

Also applies to: 602-603

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/09-standard-library.md` around lines 517 - 518, Add the missing
collapsed text fallbacks for the two diagram embeds in the standard library
spec. The async figure currently only inserts the SVG, so pair it with a
matching details/summary text version block that describes the async(e),
commutative effect-row, host worker thread, and W002 eager-evaluation behavior;
do the same for the vera serve figure. Keep the fallback immediately beside each
SVG embed to follow the diagram-set convention and make both figures accessible
without relying on the image.

Source: Path instructions

[coderabbitai]

📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

Add the text fallback for the closure diagram.

The SVG is in place, but this figure still needs the collapsed text version that the diagram-set convention requires. Please add the matching <details><summary>Text version…</summary> block here as well.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/11-compilation.md` around lines 392 - 393, The closure diagram figure is
missing its required collapsed text fallback. In the section containing the
`closure-layout.svg` image, add the matching `<details><summary>Text
version…</summary>` block immediately alongside the SVG so it follows the
diagram-set convention and provides the alternate text version for the same
closure-layout content.

Source: Path instructions

[coderabbitai]

📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

Add text fallbacks for both figures.

Both inserts only add the SVG. assets/diagrams/README.md requires a collapsed text version beside each embed, so please add the matching <details><summary>Text version…</summary> blocks for the GC-cycle and browser-runtime figures.

Also applies to: 607-608

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@spec/12-runtime.md` around lines 498 - 499, Add collapsed text fallbacks next
to both SVG embeds in the runtime spec, since the diagram inserts currently only
reference the image and miss the required readable alternative. Update the
GC-cycle and browser-runtime figure sections in the same style as other embeds,
using matching <details><summary>Text version…</summary> blocks so they can be
located by the existing diagram references and the surrounding figure content.

Source: Path instructions

[coderabbitai]

🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win

Show vera test on the execution branch.

The diagram/text version makes vera test look like a code-generation-only gate, but it compiles and then executes the generated WASM to run contract-driven tests. Redraw that branch so the stage boundary matches the command behaviour.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@TOOLCHAIN.md` around lines 20 - 31, The toolchain diagram and text version
currently place test under the code-generation branch, but `vera test` belongs
on the execution path alongside `run` and `serve`. Update the diagram source and
the text block in the toolchain docs so the branch boundary after `compile`
flows into execution, and move `test` to that execution branch while keeping
`compile` as the code-generation step. Use the existing `toolchain.svg`/text
version content as the target to keep both representations aligned with the
command behavior.

[coderabbitai]

📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

Sync the test-suite count with the roadmap.

This still says 6,821 tests, but ROADMAP.md now reports 6,822. Please update the count so the docs do not disagree about the suite size.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@vera/README.md` at line 725, Update the test-suite count in README.md so it
matches ROADMAP.md; the current “6,821 tests” value is stale and should be
changed to the new suite size reported by the roadmap. Locate the testing
overview text in the README and keep the surrounding description of the pytest
suite, conformance suite, and example programs unchanged while correcting only
the numeric count.