Background
Kani integration tests for the harnesses introduced in skills/kani/references/kani-harness-example.rs and documented in skills/kani/SKILL.md require the Kani toolchain (cargo kani setup) and a Rust nightly compiler. Neither is currently available in this repository's CI environment.
This issue was identified during review of #13 (Add Kani and Verus agent skills for Rust formal verification).
Requested by @leynos.
Work required
- Provision the Kani toolchain in CI (e.g. via a dedicated GitHub Actions job that installs
cargo kani and runs cargo kani setup).
- Add integration tests that invoke
cargo kani against the harnesses in skills/kani/references/kani-harness-example.rs.
- Gate the Kani CI job appropriately (e.g. on push to
main or on PRs touching skills/kani/) to avoid unnecessary overhead.
- Document the CI additions in
docs/developers-guide.md under the "Formal verification tooling" section.
References
Background
Kani integration tests for the harnesses introduced in
skills/kani/references/kani-harness-example.rsand documented inskills/kani/SKILL.mdrequire the Kani toolchain (cargo kani setup) and a Rust nightly compiler. Neither is currently available in this repository's CI environment.This issue was identified during review of #13 (Add Kani and Verus agent skills for Rust formal verification).
Requested by @leynos.
Work required
cargo kaniand runscargo kani setup).cargo kaniagainst the harnesses inskills/kani/references/kani-harness-example.rs.mainor on PRs touchingskills/kani/) to avoid unnecessary overhead.docs/developers-guide.mdunder the "Formal verification tooling" section.References
skills/kani/SKILL.mdskills/kani/references/kani-harness-example.rs