-
Notifications
You must be signed in to change notification settings - Fork 20
Issues
is:issue state:open
is:issue state:open
Issue creation is restricted in this repository
Search results
Verifier: a value's postcondition/refinement is not propagated through an ADT field (box then unbox loses the fact)
limitationKnown compilation limitationKnown compilation limitationStatus: Open.#909 In aallan/vera;Harden the four sibling shadow-stack bounds to slot-complete checks (follow-up to #791)
enhancementNew feature or requestNew feature or requestruntime-gcWASM runtime, host bindings, and GCWASM runtime, host bindings, and GCStatus: Open.#860 In aallan/vera;Extend the wasi-p2 target beyond the IO+Random surface (Http via wasi:http outgoing-handler, streaming filesystem, sockets)
codegenCode generation backendCode generation backendenhancementNew feature or requestNew feature or requestlimitationKnown compilation limitationKnown compilation limitationStatus: Open.#853 In aallan/vera;CI: run check_limitations_sync.py --check-states on a schedule to catch closed-issue drift
ciCI/CD and GitHub ActionsCI/CD and GitHub ActionsenhancementNew feature or requestNew feature or requesttoolingIssue around tooling built for the language (e.g. package managers, IDE plug-ins)Issue around tooling built for the language (e.g. package managers, IDE plug-ins)Status: Open.#852 In aallan/vera;Advisory diagnostic for effect-eligible but shape-unfusable async arguments
enhancementNew feature or requestNew feature or requestStatus: Open.#844 In aallan/vera;Extend TestErrorDisplaySync to cover all E001 spec_ref mirrors (AGENTS.md + the build_site.py generator)
documentationImprovements or additions to documentationImprovements or additions to documentationtestingTest suite structure and coverageTest suite structure and coverageStatus: Open.#829 In aallan/vera;Enforce error_code uniqueness — one stable code per diagnostic concept (deterministic registration shipped; semantic + structural enforcement remain)
toolingIssue around tooling built for the language (e.g. package managers, IDE plug-ins)Issue around tooling built for the language (e.g. package managers, IDE plug-ins)Status: Open.#828 In aallan/vera;Diagnostic-fields gate: plumbing-skip keys on function name only — a stray/second Diagnostic in an _error/_warning helper escapes both passes
toolingIssue around tooling built for the language (e.g. package managers, IDE plug-ins)Issue around tooling built for the language (e.g. package managers, IDE plug-ins)Status: Open.#827 In aallan/vera;@Nat → @Int widening: remaining deferred coercion sites (follow-up to #813)
limitationKnown compilation limitationKnown compilation limitationverificationContract verification systemContract verification systemStatus: Open.#820 In aallan/vera;Mutation testing beyond the soundness core: whole-vera/ sweep + full-sweep reliability
enhancementNew feature or requestNew feature or requesttestingTest suite structure and coverageTest suite structure and coverageStatus: Open.#795 In aallan/vera;Feedback-driven mutation-hardening for the deep verifier/smt soundness layers (#387 follow-up)
testingTest suite structure and coverageTest suite structure and coverageverificationContract verification systemContract verification systemStatus: Open.#792 In aallan/vera;Bookmark: GitHits MCP — dependency-reference retrieval for Vera (trial at the next dependency-facing milestone)
bookmarkSaving a link to another projectSaving a link to another projectintegrationIntegration with external tools and languagesIntegration with external tools and languagesStatus: Open.#785 In aallan/vera;