Promote formal verification to tasks; renumber roadmap items#511
Merged
Promote formal verification to tasks; renumber roadmap items#511
Conversation
…ion phase The roadmap documentation has been reorganized to renumber phases following formal verification, expanding the formal verification section from former 9.8 to 10.x with more detailed substeps. This includes separating tooling setup, protocol decisions, verification harnesses, model checks, and proofs into distinct checklist items with updated references and success criteria. Subsequent phases are renumbered to maintain consistency, and related docs references have been updated accordingly. Co-authored-by: devboxerhub[bot] <devboxerhub[bot]@users.noreply.github.com>
Contributor
Reviewer's GuideReorganizes the roadmap’s formal verification work into a dedicated phase with task-style items and success criteria, renumbers downstream roadmap sections accordingly, and updates all in-doc references (including user and client design guides) to align with the new 10.x/11.x numbering scheme. Flow diagram for 10.x formal verification task dependencies in the roadmapflowchart LR
direction LR
subgraph Phase10_Formal_verification[10. Formal verification]
subgraph VWork[10.1 Verification workspace and tooling]
T10_1_1[10.1.1 Root manifest hybrid workspace]
T10_1_2[10.1.2 wireframe-verification crate]
T10_1_3[10.1.3 Kani and Verus pinned tooling]
T10_1_4[10.1.4 Make targets for verification]
T10_1_5[10.1.5 CI jobs for Stateright, Kani, Verus]
T10_1_1 --> T10_1_2
T10_1_1 --> T10_1_3
T10_1_3 --> T10_1_4
T10_1_4 --> T10_1_5
end
subgraph ProtocolDecisions[10.2 Protocol contract decisions]
T10_2_1[10.2.1 Length-prefix width decision]
T10_2_2[10.2.2 total_body_len semantics decision]
T10_2_3[10.2.3 ConnectionActor fairness guarantees]
end
subgraph KaniChecks[10.3 Kani bounded model checks]
T10_3_1[10.3.1 Kani smoke harnesses for frames]
T10_3_2[10.3.2 Kani harnesses for FragmentSeries, Reassembler, MessageSeries]
T10_3_3[10.3.3 Proptest extensions for fragments and traces]
end
subgraph StaterightChecks[10.4 Stateright model checks]
T10_4_1[10.4.1 ConnectionActor model in wireframe-verification]
T10_4_2[10.4.2 Shared checker harness]
T10_4_3[10.4.3 CI-gated BFS model runs]
end
subgraph VerusProofs[10.5 Verus proofs for message assembly]
T10_5_1[10.5.1 Enforce total_body_len contract in runtime]
T10_5_2[10.5.2 Verus proof modules under verus/]
T10_5_3[10.5.3 Document proof trigger discipline and expectations]
end
end
%% Cross-subtask dependencies from roadmap
T10_1_1 --> T10_2_1
T10_1_1 --> T10_2_2
T10_1_1 --> T10_2_3
T10_1_3 --> T10_3_1
T10_2_1 --> T10_3_1
T10_1_3 --> T10_3_2
T10_2_2 --> T10_3_2
T10_3_1 --> T10_3_3
T10_1_2 --> T10_4_1
T10_2_3 --> T10_4_1
T10_4_1 --> T10_4_2
T10_1_5 --> T10_4_3
T10_4_2 --> T10_4_3
T10_2_2 --> T10_5_1
T10_1_3 --> T10_5_2
T10_5_1 --> T10_5_2
T10_5_2 --> T10_5_3
File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
Contributor
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Run ID: 📒 Files selected for processing (1)
Summary by CodeRabbit
WalkthroughSummarise the documentation update: restructure the formal verification roadmap into a multi‑phase plan (phase 10 → sub‑phases 10.1–10.5) with explicit "Requires" links and success criteria, add a formal‑verification footnote, and update cross‑references ( Changes
Estimated code review effort🎯 2 (Simple) | ⏱️ ~10 minutes Poem
🚥 Pre-merge checks | ✅ 3✅ Passed checks (3 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Comment |
![codescene-delta-analysis[bot]](https://avatars.githubusercontent.com/in/53921?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
![sourcery-ai[bot]](https://avatars.githubusercontent.com/in/48477?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Hey - I've left some high level feedback:
- You’ve introduced the
[fv-guide]reference but still have several inline links toformal-verification-methods-in-wireframe.md; consider switching those remaining references to[fv-guide]for consistency and to make future URL changes easier.
Prompt for AI Agents
Please address the comments from this code review:
## Overall Comments
- You’ve introduced the `[fv-guide]` reference but still have several inline links to `formal-verification-methods-in-wireframe.md`; consider switching those remaining references to `[fv-guide]` for consistency and to make future URL changes easier.Help me be more useful! Please click 👍 or 👎 on each comment and I'll use the feedback to improve your reviews.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
The [fv-guide] link definition was using plain Markdown reference-link syntax instead of GFM footnote syntax ([^fv-guide]). Align with the existing [^adr-005], [^adr-006], and [^message-versioning] footnotes already used in the same file. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
leynos
changed the title
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 3
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/roadmap.md`:
- Around line 552-556: Standardize section reference formatting by enclosing the
referenced section titles in quotes to match other occurrences: update the two
references that mention §Is `total_body_len` authoritative or advisory? and
§What Verus should prove in Wireframe so they become §"Is `total_body_len`
authoritative or advisory?" and §"What Verus should prove in Wireframe"
(preserving the inline code `total_body_len`) to match the quoted style used
elsewhere like §"What widths does Wireframe actually support...".
- Around line 457-463: The task entry for "10.1.2. Add
`crates/wireframe-verification`" is missing its prerequisite; update the task
description in the roadmap (the "10.1.2. Add `crates/wireframe-verification`"
bullet) to append "Requires 10.1.1." so it explicitly depends on the workspace
conversion task 10.1.1; ensure the phrasing is consistent with other dependency
notes in the document and retains the existing success criteria text.
- Around line 471-476: Update the description for task 10.1.4 to declare its
prerequisites by adding "Requires 10.1.2 and 10.1.3." so the Makefile targets
(make test-verification, make kani, make verus, etc.) explicitly state they
depend on the verification crate being present (10.1.2) and the formal tools
being installed (10.1.3); modify the task text that currently lists the targets
and success criteria (task identifier 10.1.4) to include this dependency
sentence.
🪄 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: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: e917709d-2440-4c8d-a7fd-fa5c7cf593fb
📒 Files selected for processing (1)
docs/roadmap.md
…ncies 1. Quote section references in 10.5.1 (§"Is `total_body_len`..." and §"What Verus should prove...") to match style elsewhere. 2. Add "Requires 10.1.1." to task 10.1.2 (verification crate needs workspace). 3. Add "Requires 10.1.2 and 10.1.3." to task 10.1.4 (Makefile targets need verification crate and tools installed). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Contributor
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Inline comments:
In `@docs/roadmap.md`:
- Around line 485-503: Rewrite the three checklist items (10.2.1, 10.2.2,
10.2.3) from intention statements into concrete delivered outcomes: for 10.2.1
replace "Decide whether length-prefix widths are limited to..." with an outcome
like "Support length-prefix widths {…} and enforce them in
constructors/conversions/tests; record decision in ADR" and ensure the success
criteria (constructors enforce chosen widths, tests reject others) are included;
for 10.2.2 replace "Decide whether `total_body_len` is authoritative or
advisory..." with an outcome such as "Treat `total_body_len` as
[authoritative|advisory] and enforce/rename it across message assembly code;
record ADR and add tests for conforming/violating inputs" and include the
runtime enforcement and test criteria; for 10.2.3 replace "Document the intended
fairness and priority guarantees for `ConnectionActor`..." with an outcome like
"Publish named fairness and priority guarantees for `ConnectionActor` and encode
them as model properties for Stateright checks" and include the success criteria
(design doc enumerates named properties and model checks reference them). Use
capability-delivery phrasing for each item and keep the existing success
criteria text paired to the new outcome statements.
🪄 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: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 97c25ca4-9a05-4624-bfbf-23131ccab415
📒 Files selected for processing (1)
docs/roadmap.md
Convert tasks 10.2.1, 10.2.2, and 10.2.3 from intention statements
("Decide whether...", "Document the intended...") to capability-delivery
phrasing that describes concrete delivered outcomes:
- 10.2.1: "Support a determined set of length-prefix widths and enforce..."
- 10.2.2: "Treat `total_body_len` as either authoritative or advisory and
enforce..."
- 10.2.3: "Publish named fairness and priority guarantees for
`ConnectionActor` and encode..."
Each task retains its existing success criteria paired with the new outcome
statement, ensuring tasks describe what will be built rather than what will
be decided.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
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.
Summary
Changes
Roadmap and formal verification section
Documentation updates
Notes
Testing
◳ Generated by DevBoxer ◰
ℹ️ Tag @devboxerhub to ask questions and address PR feedback
📎 Task: https://www.devboxer.com/task/afded234-af14-4bf3-ae3e-2243e7c883d1
Summary by Sourcery
Reorganize the roadmap’s formal verification work into a dedicated, task-based phase and renumber downstream roadmap sections accordingly.
Enhancements:
Documentation: