Conversation
Add `docs/formal-verification-methods-in-wireframe.md` as the formal verification strategy guide for Wireframe. Sweep the document for style-guide conformance by removing personal pronouns, expanding acronyms on first use, normalizing British English, and converting references to numbered GFM footnotes in appearance order. Update `docs/contents.md` and add roadmap work item `9.8` so the workspace, Kani, Stateright, Verus, and CI follow-up tasks are tracked explicitly.
Contributor
Reviewer's GuideAdds a new formal verification roadmap item and comprehensive design document describing how to integrate Kani, Stateright, and Verus into the Wireframe project, wires that document into the docs contents, and leaves code behaviour unchanged. Flow diagram for formal verification workflow in development and CIflowchart TD
Dev[Developer_edits_wireframe_code] --> DecideFormal[Decide_whether_change_affects_formal_targets]
DecideFormal -->|No| RunStdTests[Run_standard_make_test_flow]
DecideFormal -->|Yes| RunFormalLocally[Run_local_formal_targets]
subgraph Local_formal_workflow
RunFormalLocally --> L1[make_test_verification]
RunFormalLocally --> L2[make_kani]
RunFormalLocally --> L3[make_verus]
L1 --> FixModel[Refine_connection_actor_model_or_properties]
L2 --> FixKaniHarness[Adjust_Kani_harness_bounds_or_assumptions]
L3 --> FixVerusProof[Update_Verus_specs_or_triggers]
end
RunStdTests --> OpenPR[Open_pull_request]
FixModel --> OpenPR
FixKaniHarness --> OpenPR
FixVerusProof --> OpenPR
subgraph CI_PR_pipeline
OpenPR --> CIbuild[CI_job_build_test]
OpenPR --> CIKani[CI_job_kani_smoke]
OpenPR --> CIStateright[CI_job_stateright_models]
OpenPR --> CIVerus[CI_job_verus_proofs]
CIbuild --> PRStatus[PR_status_checks]
CIKani --> PRStatus
CIStateright --> PRStatus
CIVerus --> PRStatus
end
PRStatus -->|All_pass| Merge[Merge_change]
PRStatus -->|Any_fail| Investigate[Investigate_formal_or_test_failure]
Investigate --> RunFormalLocally
subgraph Nightly_pipeline
NightlyTrigger[Scheduled_or_manual_trigger] --> NightlyFormal[make_formal_nightly]
NightlyFormal --> N1[Deeper_Stateright_BFS_or_DFS]
NightlyFormal --> N2[make_kani_full]
NightlyFormal --> N3[Full_Verus_proof_suite]
end
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 pull request: add formal verification planning and documentation (Kani, Stateright, Verus), extend the roadmap with formal verification milestones, and add a .gitignore rule to exclude Windows Changes
Estimated code review effort🎯 2 (Simple) | ⏱️ ~15 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:
- In the example
[workspace]configuration you reference awireframe_testingmember that doesn’t appear elsewhere in the doc or tree; consider either explaining what that crate is or removing it from the snippet to avoid confusion when people copy-paste it. - The new formal-verification guide hardcodes many GitHub
main-branch URLs to files already in this repo; you may want to switch those to relative links so they keep working if files move or the default branch changes.
Prompt for AI Agents
Please address the comments from this code review:
## Overall Comments
- In the example `[workspace]` configuration you reference a `wireframe_testing` member that doesn’t appear elsewhere in the doc or tree; consider either explaining what that crate is or removing it from the snippet to avoid confusion when people copy-paste it.
- The new formal-verification guide hardcodes many GitHub `main`-branch URLs to files already in this repo; you may want to switch those to relative links so they keep working if files move or the default branch changes.Help me be more useful! Please click 👍 or 👎 on each comment and I'll use the feedback to improve your reviews.
Remove the unexplained `wireframe_testing` workspace member from the example workspace snippet so copy-pasted configuration stays aligned with the surrounding guidance. Replace hardcoded GitHub `main` links for Wireframe-owned files with repo-relative links so the references remain valid if files move or the default branch changes.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
Contributor
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 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/formal-verification-methods-in-wireframe.md`:
- Around line 572-573: Replace the second-person phrase "depending on the exact
contract you choose" in the safety-property bullet with project-neutral wording
(e.g., "depending on the exact contract chosen" or "depending on the specific
contract selected") so the documentation avoids 2nd-person phrasing; update the
safety-property bullet text where that exact phrase appears to the neutral
alternative.
In `@docs/roadmap.md`:
- Around line 446-492: Update each 9.8 checklist item so it cites the exact
section in formal-verification-methods-in-wireframe.md that defines the design
scope: for headings "9.8.1. Establish the formal verification workspace...",
"9.8.2. Resolve the protocol contracts...", "9.8.3. Add bounded Kani checks...",
"9.8.4. Add Stateright model checks...", and "9.8.5. Add Verus proofs..." add a
parenthetical/link like “(See formal-verification-methods-in-wireframe.md §X.Y)”
pointing to the corresponding section; ensure the section numbers map to the
correct design subsections and update the checklist lines (e.g., the sub-bullets
under each 9.8.* item) to include that reference so each roadmap task directly
links to its source design scope.
🪄 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: dcd62bc0-6d92-431a-b4d5-38ffb170289f
📒 Files selected for processing (4)
.gitignoredocs/contents.mddocs/formal-verification-methods-in-wireframe.mddocs/roadmap.md
Replace the remaining second-person phrasing in the Stateright safety property note with project-neutral wording. Update roadmap item `9.8` so each checklist item points back to the relevant section of `docs/formal-verification-methods-in-wireframe.md`, keeping the implementation tasks tied to their source design scope.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Owner
Author
|
@coderabbitai review |
Contributor
✅ Actions performedReview triggered.
|
Contributor
There was a problem hiding this comment.
Actionable comments posted: 2
🤖 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/formal-verification-methods-in-wireframe.md`:
- Line 974: Replace the phrase "anti-patterns" in the sentence "A few
anti-patterns are worth ruling out explicitly." with the single-word form
"antipatterns" to conform to the requested technical writing convention; search
for the exact string "A few anti-patterns are worth ruling out explicitly." and
update it to use "antipatterns" so the sentence reads "A few antipatterns are
worth ruling out explicitly."
- Around line 1-1089: The Markdown file's prose paragraphs exceed the 80-column
limit; reflow all narrative paragraphs to wrap at 80 characters while preserving
the original content, leaving headings (e.g., "Executive summary", "Kani
integration", "Stateright integration"), code blocks, inline code, tables,
lists, and reference footnotes untouched; ensure bullet points and list items
are wrapped at 80 columns as well and that no headings or fenced code blocks are
altered.
🪄 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: 91c9ca04-45dc-405f-a5c0-35c2e2c43898
📒 Files selected for processing (2)
docs/formal-verification-methods-in-wireframe.mddocs/roadmap.md
Use `antipatterns` in the formal-verification guide so the sentence matches the requested technical writing convention.
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/formal-verification-methods-in-wireframe.md`:
- Line 42: Update the British-Oxford spelling to use the -ize suffix in the
sentence "- **Loom** stays in place for real synchronisation interleavings on
queue" by changing "synchronisation" to "synchronization"; apply the same Oxford
-ize change to the other occurrences called out (lines referenced in the review:
794, 929, 1024) so all instances use "synchronization" consistently across the
document.
🪄 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: e527ddaf-b061-4c7d-bb50-f695c1d5a21b
📒 Files selected for processing (1)
docs/formal-verification-methods-in-wireframe.md
Replace the remaining `synchronisation` spellings in the formal verification guide with `synchronization` to match the requested technical writing convention.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Contributor
There was a problem hiding this comment.
♻️ Duplicate comments (1)
docs/formal-verification-methods-in-wireframe.md (1)
793-795:⚠️ Potential issue | 🟡 MinorNormalize Oxford
-izespellings in remaining lines.Replace the remaining non-compliant forms to match repository spelling rules.
✏️ Proposed edit
-1. `cargo test` is the better starting point for the Stateright crate because - it minimises the delta from current Wireframe practice. If the wider repo +1. `cargo test` is the better starting point for the Stateright crate because + it minimizes the delta from current Wireframe practice. If the wider repo @@ -That will give Wireframe the highest bug-finding return for the least -organisational friction. +That will give Wireframe the highest bug-finding return for the least +organizational friction.As per coding guidelines, "
docs/**/*.md: Use British English based on the Oxford English Dictionary (en-GB-oxendict), including: suffix -ize ...".Also applies to: 1023-1024
🤖 Prompt for AI Agents
Verify each finding against the current code and only fix it if needed. In `@docs/formal-verification-methods-in-wireframe.md` around lines 793 - 795, Replace non‑Oxford -ize spellings in the sentence starting "cargo test is the better starting point for the Stateright crate because it minimises the delta..." by changing "minimises" to "minimizes", and scan the rest of the document for other -ise variants (e.g., any remaining "‑ise" suffixes referenced in the review) and normalize them to the Oxford "-ize" form so all occurrences (including the additional instances noted nearby) follow the repository en-GB-oxendict rule.
🤖 Prompt for all review comments with AI agents
Verify each finding against the current code and only fix it if needed.
Duplicate comments:
In `@docs/formal-verification-methods-in-wireframe.md`:
- Around line 793-795: Replace non‑Oxford -ize spellings in the sentence
starting "cargo test is the better starting point for the Stateright crate
because it minimises the delta..." by changing "minimises" to "minimizes", and
scan the rest of the document for other -ise variants (e.g., any remaining
"‑ise" suffixes referenced in the review) and normalize them to the Oxford
"-ize" form so all occurrences (including the additional instances noted nearby)
follow the repository en-GB-oxendict rule.
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 134ff5a3-3fe9-43f5-8cbf-e105cda230a9
📒 Files selected for processing (1)
docs/formal-verification-methods-in-wireframe.md
Update the formal-verification guide to use `minimizes` and `organizational` so the wording matches the repository's spelling convention.
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: 2
🤖 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/formal-verification-methods-in-wireframe.md`:
- Around line 218-262: Add a short prose description and a Mermaid diagram (with
an accessible short description immediately before it) that visualizes the
rollout and component split: show the main crate Kani harnesses, the
verification crate wireframe-verification (Stateright model), the verus/ proof
tree, and the phase ordering (e.g., build → Kani → Stateright → Verus) mapped to
CI targets; ensure diagram node/labels match the names "Kani",
"wireframe-verification", "verus/", "Stateright" and align the diagram text with
the listed phases and CI targets so readers and screen readers can correlate
phases to CI jobs. Apply the same addition to the other section mentioned (lines
935-970).
- Line 827: The workflow snippet uses the incomplete action ref string
"leynos/shared-actions/.github/actions/setup-rust@..." — replace the trailing
"@..." with a pinned commit SHA (preferred for production) or the placeholder
"<PINNED_SHA>" for documentation templates; update every occurrence of that
action ref (and any other refs using "@...") so the example workflows contain
explicit, auditable refs instead of the "@..." placeholder.
🪄 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: 1d602121-414b-49e1-84b0-ecbe058ce55c
📒 Files selected for processing (1)
docs/formal-verification-methods-in-wireframe.md
Document the formal-verification rollout with accessible Mermaid diagrams in both the repository-layout and first-tasks sections so the crate split, phase ordering, and CI targets are easier to correlate. Replace the `@...` action placeholders in the workflow examples with the documented `<PINNED_SHA>` placeholder so the examples use explicit, auditable refs.
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 by Sourcery
Document a recommended approach for integrating formal verification into Wireframe, including tooling choices, repository layout, and phased adoption strategy.
Documentation: