Skip to content

Record Verus and Stateright phase-1 boundary (4.1.3) #311

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
leynos wants to merge 6 commits into
base: main
Choose a base branch
from
Open

Record Verus and Stateright phase-1 boundary (4.1.3) #311

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
77b2315
Add Verus and Stateright boundary plan
leynos May 22, 2026
f4593cb
Record Verus and Stateright phase-1 boundary
leynos May 24, 2026
2eff8cc
Use rust-prover-tools for prover workflows
leynos May 25, 2026
7bcb93f
Disable uv cache in CI setup
leynos May 26, 2026
a3cca33
Import updated agent instructions
leynos May 26, 2026
19f8eab
Import updated documentation style guide
leynos May 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,14 +80,16 @@ jobs:
uses: leynos/shared-actions/.github/actions/setup-rust@e4c6b0e200a057edf927c45c298e7ddf229b3934
with:
toolchain: stable
- name: Install uv
uses: astral-sh/setup-uv@4cda7d73322c50eac316ad623a716f09a2db2ac7 # v3.1.2
- name: Cache Kani tools
uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4.3.0
with:
path: |
.kani-cargo
.kani-home
key: ${{ runner.os }}-kani-${{ hashFiles('tools/kani/VERSION', 'scripts/install-kani.sh') }}
key: ${{ runner.os }}-kani-${{ hashFiles('tools/kani/VERSION', 'Makefile') }}
- name: Install Kani
run: scripts/install-kani.sh
run: make install-kani
- name: Kani smoke
run: make kani
121 changes: 88 additions & 33 deletions AGENTS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Assistant Instructions
# Assistant instructions

## Code Style and Structure
## Code style and structure

- **Code is for humans.** Write code with clarity and empathy—assume a
tired teammate will need to debug it at 3 a.m.
Expand All @@ -22,8 +22,8 @@
- **Group by feature, not layer.** Colocate views, logic, fixtures, and helpers
related to a domain concept rather than splitting by type.
- **Use consistent spelling and grammar.** Comments must use en-GB-oxendict
("-ize" / "-yse" / "-our") spelling and grammar, except for references to
external APIs.
("-ize" / "-yse" / "-our") spelling and grammar, with the exception of
references to external APIs.
- **Illustrate with clear examples.** Function documentation must include clear
examples demonstrating the usage and outcome of the function. Test
documentation should omit examples where the example serves only to reiterate
Expand All @@ -33,22 +33,31 @@
feature and constituents colocated with targets. Large blocks of test data
should be moved to external data files.

## Documentation Maintenance
## Documentation maintenance

- **Reference:** Use the markdown files within the `docs/` directory as a
knowledge base and source of truth for project requirements, dependency
choices, and architectural decisions.
choices, and architectural decisions. Start with
[documentation contents](docs/contents.md) and
[repository layout](docs/repository-layout.md) when orienting within the
project.
- **Update:** When new decisions are made, requirements change, libraries are
added/removed, or architectural patterns evolve, **proactively update** the
relevant file(s) in the `docs/` directory to reflect the latest state.
**Ensure the documentation remains accurate and current.**
- Documentation must use en-GB-oxendict ("-ize" / "-yse" / "-our") spelling
and grammar. (EXCEPTION: the LICENSE filename is left unchanged for community
consistency.)
- A documentation style guide is provided at
`docs/documentation-style-guide.md`.

## Change Quality & Committing
relevant file(s) in the `docs/` directory to reflect the latest state. Ensure
the documentation remains accurate and current.
- **Design decisions:** Record design decisions in the relevant design
document. When a decision is substantive, capture it in an Architectural
Decision Record (ADR) following the documentation style guide, and reference
that ADR from the design document.
- **User-facing behaviour:** Update [users' guide](docs/users-guide.md) for
behaviour or user-interface changes that users should know about.
- **Internal interfaces:** Document internally facing interfaces in the
relevant component architecture document. Document internally facing
conventions and practices in [developers' guide](docs/developers-guide.md).
- **Style:** All documentation must adhere to the
[documentation style guide](docs/documentation-style-guide.md).

## Change quality and committing

- **Atomicity:** Aim for small, focused, atomic changes. Each change (and
subsequent commit) should represent a single logical unit of work.
Expand Down Expand Up @@ -78,7 +87,7 @@
code snippets) within the commit message body.
- Do not commit changes that fail any of the quality gates.

## Refactoring Heuristics & Workflow
## Refactoring heuristics and workflow

- **Recognizing Refactoring Needs:** Regularly assess the codebase for potential
refactoring opportunities. Perform refactoring when observing:
Expand Down Expand Up @@ -109,7 +118,7 @@
pass before and after, unit tests added for new units).
- Ensure the refactoring commit itself passes all quality gates.

## Rust Specific Guidance
## Rust specific guidance

This repository is written in Rust and uses Cargo for building and dependency
management. Contributors should follow these best practices when working on the
Expand Down Expand Up @@ -151,26 +160,34 @@ project:
meaningfully named structs.
- Where a function is returning a large error, consider using `Arc` to reduce
the amount of data returned.
- Write unit and behavioural tests for new functionality. Run both before and
after making any change.
- Ensure that new features are validated with unit tests using `rstest` and
behavioural tests using `rstest-bdd` where applicable. Cover happy paths,
unhappy paths, and relevant edge cases.
- Add end-to-end tests where a change affects externally observable workflows,
integration contracts, persistence, command-line behaviour, network
boundaries, UI flows, or other system-level behaviour.
- Use property tests with `proptest` or a bounded model checker with `kani`
when a change introduces an invariant over a range of inputs, states,
orderings, or transitions. Use judgement to choose the appropriate level of
rigour.
- Use an exhaustive proof with `verus` for introduced lemmas or contractual
business logic. Proofs must be substantive, rigorous, and well-founded, not
merely a restatement of the assumed property.
- Run relevant unit, behavioural, property, model-checking, proof, and
end-to-end suites before and after making any change.
- Every module **must** begin with a module level (`//!`) comment explaining the
module's purpose and utility.
- Document public APIs using Rustdoc comments (`///`) so documentation can be
generated with cargo doc.
- Prefer immutable data and avoid unnecessary `mut` bindings.
- Handle errors with the `Result` type instead of panicking where feasible.
- Use explicit version ranges in `Cargo.toml` and keep dependencies up-to-date.
- Avoid `unsafe` code unless absolutely necessary, and document any usage
clearly.
clearly with a "SAFETY" comment.
- Place function attributes **after** doc comments.
- Do not use `return` in single-line functions.
- Use predicate functions for conditional criteria with more than two branches.
- Lints must not be silenced except as a **last resort**.
- Lint rule suppressions must be tightly scoped and include a clear reason.
- Prefer `expect` over `allow`.
- Use `rstest` fixtures for shared setup.
- Replace duplicated tests with `#[rstest(...)]` parameterized cases.
- Prefer `mockall` for mocks/stubs.
- Use `concat!()` to combine long string literals rather than escaping newlines
with a backslash.
- Prefer single line versions of functions where appropriate. i.e.,
Expand Down Expand Up @@ -201,22 +218,36 @@ project:
consistent without per-type boilerplate. Combine approaches: lean on
`newt-hype` for the common case, tuple structs for outliers, and
`the-newtype` to unify behaviour when owning the trait definitions.
- Use `cap_std` and `cap_std::fs_utf8` / `camino` in place of `std::fs` and
`std::path` for enhanced cross platform support and capabilities oriented
filesystem access.

### Testing

- Use `rstest` fixtures for shared setup.
- Replace duplicated tests with `#[rstest(...)]` parameterized cases.
- Prefer `mockall` for ad hoc mocks/stubs.
- For testing of functionality depending upon environment variables, dependency
injection and the `mockable` crate are the preferred option.
- If mockable cannot be used, env mutations in tests MUST be wrapped in shared
guards and mutexes placed in a shared `test_utils` or `test_helpers` crate.
Direct environment mutation is FORBIDDEN in tests.

### Dependency Management
### Dependency management

- **Mandate caret requirements for all dependencies.** All crate versions
specified in `Cargo.toml` must use SemVer-compatible caret requirements
(e.g., `some-crate = "1.2.3"`). This is Cargo's default and allows for safe,
specified in `Cargo.toml` must use SemVer-compatible caret requirements (e.g.,
`some-crate = "1.2.3"`). This is Cargo's default and allows for safe,
non-breaking updates to minor and patch versions while preventing breaking
changes from new major versions. This approach is critical for ensuring build
stability and reproducibility.
- **Prohibit unstable version specifiers.** The use of wildcard (`*`) or
open-ended inequality (`>=`) version requirements is strictly forbidden as
they introduce unacceptable risk and unpredictability. Tilde requirements
(`~`) should only be used where a dependency must be locked to patch-level
they introduce unacceptable risk and unpredictability. Tilde requirements (
`~`) should only be used where a dependency must be locked to patch-level
updates for a specific, documented reason.

### Error Handling
### Error handling

- **Prefer semantic error enums**. Derive `std::error::Error` (via the
`thiserror` crate) for any condition the caller might inspect, retry, or map
Expand All @@ -239,7 +270,31 @@ project:
- Consume fallible fixtures in `rstest` by **making the test return `Result`**
and applying `?` to the fixture.

## Markdown Guidance
### Observability

- Use `tracing` for logging and diagnostics. Prefer structured
`tracing::{trace, debug, info, warn, error}` events and spans over `println!`,
`eprintln!`, or direct `log` macros. Add fields for identifiers, state, and
error context so downstream subscribers can filter and correlate events
without parsing message text.
- Use `#[tracing::instrument]` or explicit spans around request handling,
command execution, retries, background jobs, and other meaningful units of
work. Do not hold `Span::enter()` guards across `.await`; use
`Instrument::instrument` or scoped synchronous spans instead.
- Use the `metrics` crate for metric emission where usage, uptake, failure,
or mitigation metrics are required. Prefer `counter!` for cumulative events,
`gauge!` for values that rise and fall, and `histogram!` for distributions
such as latency or payload size.
- Describe emitted metrics with `describe_counter!`, `describe_gauge!`, or
`describe_histogram!` where the unit or purpose is not obvious from the
metric name. Keep metric names stable and labels low-cardinality; do not put
user input, request IDs, paths with unbounded parameters, or raw error
strings into labels.
- Libraries may emit `metrics` and `tracing` instrumentation, but must not
install global recorders or subscribers. Applications should initialise
Copy link
Copy Markdown
Contributor

@coderabbitai coderabbitai Bot May 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️ Potential issue | 🟡 Minor | ⚡ Quick win

Use Oxford -ize spelling in normative guidance.

Replace initialise with initialize to align with the repository’s en-GB-oxendict rule.

Triage: [type:spelling] [type:docstyle]

Suggested patch 
-  install global recorders or subscribers. Applications should initialise
+  install global recorders or subscribers. Applications should initialize

As per coding guidelines: “Use British English based on the Oxford English Dictionary locale en-GB-oxendict, including suffix -ize in words like 'realize' and 'organization'.”

🧰 Tools
🪛 LanguageTool

[style] ~294-~294: Would you like to use the Oxford spelling “initialize”? The spelling ‘initialise’ is also correct.
Context: ...ers or subscribers. Applications should initialise exporters/subscribers once, as early ...

(OXFORD_SPELLING_Z_NOT_S)

🤖 Prompt for 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.

In `@AGENTS.md` at line 294, Replace the British spelling "initialise" with the
Oxford -ize form "initialize" in the sentence containing "install global
recorders or subscribers. Applications should initialise" in AGENTS.md so the
file follows the en-GB-oxendict rule; update the single occurrence to
"initialize" ensuring the rest of the sentence and punctuation remain unchanged.

exporters/subscribers once, as early as practical in startup.

## Markdown guidance

- Validate Markdown files using `make markdownlint`.
- Run `make fmt` after any documentation changes to format all Markdown
Expand Down Expand Up @@ -291,7 +346,7 @@ The following tooling is available in this environment:
- `difft` **(Difftastic)** — Semantic diff tool that compares code structure
rather than just text differences.

## Key Takeaway
## Key takeaway

These practices help maintain a high-quality codebase and facilitate
collaboration.
20 changes: 17 additions & 3 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,15 +1,20 @@
.PHONY: help all clean test build release lint fmt check-fmt typecheck markdownlint nixie kani kani-full formal-pr
.PHONY: help all clean test build release lint fmt check-fmt typecheck markdownlint nixie install-kani kani kani-full install-verus verus formal-pr

APP ?= netsuke
CARGO ?= $(shell command -v cargo 2>/dev/null || printf '%s' "$$HOME/.cargo/bin/cargo")
BUILD_JOBS ?=
CLIPPY_FLAGS ?= --all-targets --all-features -- -D warnings
KANI ?= cargo kani
KANI_FLAGS ?=
KANI_VERSION_CHECK ?= scripts/check-kani-version.sh
KANI_INSTALL_FLAGS ?=
KANI_CHECK_FLAGS ?=
MDLINT ?= $(shell command -v markdownlint-cli2 2>/dev/null || printf '%s' "$$HOME/.bun/bin/markdownlint-cli2")
NIXIE ?= nixie
PROVER_TOOLS_SOURCE ?= git+https://github.com/leynos/rust-prover-tools@b07ef696f8373d54ae68e517d39d47a5d27a5bd5
PROVER_TOOLS ?= uv tool run --from $(PROVER_TOOLS_SOURCE) prover-tools
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot May 26, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Remove hard runtime fetch from the Kani smoke path

The new PROVER_TOOLS command shells out to uv tool run --from git+https://... for both make install-kani and make kani, which means the formal-verification smoke path now depends on reaching GitHub at runtime. In any restricted or offline environment, make kani/make formal-pr can fail before invoking cargo kani, even when Kani is already installed, because the helper itself cannot be resolved. This introduces a reliability regression in CI and local validation compared with the previous repository-local scripts.

Useful? React with 👍 / 👎.

RUSTDOC_FLAGS ?= --cfg docsrs -D warnings
VERUS_FLAGS ?=
VERUS_INSTALL_FLAGS ?=

export PATH := $(HOME)/.cargo/bin:$(HOME)/.bun/bin:$(PATH)

Expand Down Expand Up @@ -47,12 +52,21 @@ markdownlint: ## Lint Markdown files
nixie: ## Validate Mermaid diagrams
nixie --no-sandbox

install-kani: ## Install the pinned Kani verifier
$(PROVER_TOOLS) kani install $(KANI_INSTALL_FLAGS)

kani: ## Run the Kani local smoke check
KANI="$(KANI)" $(KANI_VERSION_CHECK)
$(PROVER_TOOLS) kani check-version --kani-command "$(KANI)" $(KANI_CHECK_FLAGS)

kani-full: ## Run the full Kani verification suite
$(KANI) $(KANI_FLAGS)

install-verus: ## Install the pinned Verus verifier
$(PROVER_TOOLS) verus install $(VERUS_INSTALL_FLAGS)

verus: ## Run the Verus proof entry point
$(PROVER_TOOLS) verus run $(VERUS_FLAGS)

formal-pr: ## Run pull-request formal-verification checks
$(MAKE) kani

Expand Down
40 changes: 28 additions & 12 deletions docs/developers-guide.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,14 +85,15 @@ repository work.
Install or refresh the pinned Kani tool with:

```bash
scripts/install-kani.sh
make install-kani
```

The installer reads `tools/kani/VERSION`, runs
`cargo install --locked kani-verifier --version <version>`, runs
`cargo kani setup`, and verifies that `cargo kani` is callable. Kani may manage
its own supporting Rust nightly toolchain during setup. That toolchain must not
replace the repository's ordinary stable Rust workflow.
`make install-kani` delegates to the pinned `rust-prover-tools` CLI through
`uv tool run`. The prover tool reads `tools/kani/VERSION`, runs
`cargo install --locked kani-verifier --version <version>`, runs `cargo kani
setup`, and verifies that `cargo kani` is callable. Kani may manage its own
supporting Rust nightly toolchain during setup. That toolchain must not replace
the repository's ordinary stable Rust workflow.

Use the Make targets for day-to-day formal-verification checks:

Expand All @@ -102,17 +103,32 @@ Use the Make targets for day-to-day formal-verification checks:
- `make kani-full` is reserved for the full Kani proof suite once harnesses
exist. Today it invokes `cargo kani` without additional smoke flags.
- `make formal-pr` aliases the pull-request formal-verification smoke path.
- `make install-verus` and `make verus` delegate to `rust-prover-tools` for
the optional Verus installer and proof runner. These targets are not part of
the ordinary pull-request gate.

Kani is intentionally not part of `make test`, `make lint`, `make check-fmt`,
or `make all`.

Phase 1 keeps the rest of the formal-verification surface deliberately narrow.
Kani is the only supported and gated formal-verification tool today. Verus is
optional, proof-kernel-only, and not installed or run by default; any first
Verus work must stay outside ordinary Cargo and focus on a small cycle
canonicalization model. Stateright is deferred entirely until Netsuke gains an
accepted stateful concurrent subsystem such as a daemon, watch service,
remote-execution coordinator, actor protocol, or internal scheduler with
long-lived mutable control-plane state. See
[`docs/formal-verification-methods-in-netsuke.md`](formal-verification-methods-in-netsuke.md)
for the design rationale and re-entry criteria.

Pull requests run a dedicated `kani-smoke` CI job alongside the ordinary
`build-test` job. The job installs the pinned Kani version with
`scripts/install-kani.sh` and runs only `make kani`; it does not run
`make kani-full`, coverage, CodeScene upload, or the normal build matrix. Its
cache is intentionally separate from ordinary Cargo build artefacts: the job
uses a Kani-specific cache key derived from `tools/kani/VERSION` and caches the
job-local Kani Cargo home plus Kani support-file home.
`build-test` job. The job installs `uv`, installs the pinned Kani version
through `make install-kani`, and runs only `make kani`; it does not run
`make kani-full`, `make verus`, coverage, CodeScene upload, or the normal build
matrix. Its cache is intentionally separate from ordinary Cargo build
artefacts: the job uses a Kani-specific cache key derived from
`tools/kani/VERSION` and the Makefile, then caches the job-local Kani Cargo
home plus Kani support-file home.

## Test suite map

Expand Down
Loading
Loading