Add Kani tooling and local smoke targets (4.1.1)#305
Merged
Conversation
Draft the approval-gated plan for roadmap item 4.1.1. Capture the Kani version-pin, installer-script, and local Make target workflow, along with validation, review, and rollback guidance.
Contributor
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (1)
OverviewImplements roadmap task 4.1.1 by adding pinned Kani tooling integration and local smoke verification targets to the Netsuke formal‑verification workflow. Deliverables: a repository pin for Kani (tools/kani/VERSION → 0.67.0), an installer script, Makefile targets for Kani checks, a Kani version‑check script, and supporting documentation including a new ExecPlan (docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md). Key Changes
Rationale & Design
Validation
Scope & Next Steps
WalkthroughEstablish Kani bounded-model-checker support: pin version 0.67.0, add installer and version-check scripts, add Make targets ChangesKani tooling integration
Suggested labelsRoadmap Poem
Caution Pre-merge checks failedPlease resolve all errors before merging. Addressing warnings is optional.
❌ Failed checks (2 errors, 2 warnings, 1 inconclusive)
✅ Passed checks (13 passed)
✨ 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.
Pin the supported Kani verifier version and add the local installer script used by the formal-verification workflow.
Expose local Kani smoke and full-suite Make targets for the formal-verification workflow, document their use, and mark roadmap item 4.1.1 complete after validation.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Contributor
Reviewer's GuideAdds pinned Kani formal-verification tooling and opt-in Make targets, plus documentation and roadmap updates, to establish a repeatable local Kani smoke workflow without impacting existing CI/test paths. Sequence diagram for make formal-pr Kani smoke workflowsequenceDiagram
actor Developer
participant Make
participant cargo_kani
Developer->>Make: make formal-pr
Make->>Make: kani
Make->>cargo_kani: cargo kani --version
Flow diagram for scripts/install-kani.sh installation stepsflowchart TD
A[run scripts/install-kani.sh] --> B[require_command cargo]
B --> C[read tools/kani/VERSION]
C --> D[validate MAJOR.MINOR.PATCH]
D --> E[cargo install --locked kani-verifier --version <version>]
E --> F[cargo kani setup]
F --> G[cargo kani --version]
File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
![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 found 2 issues
Prompt for AI Agents
Please address the comments from this code review:
## Individual Comments
### Comment 1
<location path="docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md" line_range="44" />
<code_context>
+- Keep Makefile additions consistent with the current target style: variables
+ near the top, `.PHONY` declarations, target descriptions using `##`, and
+ recipes that honour overrideable variables.
+- Preserve the existing OrthoConfig and localized CLI help surfaces. This
+ item adds developer tooling, not a user-facing Netsuke subcommand or flag.
+- If any Kani-specific Rust source is introduced later during implementation,
</code_context>
<issue_to_address>
**issue (typo):** Align "localized" with the stated en-GB-oxendict spelling ("localised").
This bullet references en-GB-oxendict spelling but uses the en-US form "localized"; please change it to "localised" for consistency with the documented style.
```suggestion
- Preserve the existing OrthoConfig and localised CLI help surfaces. This
```
</issue_to_address>
### Comment 2
<location path="docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md" line_range="276" />
<code_context>
+
+## Context and orientation
+
+Netsuke is a Rust build-system compiler. It reads a YAML `Netsukefile`, expands
+MiniJinja-controlled manifest logic, validates a static Intermediate
+Representation (IR), emits a deterministic Ninja file, and delegates execution
</code_context>
<issue_to_address>
**suggestion (review_instructions):** The acronym “YAML” is used without being expanded on first use.
Please expand YAML on first use, for example: “YAML Ain’t Markup Language (YAML) `Netsukefile`”. Later occurrences can use “YAML” alone.
<details>
<summary>Review instructions:</summary>
**Path patterns:** `**/*.md`
**Instructions:**
Define uncommon acronyms on first use.
</details>
</issue_to_address>Help me be more useful! Please click 👍 or 👎 on each comment and I'll use the feedback to improve your reviews.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b9e59e9e6b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Route `make kani` through a smoke helper that reads `tools/kani/VERSION` and compares it with the installed `cargo-kani` version. This makes `formal-pr` fail when a developer or CI image has a stale or newer Kani binary installed. Update the developer guide and ExecPlan to document the pinned-version smoke check and address the review wording fixes.
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: 1
🤖 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 `@docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md`:
- Line 44: The document uses the en-GB-oxendict form inconsistently—replace
every instance of the word "localised" with "localized" (including the phrase
"localised CLI help surfaces" and the changelog note references around the file)
to normalize Oxford "-ize" spelling across the doc; search for the token
"localised" and update each occurrence (notably the inline text mentioning
OrthoConfig and the changelog entries) so the file consistently uses
"localized".
🪄 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 Plus
Run ID: ab7ea2b6-4490-41ec-b2a1-8de31f6f4931
📒 Files selected for processing (4)
Makefiledocs/developers-guide.mddocs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.mdscripts/check-kani-version.sh
Use Oxford `-ize` spelling consistently for localized help references in the Kani tooling ExecPlan.
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 current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md`:
- Around line 275-277: Remove the draft-only retrospective sentence "This
section is intentionally empty while the plan is in draft." from the document so
the section matches its "Status: COMPLETE" and the populated outcomes below;
locate the sentence in the retrospective paragraph (the one beginning with "This
section is intentionally empty...") and delete it, leaving the rest of the
section's content intact and aligned with the completed-plan wording.
- Around line 593-596: Update the rollback command block that currently lists
"git restore Makefile docs/developers-guide.md docs/roadmap.md" and "rm -rf
tools/kani scripts/install-kani.sh" to also remove
scripts/check-kani-version.sh; ensure the rollback step in the document (the
rollback command block) matches the repository's committed file list and any
declared interfaces in this doc so recovery steps remain synchronized with
what's introduced (i.e., include scripts/check-kani-version.sh alongside
tools/kani and scripts/install-kani.sh in the rm -rf step and verify the doc's
file list/interface section reflects the same set).
🪄 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 Plus
Run ID: 5f01d1e3-cbdd-456d-9062-fb9aca8be310
📒 Files selected for processing (1)
docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md
Remove stale draft-only retrospective wording and keep the rollback command block aligned with the committed Kani helper files.
Owner
Author
|
@coderabbitai please create a new GitHub issue for the following: Note that tests for shell scripts must be written in Python using ❌ Failed checks (2 errors, 2 warnings, 1 inconclusive)
|
Contributor
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: Length of output: 45 🏁 Script executed: Length of output: 144
It covers all four findings — the two errors (testing gap and module-level documentation) and the two warnings (docstring coverage and unit/behavioural tests) — and includes the requirement to use ✏️ Learnings added
|
This was referenced May 17, 2026
Open
This was referenced May 22, 2026
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
This branch implements roadmap task (4.1.1), adding the pinned local Kani tooling contract for Netsuke's formal-verification workflow.
It adds
tools/kani/VERSION,scripts/install-kani.sh, and the localmake kani,make kani-full, andmake formal-prtargets. It also documents the developer workflow and marks the roadmap item complete after validation.Roadmap task: (4.1.1)
Execplan: docs/execplans/4-1-1-kani-tooling-and-local-smoke-targets.md
Review walkthrough
tools/kani/VERSIONandscripts/install-kani.shfor the pinnedkani-verifierinstallation path.Makefilefor the opt-in Kani smoke, full-suite, and formal pull-request targets.docs/developers-guide.mdanddocs/roadmap.mdfor the developer workflow and completed roadmap checkboxes.Validation
scripts/install-kani.sh: passed, installedkani-verifier0.67.0 and rancargo kani setupmake kani: passedmake formal-pr: passedmake kani-full: passed; currently reports that no#[kani::proof]harnesses existmbake validate Makefile: passedmake check-fmt: passedmake lint: passedmake test: passedmake markdownlint: passedmake nixie: passedcoderabbit review --agent: passed with 0 findings on each milestone and final runNotes
make fmtwas attempted, but it still fails on pre-existing Markdown line-length and table issues in unrelated documentation. Formatter-only edits outside this branch's intended files were restored.Summary by Sourcery
Add pinned Kani formal-verification tooling and local make targets for smoke and full runs, along with developer documentation and roadmap updates.
New Features:
Enhancements:
Documentation: