[feliperodri]

This PR adds the Kani agent plugin. The goal is to make Kani easy to try and adopt from the coding agents Rust developers already use (Kiro, Claude Code, Copilot/VS Code, Cursor, Codex). An agent can verify a property, write or improve a proof harness, run Kani, explain a counterexample, and check that a passing proof is not vacuous, without the user first learning every Kani command.

What's included

• agent-plugin/skills/verify-rust/: the orchestration skill. Steps: pin down the property, check Kani is installed, write the harness, run Kani with --export-json, get a counterexample via concrete playback, check vacuity and assumptions, and report exactly what was proven, with its bounds and stubs. Detailed guidance lives in references/ (Kani, AutoHarness, contracts, Miri, rust-analyzer, vacuity).
• agent-plugin/scripts/ (Python 3 only, JSON output):
  • summarize-results.py: a compact summary of an RFC 0015 export.
  • check-vacuity.py: unreachable assertions and unsatisfiable covers.
  • check-assumptions.py: contradictory, pinned, or success-assuming kani::assume, and requires(false).
  • inspect-harness.py: harness structure.
  • check-kani-version.py: checks the installed Kani against the plugin's supported range.
• Proof-integrity checks, so an agent cannot get a green result by weakening the proof:
  • summarize-results.py (and kani_verify_harness) report weakened_checks (disabled checks, raw CBMC arguments) and, per harness, the stubs and stub_verified contracts the result relies on.
  • check-specs.py checks specs with Kani itself, in a temporary copy of the crate: is the end of each harness reachable, are contract preconditions satisfiable, does a clause constrain nothing, and is a changed precondition stronger or weaker than the baseline's. A check that cannot run is reported as unchecked, never as passing.
  • check-proof-diff.py compares harnesses, contracts, and code with the baseline the user approved. It flags removed assertions or covers, new assumptions, stubs, should_panic, lower unwind bounds, changed contracts, and any change to the code under verification.
  • check-witness.py confirms a defect (its concrete playback witness fails) or a fix (the witness fails before the fix and passes after).
  • evidence.py records the run behind a reported result, and re-checks it later.
  • The skill pins the agreed property, forbids silent code changes, and requires evidence for every claim. A new strategy.md reference covers when to write one harness and when to prove contracts bottom-up along the call graph, which comes from rust-analyzer's call hierarchy.
• tools/kani-mcp: a minimal MCP server, stdio only, with no new dependencies. It has four tools: kani_get_version, kani_list_harnesses, kani_verify_harness, and kani_get_counterexample. It shells out to the user's installed Kani. MCP is optional: the skill falls back to the CLI, which covers every feature, including AutoHarness.
• Compatibility: the plugin is versioned on its own. compatibility.json says plugin 0.1.0 supports Kani >= 0.68.0, < 1.0.0; 0.68.0 is the first release with --export-json. Both the script and the MCP tool enforce this range.

Testing

• agent-plugin/tests/validate_plugin.py checks manifests, skill frontmatter, and links.
• agent-plugin/tests/test_scripts.py has 48 unit tests over the existing RFC 0015 fixtures and Rust samples, and needs no Kani.
• cargo test -p kani-mcp runs 16 unit tests.
  • The three items above run in a new path-filtered Agent Plugin workflow.
• The new agent-plugin exec suite in kani-regression.sh runs end to end against a fixture crate with one good proof, one real overflow, and one vacuous proof. It checks:
  • version detection, including a clear error for an old or missing Kani;
  • the CLI-only workflow: JSON summary, concrete playback, vacuity and assumption checks, and AutoHarness through the CLI;
  • all four MCP tools over stdio, including that kani_verify_harness matches summarize-results.py;
  • proof integrity: Kani-backed spec checks catch a vacuous harness and an unsatisfiable precondition; the proof diff catches a cheating edit; a witness confirms the defect and then the fix; an evidence bundle re-verifies and detects a changed source.
• Manual testing: drove kani-mcp over stdio by hand on sample files. The suite passes locally through compiletest on macOS.

Field testing

A trial run on two real crates found one real defect in each, and a list of false results and usability problems in the scripts and MCP server. All of them are fixed in this PR:

• multi-line contract attributes are parsed;
• assumptions in helper functions count toward the harness;
• built-in checks are no longer reported as vacuous user assertions;
• contracts on methods are checked;
• witnesses work when a crate's test targets don't build under cfg(kani), and failures caused only by stubs are reported as spurious;
• evidence covers every source file;
• the MCP tools have timeouts, progress notifications, parallel jobs, and export/log paths, and listing returns a summary by default;
• the version check verifies that the toolchain works.

A second round on three crates confirmed most of those fixes and found more, now also fixed:

• the plugin no longer lets rustup install a toolchain a project pins (it pins RUSTUP_TOOLCHAIN to an installed toolchain and disables auto-install);
• unreachable checks are classified by location;
• a witness only confirms a defect when it panics with the failure Kani reported;
• the proof diff catches a harness that loses #[kani::proof] and resolves helpers by path;
• work copies keep external path dependencies resolvable;
• MCP timeouts return the harnesses that finished.

Not done yet

• End-to-end sessions in real agents (Kiro, Claude Code).
• Review against prior art (KVerus, ExVerus).
• Marketplace-specific manifests and submissions.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Warning

Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.

Copilot review overview

No open issues 🎉

What changed in this PR

Adds a Kani agent plugin plus a minimal MCP server (kani-mcp) to make Kani verification workflows accessible to coding agents, with helper scripts and CI/smoke tests to validate behavior and compatibility.

Changes:

• Introduces kani-mcp (stdio JSON-RPC/MCP server) with tools for version, harness listing, verification summaries, and counterexamples.
• Adds Python helper scripts and tests for summarizing --export-json, vacuity/assumption checks, and plugin metadata validation.
• Adds CI workflow + regression suite hooks and end-to-end smoke tests for CLI fallback and MCP tool parity.

File	Description
tools/​kani-mcp/​src/​summary.rs	Rust implementation of compact RFC0015 export summary (mirrors Python script) + unit test fixture coverage
tools/​kani-mcp/​src/​main.rs	MCP stdio server implementing kani_get_version, kani_list_harnesses, kani_verify_harness, kani_get_counterexample
tools/​kani-mcp/​Cargo.toml	New kani-mcp crate definition and dependencies
Cargo.toml	Adds tools/kani-mcp to workspace members
tests/​agent-plugin/​version-check/​test.sh	Smoke test for version enforcement and error clarity
tests/​agent-plugin/​version-check/​config.yml	Registers version-check smoke test
tests/​agent-plugin/​mcp/​test.sh	End-to-end MCP tool exercise + parity check vs CLI summary
tests/​agent-plugin/​mcp/​config.yml	Registers MCP smoke test
tests/​agent-plugin/​cli-fallback/​test.sh	End-to-end skill workflow through CLI-only (export, summary, vacuity/assumptions, playback, autoharness)
tests/​agent-plugin/​cli-fallback/​config.yml	Registers CLI-fallback smoke test
scripts/​kani-regression.sh	Adds agent-plugin exec suite to regression
.github/​workflows/​agent-plugin.yml	New path-filtered workflow to validate plugin + run unit tests
agent-plugin/​plugin.json	Plugin manifest (name/version/paths/metadata)
agent-plugin/​mcp.json	Registers local stdio MCP server command (kani-mcp)
agent-plugin/​compatibility.json	Supported Kani range + required unstable features
agent-plugin/​README.md	Plugin documentation, installation, tools/scripts overview
agent-plugin/​tests/​validate_plugin.py	Validation for manifests, versions, skill frontmatter, and reference/script presence
agent-plugin/​tests/​test_scripts.py	Unit tests for Python scripts using JSON fixtures + Rust source fixtures
agent-plugin/​tests/​smoke-lib.sh	Shared harness for smoke tests (temp fixture crate, build kani-mcp, helpers)
agent-plugin/​tests/​mcp_client.py	Minimal MCP stdio client used by smoke tests
agent-plugin/​tests/​fixtures/​rust/​assumptions.rs	Rust text fixture for assumption scanner tests
agent-plugin/​tests/​fixtures/​crate/​Cargo.toml	Fixture crate used by end-to-end smoke tests
agent-plugin/​tests/​fixtures/​crate/​src/​lib.rs	Fixture crate code + proof harnesses (good/failing/vacuous)
agent-plugin/​scripts/​kani_plugin_lib.py	Shared text-scanning utilities for plugin scripts
agent-plugin/​scripts/​summarize-results.py	Python compact summary implementation of RFC0015 export
agent-plugin/​scripts/​check-vacuity.py	Python vacuity checker over RFC0015 export
agent-plugin/​scripts/​check-assumptions.py	Python assumption checker over Rust source text
agent-plugin/​scripts/​check-kani-version.py	Python Kani version-range validator
agent-plugin/​scripts/​inspect-harness.py	Python harness structure inspector
agent-plugin/​skills/​verify-rust/​SKILL.md	Skill orchestration workflow/policy for agents
agent-plugin/​skills/​verify-rust/​references/​kani.md	Reference guidance for harness writing/running Kani
agent-plugin/​skills/​verify-rust/​references/​vacuity.md	Reference guidance for vacuity/sanity checks
agent-plugin/​skills/​verify-rust/​references/​contracts.md	Reference guidance for contracts
agent-plugin/​skills/​verify-rust/​references/​autoharness.md	Reference guidance for autoharness usage
agent-plugin/​skills/​verify-rust/​references/​miri.md	Reference guidance for Miri complementing Kani
agent-plugin/​skills/​verify-rust/​references/​rust-analyzer.md	Reference guidance for using rust-analyzer in verification workflows

_{Review effort: Lite}