Research sweep + Roadmap 3.0 (release plan: v2.6 → v3.0)#75
Merged
Conversation
… release plan Research the open scry requirements/gaps, what commercial tools have that we'd want, and old+new academic research that could benefit us — captured in rivet (research schema) and turned into a next-release plan using rivet's new release-planning axis (the `release:` field, rivet >= 0.21). artifacts/research-2.yaml (NEW): - academic-reference AC-012..024 — classic numeric domains scry lacks (polyhedra, Karr, pentagons, array segmentation, gauge), precision (trace partitioning), termination (segmented ranking functions), cost bounds (SPEED), verified- analyzer methodology (Verasco), incremental AI (demanded summarization), and the float/recent frontier (Miné FP octagon, DeepPoly, hybrid Wasm call graph). - competitive-analysis CA-001..011 — the sound-analyzer bar (Astrée, aiT/Stack- Analyzer, Polyspace, Frama-C/Eva, TrustInSoft), the Wasm peers (VeriWasm, Wasmati, symbolic exec, Component-Model green field), CodeQL/Semgrep UX, and the DO-330/ISO-26262 qualification ecosystem. - technology-evaluation TE-011 (AI-agent gap detection: structured-primary, viz-secondary — agents under-read charts/SVG; emit gaps as data, not silence) + TE-012 (Apron/ELINA). market-finding MF-006 (trap detection is the bar's defining capability scry lacks) + MF-007 (no sound Component-Model handle-state analyzer — uncontested green field). artifacts/roadmap-3.0.yaml (NEW) — release plan: - New requirements REQ-014 (trap classification), REQ-015 (IEEE-754 float), REQ-016 (surface relational invariants), REQ-017 (machine-readable gap report). - v2.6.0 "Make the analysis observable": FEAT-040 gap report, FEAT-041 surface octagon relations, FEAT-042 threshold widening, FEAT-043 indirect-call stack weighting. - v2.7.0 "Prove safety": FEAT-044 pentagons, FEAT-045 div/overflow traps, FEAT-046 OOB-memory traps (the Astrée/Polyspace headline capability). - v3.0.0 "Qualifiable + differentiated": FEAT-047 float domain, FEAT-048 WasmCert-Coq wrap-aware soundness (the differentiator) + fix the false Verus join proof, FEAT-049 Component-Model handle-state (the moat), FEAT-050 tool-qualification dossier. - Backlog FEAT-051..058 (Karr, ranking-function termination, incremental summaries, WIT surfacing, counterexamples, sound queryable CPG, polyhedra, array segmentation), researched and traced, not yet release-scoped. - research→requirement→feature traceability wired (references-paper / addresses-finding / evaluates-tech). Track with `rivet release status <ver>`. Also: back-filled `release:` tags on shipped v2.1.0–v2.5.0 features (FEAT-034..039) so the release axis is accurate; bumped the release.yml compliance action's rivet to v0.22.0 so it understands the `release:` field. rivet validate PASS (warnings are advisory prose-mentions + future-REQ-not-yet-verified). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #75 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Researches scry's open requirements/gaps, what commercial tools have that we'd want, and old+new academic research that could benefit us — captured in rivet (research schema) and turned into a next-release plan using rivet's new release-planning axis (
release:field +rivet release status).Research captured (
artifacts/research-2.yaml)Release plan (
artifacts/roadmap-3.0.yaml)New requirements REQ-014 (trap classification), REQ-015 (IEEE-754 float), REQ-016 (surface relational invariants), REQ-017 (machine-readable gap report).
Backlog FEAT-051–058 (Karr, ranking-function termination, incremental summaries, WIT surfacing, counterexamples, sound queryable CPG, polyhedra, array segmentation) — researched, traced, not yet release-scoped.
Track with
rivet release status v2.6.0(etc.). research→requirement→feature traceability wired viareferences-paper/addresses-finding/evaluates-tech.Also: back-filled
release:tags on shipped v2.1.0–v2.5.0 features so the release axis is accurate; bumped the release.yml compliance action's rivet to v0.22.0 for therelease:field.rivet validatePASS (warnings are advisory prose-mentions + future-REQ-not-yet-verified).🤖 Generated with Claude Code