diff --git a/Cargo.lock b/Cargo.lock index d0a5d939a02..5fcffa47c55 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -491,7 +491,7 @@ dependencies = [ "crossterm_winapi", "document-features", "parking_lot", - "rustix", + "rustix 1.1.2", "winapi", ] @@ -1021,6 +1021,20 @@ dependencies = [ "which 8.0.0", ] +[[package]] +name = "kani-mcp-server" +version = "0.1.0" +dependencies = [ + "anyhow", + "serde", + "serde_json", + "thiserror 1.0.69", + "tokio", + "tracing", + "tracing-subscriber", + "which 6.0.3", +] + [[package]] name = "kani-verifier" version = "0.66.0" @@ -1083,6 +1097,12 @@ dependencies = [ "serde_test", ] +[[package]] +name = "linux-raw-sys" +version = "0.4.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d26c52dbd32dccf2d10cac7725f8eae5296885fb5703b261f7d0a0739ec807ab" + [[package]] name = "linux-raw-sys" version = "0.11.0" @@ -1724,6 +1744,19 @@ dependencies = [ "semver", ] +[[package]] +name = "rustix" +version = "0.38.44" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fdb5bc1ae2baa591800df16c9ca78619bf65c0488b41b96ccec5d11220d8c154" +dependencies = [ + "bitflags", + "errno", + "libc", + "linux-raw-sys 0.4.15", + "windows-sys 0.59.0", +] + [[package]] name = "rustix" version = "1.1.2" @@ -1733,7 +1766,7 @@ dependencies = [ "bitflags", "errno", "libc", - "linux-raw-sys", + "linux-raw-sys 0.11.0", "windows-sys 0.61.2", ] @@ -1941,6 +1974,16 @@ version = "1.15.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03" +[[package]] +name = "socket2" +version = "0.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "17129e116933cf371d018bb80ae557e889637989d8638274fb25622827b03881" +dependencies = [ + "libc", + "windows-sys 0.60.2", +] + [[package]] name = "stacker" version = "0.1.22" @@ -2027,7 +2070,7 @@ dependencies = [ "fastrand", "getrandom", "once_cell", - "rustix", + "rustix 1.1.2", "windows-sys 0.61.2", ] @@ -2137,11 +2180,25 @@ dependencies = [ "bytes", "libc", "mio", + "parking_lot", "pin-project-lite", "signal-hook-registry", + "socket2", + "tokio-macros", "windows-sys 0.61.2", ] +[[package]] +name = "tokio-macros" +version = "2.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "af407857209536a95c8e56f8231ef2c2e2aff839b22e07a1ffcbc617e9db9fa5" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "toml" version = "0.8.23" @@ -2478,6 +2535,18 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "which" +version = "6.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b4ee928febd44d98f2f459a4a79bd4d928591333a494a10a868418ac1b39cf1f" +dependencies = [ + "either", + "home", + "rustix 0.38.44", + "winsafe", +] + [[package]] name = "which" version = "7.0.3" @@ -2486,7 +2555,7 @@ checksum = "24d643ce3fd3e5b54854602a080f34fb10ab75e0b813ee32d00ca2b44fa74762" dependencies = [ "either", "env_home", - "rustix", + "rustix 1.1.2", "winsafe", ] @@ -2497,7 +2566,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d3fabb953106c3c8eea8306e4393700d7657561cb43122571b172bbfb7c7ba1d" dependencies = [ "env_home", - "rustix", + "rustix 1.1.2", "winsafe", ] @@ -2597,7 +2666,16 @@ version = "0.59.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" dependencies = [ - "windows-targets", + "windows-targets 0.52.6", +] + +[[package]] +name = "windows-sys" +version = "0.60.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2f500e4d28234f72040990ec9d39e3a6b950f9f22d3dba18416c35882612bcb" +dependencies = [ + "windows-targets 0.53.5", ] [[package]] @@ -2615,14 +2693,31 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", + "windows_aarch64_gnullvm 0.52.6", + "windows_aarch64_msvc 0.52.6", + "windows_i686_gnu 0.52.6", + "windows_i686_gnullvm 0.52.6", + "windows_i686_msvc 0.52.6", + "windows_x86_64_gnu 0.52.6", + "windows_x86_64_gnullvm 0.52.6", + "windows_x86_64_msvc 0.52.6", +] + +[[package]] +name = "windows-targets" +version = "0.53.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4945f9f551b88e0d65f3db0bc25c33b8acea4d9e41163edf90dcd0b19f9069f3" +dependencies = [ + "windows-link", + "windows_aarch64_gnullvm 0.53.1", + "windows_aarch64_msvc 0.53.1", + "windows_i686_gnu 0.53.1", + "windows_i686_gnullvm 0.53.1", + "windows_i686_msvc 0.53.1", + "windows_x86_64_gnu 0.53.1", + "windows_x86_64_gnullvm 0.53.1", + "windows_x86_64_msvc 0.53.1", ] [[package]] @@ -2631,48 +2726,96 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.53.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a9d8416fa8b42f5c947f8482c43e7d89e73a173cead56d044f6a56104a6d1b53" + [[package]] name = "windows_aarch64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" +[[package]] +name = "windows_aarch64_msvc" +version = "0.53.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9d782e804c2f632e395708e99a94275910eb9100b2114651e04744e9b125006" + [[package]] name = "windows_i686_gnu" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" +[[package]] +name = "windows_i686_gnu" +version = "0.53.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "960e6da069d81e09becb0ca57a65220ddff016ff2d6af6a223cf372a506593a3" + [[package]] name = "windows_i686_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" +[[package]] +name = "windows_i686_gnullvm" +version = "0.53.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fa7359d10048f68ab8b09fa71c3daccfb0e9b559aed648a8f95469c27057180c" + [[package]] name = "windows_i686_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" +[[package]] +name = "windows_i686_msvc" +version = "0.53.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e7ac75179f18232fe9c285163565a57ef8d3c89254a30685b57d83a38d326c2" + [[package]] name = "windows_x86_64_gnu" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" +[[package]] +name = "windows_x86_64_gnu" +version = "0.53.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9c3842cdd74a865a8066ab39c8a7a473c0778a3f29370b5fd6b4b9aa7df4a499" + [[package]] name = "windows_x86_64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.53.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ffa179e2d07eee8ad8f57493436566c7cc30ac536a3379fdf008f47f6bb7ae1" + [[package]] name = "windows_x86_64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" +[[package]] +name = "windows_x86_64_msvc" +version = "0.53.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d6bbff5f0aada427a1e5a6da5f1f98158182f26556f345ac9e04d36d0ebed650" + [[package]] name = "winnow" version = "0.7.13" diff --git a/Cargo.toml b/Cargo.toml index 2d82261b3ec..b2dd3fb82b4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -52,7 +52,7 @@ members = [ "kani-driver", "kani-compiler", "kani_metadata", - "library/kani_core", + "library/kani_core", "kani-mcp-server", ] # This indicates what package to e.g. build with 'cargo build' without --workspace @@ -60,6 +60,7 @@ default-members = [ ".", "kani-driver", "kani-compiler", + "kani-mcp-server", ] exclude = [ diff --git a/kani-mcp-server/Cargo.toml b/kani-mcp-server/Cargo.toml new file mode 100644 index 00000000000..e9c25c0c527 --- /dev/null +++ b/kani-mcp-server/Cargo.toml @@ -0,0 +1,22 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "kani-mcp-server" +version = "0.1.0" +edition = "2024" +description = "Model Context Protocol server for Kani Rust Verifier - enables AI assistants like Amazon Q to run formal verification" +license = "MIT OR Apache-2.0" + +[dependencies] +tokio = { version = "1", features = ["full"] } +serde = { version = "1", features = ["derive"] } +serde_json = "1" +anyhow = "1" +thiserror = "1" +tracing = "0.1" +tracing-subscriber = { version = "0.3", features = ["env-filter"] } +which = "6" + +[lints] +workspace = true \ No newline at end of file diff --git a/kani-mcp-server/README.md b/kani-mcp-server/README.md new file mode 100644 index 00000000000..e7fb4d54012 --- /dev/null +++ b/kani-mcp-server/README.md @@ -0,0 +1,476 @@ +# Amazon Q CLI with Kani MCP Server + +Complete guide for setting up and using Amazon Q CLI with the Kani verification MCP server. + +## Table of Contents + +- [Installing Amazon Q CLI](#installing-amazon-q-cli) +- [Setting Up Your AWS Builder ID](#setting-up-your-aws-builder-id) +- [Installing the Kani MCP Server](#installing-the-kani-mcp-server) +- [Configuring Amazon Q CLI](#configuring-amazon-q-cli) +- [Using Amazon Q with Kani](#using-amazon-q-with-kani) +- [Troubleshooting](#troubleshooting) +- [Quick Reference](#quick-reference) + +--- + +## Installing Amazon Q CLI + +### Prerequisites + +- macOS +- Internet connection +- Homebrew (recommended) + +### Installation Methods + +#### Option 1: Homebrew (Recommended) + +```bash +# Install Amazon Q CLI +brew install --cask amazon-q + +# Verify installation +q --version +``` + +#### Option 2: Direct Download + +1. Download from the official AWS documentation +2. Double-click the .dmg file +3. Drag Amazon Q to Applications folder +4. Open Amazon Q from Applications +5. Enable shell integrations when prompted + +### Post-Installation Setup + +After installation, restart your terminal and verify: + +```bash +# Check if q command is available +which q + +# Check version +q --version + +# Run diagnostics +q doctor +``` + +--- + +## Setting Up Your AWS Builder ID + +Amazon Q CLI requires a free AWS Builder ID for authentication. + +### Step 1: Login + +```bash +q login +``` + +This will: +- Open your web browser automatically +- Direct you to the AWS Builder ID login page +- Ask you to either sign in or create a new Builder ID + +### Step 2: Create Builder ID (First Time Users) + +If you don't have a Builder ID: + +1. Click "Create AWS Builder ID" on the login page +2. Enter your email address +3. Choose a display name +4. Verify your email (check your inbox) +5. Complete the registration + +### Step 3: Authorize Amazon Q + +1. After logging in, authorize Amazon Q Developer +2. Return to your terminal +3. You should see a success message + +### Verification + +```bash +# Check authentication status +q doctor + +# You should see: +# ✔ Everything looks good! +``` + +--- + +## Installing the Kani MCP Server + +### Prerequisites + +Install [Kani Rust Verifier](https://model-checking.github.io/kani/) - a model checker for Rust: + +```bash +# Install Kani +cargo install --locked kani-verifier +cargo kani setup + +# Verify installation +cargo kani --version +``` + +### Clone and Build Kani MCP Server + +```bash +# Clone the repository +git clone +cd kani-mcp-server + +# Build the server +cargo build --release + +# Verify the binary exists +ls -lh target/release/kani-mcp-server +``` + +The binary will be at: `target/release/kani-mcp-server` + +--- + +## Configuring Amazon Q CLI + +### Step 1: Create MCP Configuration Directory + +```bash +mkdir -p ~/.aws/amazonq +``` + +### Step 2: Create MCP Configuration File + +Create `~/.aws/amazonq/mcp.json`: + +```bash +cat > ~/.aws/amazonq/mcp.json << 'EOF' +{ + "mcpServers": { + "kani-verifier": { + "command": "/absolute/path/to/kani-mcp-server", + "env": {}, + "disabled": false, + "autoApprove": [] + } + } +} +EOF +``` + +**Important:** Replace `/absolute/path/to/kani-mcp-server` with your actual path, for example: +- `/Users/yourusername/target/release/kani-mcp-server` + +### Step 3: Verify Configuration + +```bash +# Check the config file exists +cat ~/.aws/amazonq/mcp.json + +# Verify the path is correct +ls -lh /absolute/path/to/kani-mcp-server +``` + +### Step 4: Test MCP Server Loading + +```bash +# Start Amazon Q CLI +q chat + +# You should see: +# ✓ kani-verifier loaded in 0.0X s +``` + +If you see this message, your MCP server is successfully configured! ✅ + +--- + +## Using Amazon Q with Kani + +### Starting a Chat Session + +```bash +q chat +``` + +### Basic Commands + +Inside the Q chat interface: + +- **Send a message:** Just type and press Enter +- **Multi-line input:** Press `Ctrl + J` for new lines +- **Exit:** Type `/q` or press `Ctrl + C` +- **Help:** Type `/help` +- **Clear screen:** Type `/clear` + +### Checking Available Tools + +Once in the chat, verify your Kani tools are loaded: + +``` +What MCP tools do you have? +``` + +You should see: +- `verify_rust_project` - Run Kani verification on a Rust project +- `verify_unsafe_code` - Verify unsafe Rust code blocks +- `explain_failure` - Analyze verification failures +- `generate_kani_harness` - Generate proof harness templates + +### Example Usage Scenarios + +#### 1. Verify a Rust Project + +``` +I have a Rust project at ~/my-project. Can you verify it with Kani? +``` + +Or more specifically: + +``` +Run Kani verification on the project at /Users/username/my-project +with the harness function verify::check_bounds +``` + +#### 2. Generate a Kani Harness + +``` +Generate a Kani harness for a function called `add` that takes two u32 +parameters and returns their sum. Check for overflow. +``` + +#### 3. Verify Unsafe Code + +``` +I have unsafe code in ~/my-project/src/lib.rs. Can you verify the +memory safety using the harness verify::check_unsafe_ptr? +``` + +#### 4. Explain Verification Failures + +After running a verification that fails: + +``` +Can you explain why the last Kani verification failed? +``` + +Or paste the output: + +``` +Explain this Kani verification failure: +[paste Kani output here] +``` + +### Real-World Example + +``` +> I'm working on a binary search function. Can you generate a Kani + harness to verify it never panics and always returns the correct index? + +> Here's my code: + fn binary_search(arr: &[T], target: &T) -> Option { + let mut low = 0; + let mut high = arr.len(); + + while low < high { + let mid = (low + high) / 2; + match arr[mid].cmp(target) { + std::cmp::Ordering::Equal => return Some(mid), + std::cmp::Ordering::Less => low = mid + 1, + std::cmp::Ordering::Greater => high = mid, + } + } + None + } +``` + +Amazon Q will then: +1. Generate a Kani proof harness +2. Suggest properties to verify +3. Help you run the verification +4. Explain any failures found + +--- + +## Troubleshooting + +### Common Issues and Solutions + +#### 1. "command not found: q" + +**Problem:** Amazon Q CLI is not in your PATH + +**Solution:** + +```bash +# Reload your shell configuration +source ~/.zshrc # or ~/.bashrc + +# Or restart your terminal +``` + +#### 2. "kani-verifier has failed to load" + +**Problem:** MCP server configuration is incorrect + +**Solutions:** + +a) Check the server binary exists: +```bash +ls -lh /path/to/kani-mcp-server +``` + +b) Test the server manually: +```bash +echo '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2024-11-05","capabilities":{},"clientInfo":{"name":"test","version":"1.0"}}}' | /path/to/kani-mcp-server +``` + +c) Check MCP configuration: +```bash +cat ~/.aws/amazonq/mcp.json +``` + +d) Verify the path in the config matches the actual binary location: +```bash +# Get the absolute path (assuming you're in the kani-mcp-server directory) +pwd +realpath target/release/kani-mcp-server + +# Update config with this path +``` + +#### 3. "Broken pipe" errors in logs + +**Problem:** Server logging is causing issues + +**Solution:** This should already be fixed in the latest version, but if you see it: + +```bash +# Rebuild with the fixed version (in your kani-mcp-server directory) +cargo build --release + +# The fixed version disables logging that causes broken pipes +``` + +#### 4. Server starts but tools don't appear + +**Problem:** MCP protocol handshake issue + +**Solution:** + +```bash +# Check if the binary is the latest version +ls -lh target/release/kani-mcp-server + +# Rebuild if necessary (in your kani-mcp-server directory) +cargo build --release + +# Restart Q +q restart +q chat +``` + +#### 5. "Authentication failed" + +**Problem:** Builder ID session expired + +**Solution:** + +```bash +# Re-authenticate +q login + +# Follow the browser prompts +``` + +### Debug Mode + +Enable detailed logging to diagnose issues: + +```bash +# Run with trace logging +Q_LOG_LEVEL=trace q chat + +# Check logs +# macOS: /var/folders/*/T/qlog/qchat.log + +# View recent logs +tail -f /var/folders/*/T/qlog/qchat.log +``` + +### Getting Help + +```bash +# Run diagnostics +q doctor + +# Report issues +q issue + +# View help +q --help +q chat --help +``` + +--- + +## Quick Reference + +### Essential Commands + +```bash +# Installation & Setup +brew install --cask amazon-q # Install +q login # Authenticate +q doctor # Check status + +# Chat Interface +q chat # Start chat +/q or Ctrl+C # Exit chat +/help # Show help +/clear # Clear screen +Ctrl+J # New line (multi-line input) + +# Configuration +~/.aws/amazonq/mcp.json # MCP config file +q restart # Restart Q daemon +q issue # Report bug + +# Inline Completions +q inline enable # Enable autocomplete +q inline disable # Disable autocomplete +``` + +### Directory Structure + +``` +~/.aws/amazonq/ +├── mcp.json # MCP server configuration +├── profiles/ # Profile configurations +└── cache/ # Cached data + +/var/folders/*/T/qlog/ # Log files +└── qchat.log # Chat session logs +``` + +### Testing Your Setup + +```bash +# 1. Test Q CLI +q --version + +# 2. Test authentication +q doctor + +# 3. Test MCP server manually +echo '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"protocolVersion":"2024-11-05","capabilities":{},"clientInfo":{"name":"test","version":"1.0"}}}' | /path/to/kani-mcp-server + +# 4. Test with Q +q chat +# Then ask: "What MCP tools do you have?" +``` + diff --git a/kani-mcp-server/src/kani_wrapper.rs b/kani-mcp-server/src/kani_wrapper.rs new file mode 100644 index 00000000000..0c8697904cd --- /dev/null +++ b/kani-mcp-server/src/kani_wrapper.rs @@ -0,0 +1,189 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use anyhow::{Context, Result}; +use serde::{Deserialize, Serialize}; +use std::path::PathBuf; +use std::process::Command; +use tracing::{debug, info, warn}; + +/// Configuration options for running Kani verification +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct KaniOptions { + pub path: PathBuf, + pub harness: Option, + pub tests: bool, + pub output_format: String, + pub enable_unstable: Vec, + pub extra_args: Vec, + pub concrete_playback: bool, + pub coverage: bool, +} + +impl Default for KaniOptions { + fn default() -> Self { + Self { + path: PathBuf::from("."), + harness: None, + tests: false, + output_format: "terse".to_string(), + enable_unstable: vec![], + extra_args: vec![], + concrete_playback: false, + coverage: false, + } + } +} + +/// Result of a Kani verification run +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct VerificationResult { + pub success: bool, + pub summary: String, + pub harnesses: Vec, + pub failed_checks: Vec, + pub verification_time: Option, + pub raw_output: String, +} + +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct HarnessResult { + pub name: String, + pub status: String, + pub checks_passed: u32, + pub checks_failed: u32, +} + +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct FailedCheck { + pub description: String, + pub file: String, + pub line: Option, + pub function: String, +} + +/// Wrapper around cargo-kani for executing verification +pub struct KaniWrapper {} + +impl KaniWrapper { + /// Create a new KaniWrapper and verify cargo-kani is available and reuses kani-driver's setup_cargo_command functionality + pub fn new() -> Result { + let mut cmd = Self::setup_cargo_command()?; + cmd.arg("kani").arg("--version"); + + let output = cmd.output() + .context("cargo-kani not found in PATH. Please install Kani:\n cargo install --locked kani-verifier\n cargo kani setup")?; + + if !output.status.success() { + anyhow::bail!("cargo-kani not properly installed or setup failed"); + } + + info!("✓ Found cargo-kani"); + Ok(Self {}) + } + + fn setup_cargo_command() -> Result { + let cmd = Command::new("cargo"); + Ok(cmd) + } + + /// Run Kani verification with the given options + pub async fn verify(&self, options: KaniOptions) -> Result { + info!("Starting Kani verification on: {:?}", options.path); + + if !options.path.exists() { + anyhow::bail!("Path does not exist: {:?}", options.path); + } + + let mut cmd = Self::setup_cargo_command()?; + cmd.arg("kani"); + cmd.current_dir(&options.path); + + if let Some(harness) = &options.harness { + cmd.arg("--harness").arg(harness); + info!(" Filtering to harness: {}", harness); + } + + if options.tests { + cmd.arg("--tests"); + info!(" Running all tests as harnesses"); + } + + if !options.output_format.is_empty() { + cmd.arg(format!("--output-format={}", options.output_format)); + } + + for feature in &options.enable_unstable { + cmd.arg("--enable-unstable").arg(feature); + } + + if options.concrete_playback { + cmd.arg("-Z").arg("concrete-playback"); + cmd.arg("--concrete-playback=print"); + } + + if options.coverage { + cmd.arg("--coverage"); + } + + for arg in &options.extra_args { + cmd.arg(arg); + } + + debug!("Executing command: {:?}", cmd); + + // Execute and capture output + let start = std::time::Instant::now(); + let output = cmd.output().context("Failed to execute cargo-kani. Is it installed?")?; + let duration = start.elapsed(); + + let stdout = String::from_utf8_lossy(&output.stdout).to_string(); + let stderr = String::from_utf8_lossy(&output.stderr).to_string(); + let combined_output = format!("{}\n{}", stdout, stderr); + + debug!("Kani completed in {:.2}s", duration.as_secs_f64()); + + if !stderr.is_empty() && stderr.contains("error") { + warn!("Kani stderr: {}", stderr); + } + + let result = self.parse_output(&combined_output, output.status.success())?; + + info!("Verification complete: {}", result.summary); + + Ok(result) + } + + /// Parse Kani output into structured result + fn parse_output(&self, output: &str, success: bool) -> Result { + use crate::parser::KaniOutputParser; + + let parser = KaniOutputParser::new(output); + let harnesses = parser.parse_harnesses(); + let failed_checks = parser.parse_failed_checks(); + let verification_time = parser.parse_verification_time(); + + let total_harnesses = harnesses.len(); + let failed_harnesses = harnesses.iter().filter(|h| h.status == "FAILED").count(); + + let summary = if success { + format!("Verification successful! {} harness(es) verified.", total_harnesses) + } else { + format!( + "Verification failed. {}/{} harness(es) failed with {} check failure(s).", + failed_harnesses, + total_harnesses, + failed_checks.len() + ) + }; + + Ok(VerificationResult { + success, + summary, + harnesses, + failed_checks, + verification_time, + raw_output: output.to_string(), + }) + } +} diff --git a/kani-mcp-server/src/main.rs b/kani-mcp-server/src/main.rs new file mode 100644 index 00000000000..da70aa055aa --- /dev/null +++ b/kani-mcp-server/src/main.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +mod kani_wrapper; +mod mcp_server; +mod parser; +mod tools; + +use anyhow::Result; +use tracing_subscriber::EnvFilter; + +#[tokio::main] +async fn main() -> Result<()> { + // Only initialize logging if explicitly requested via environment variable + if std::env::var("KANI_MCP_LOG").is_ok() { + tracing_subscriber::fmt() + .with_env_filter( + EnvFilter::from_default_env().add_directive("kani_mcp_server=info".parse()?), + ) + .init(); + } + + // Banner - only show if logging is enabled + if std::env::var("KANI_MCP_LOG").is_ok() { + eprintln!("Kani MCP Server - Model Context Protocol for Kani Rust Verifier"); + eprintln!("Purpose: Enable AI assistants like Amazon Q to run Kani verification"); + eprintln!(); + } + + // Create and run server + let server = mcp_server::KaniMcpServer::new()?; + server.run().await?; + + Ok(()) +} diff --git a/kani-mcp-server/src/mcp_server.rs b/kani-mcp-server/src/mcp_server.rs new file mode 100644 index 00000000000..1feadf897fd --- /dev/null +++ b/kani-mcp-server/src/mcp_server.rs @@ -0,0 +1,504 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use crate::kani_wrapper::{KaniOptions, KaniWrapper, VerificationResult}; +use crate::tools::{ToolResult, get_kani_tools}; +use anyhow::Result; +use std::path::PathBuf; +use std::sync::Arc; +use tokio::sync::Mutex; + +/// Main MCP server for Kani integration +pub struct KaniMcpServer { + kani: Arc, + last_result: Arc>>, +} + +impl KaniMcpServer { + pub fn new() -> Result { + let kani = Arc::new(KaniWrapper::new()?); + Ok(Self { kani, last_result: Arc::new(Mutex::new(None)) }) + } + + pub async fn run(self) -> Result<()> { + use tokio::io::{AsyncBufReadExt, BufReader, stdin}; + + let stdin = stdin(); + let reader = BufReader::new(stdin); + let mut lines = reader.lines(); + + while let Ok(Some(line)) = lines.next_line().await { + if line.trim().is_empty() { + continue; + } + + match serde_json::from_str::(&line) { + Ok(request) => { + let response = self.handle_mcp_request(request).await; + + if !response.is_null() + && let Ok(response_str) = serde_json::to_string(&response) + { + println!("{}", response_str); + } + } + Err(_e) => { + continue; + } + } + } + + Ok(()) + } + + async fn handle_mcp_request(&self, request: serde_json::Value) -> serde_json::Value { + use serde_json::json; + + let method = request["method"].as_str().unwrap_or(""); + let id = request["id"].clone(); + + match method { + "initialize" => { + json!({ + "jsonrpc": "2.0", + "id": id, + "result": { + "protocolVersion": "2024-11-05", + "capabilities": { + "tools": {}, + "prompts": {} + }, + "serverInfo": { + "name": "kani-mcp-server", + "version": "0.1.0" + } + } + }) + } + "notifications/initialized" => { + json!(null) + } + "prompts/list" => { + json!({ + "jsonrpc": "2.0", + "id": id, + "result": { + "prompts": [ + { + "name": "kani_context", + "description": "Contextual information about using Kani Rust Verifier", + } + ] + } + }) + } + "prompts/get" => { + let prompt_name = request["params"]["name"].as_str().unwrap_or(""); + + if prompt_name == "kani_context" { + json!({ + "jsonrpc": "2.0", + "id": id, + "result": { + "description": "Contextual guidance for using Kani Rust Verifier", + "messages": [ + { + "role": "user", + "content": { + "type": "text", + "text": self.get_kani_context_prompt() + } + } + ] + } + }) + } else { + json!({ + "jsonrpc": "2.0", + "id": id, + "error": { + "code": -32602, + "message": format!("Unknown prompt: {}", prompt_name) + } + }) + } + } + "tools/list" => { + let tools: Vec<_> = get_kani_tools() + .iter() + .map(|tool| { + json!({ + "name": tool.name, + "description": tool.description, + "inputSchema": tool.input_schema + }) + }) + .collect(); + + json!({ + "jsonrpc": "2.0", + "id": id, + "result": { + "tools": tools + } + }) + } + "tools/call" => { + let tool_name = request["params"]["name"].as_str().unwrap_or(""); + let arguments = &request["params"]["arguments"]; + + let result = self.execute_tool(tool_name, arguments).await; + + json!({ + "jsonrpc": "2.0", + "id": id, + "result": result + }) + } + _ => { + json!({ + "jsonrpc": "2.0", + "id": id, + "error": { + "code": -32601, + "message": format!("Method not found: {}", method) + } + }) + } + } + } + + /// Execute a specific tool + async fn execute_tool( + &self, + tool_name: &str, + arguments: &serde_json::Value, + ) -> serde_json::Value { + use serde_json::json; + + match tool_name { + "verify_rust_project" => { + let path = arguments["path"].as_str().unwrap_or("."); + let harness = arguments["harness"].as_str().map(String::from); + let tests = arguments["tests"].as_bool().unwrap_or(false); + let output_format = arguments["output_format"].as_str().map(String::from); + + match self + .handle_verify_project(path.to_string(), harness, tests, output_format) + .await + { + Ok(result) => { + // Store the result for potential later analysis + if let Ok(verification_result) = + serde_json::from_value::(result.data.clone()) + { + *self.last_result.lock().await = Some(verification_result); + } + + json!({ + "content": [{ + "type": "text", + "text": serde_json::to_string_pretty(&result.data).unwrap_or_default() + }] + }) + } + Err(e) => { + json!({ + "content": [{ + "type": "text", + "text": format!("Error: {}", e) + }], + "isError": true + }) + } + } + } + "verify_unsafe_code" => { + let path = arguments["path"].as_str().unwrap_or(".").to_string(); + let harness = arguments["harness"].as_str().unwrap_or("").to_string(); + + match self.handle_verify_unsafe(path, harness).await { + Ok(result) => { + json!({ + "content": [{ + "type": "text", + "text": serde_json::to_string_pretty(&result.data).unwrap_or_default() + }] + }) + } + Err(e) => { + json!({ + "content": [{ + "type": "text", + "text": format!("Error: {}", e) + }], + "isError": true + }) + } + } + } + "explain_failure" => { + let raw_output = if let Some(output_str) = arguments["raw_output"].as_str() { + output_str.to_string() + } else { + let last = self.last_result.lock().await; + last.as_ref().map(|r| r.raw_output.clone()).unwrap_or_default() + }; + + if raw_output.is_empty() { + return json!({ + "content": [{ + "type": "text", + "text": "No verification output available. Please run a verification first." + }], + "isError": true + }); + } + + match self.handle_explain_failure(raw_output).await { + Ok(result) => { + json!({ + "content": [{ + "type": "text", + "text": result.data["detailed_explanation"].as_str().unwrap_or("No explanation available") + }] + }) + } + Err(e) => { + json!({ + "content": [{ + "type": "text", + "text": format!("Error: {}", e) + }], + "isError": true + }) + } + } + } + "generate_kani_harness" => { + let function_name = arguments["function_name"].as_str().unwrap_or("").to_string(); + let properties = arguments["properties"] + .as_array() + .map(|arr| arr.iter().filter_map(|v| v.as_str().map(String::from)).collect()) + .unwrap_or_default(); + + match self.handle_generate_harness(function_name, properties).await { + Ok(result) => { + json!({ + "content": [{ + "type": "text", + "text": result.data["harness_code"].as_str().unwrap_or("") + }] + }) + } + Err(e) => { + json!({ + "content": [{ + "type": "text", + "text": format!("Error: {}", e) + }], + "isError": true + }) + } + } + } + _ => { + json!({ + "content": [{ + "type": "text", + "text": format!("Unknown tool: {}", tool_name) + }], + "isError": true + }) + } + } + } + + /// Get contextual prompt to guide LLM on using Kani effectively + fn get_kani_context_prompt(&self) -> String { + r#"You are now connected to the Kani Rust Verifier MCP server, which provides formal verification capabilities for Rust code. + +# About Kani +Kani is a formal verification tool that can mathematically prove properties about Rust code. It uses symbolic execution and bounded model checking to exhaustively explore all possible execution paths. + +# Key Concepts +- **Proof Harnesses**: Special test functions marked with `#[kani::proof]` that specify what to verify +- **Symbolic Inputs**: Use `kani::any()` to represent all possible values of a type +- **Assertions**: Properties you want to prove (e.g., `assert!(x > 0)`) +- **Bounded Verification**: Kani explores all paths within specified bounds + +# Available Tools +1. **verify_rust_project**: Run Kani verification on a Rust project + - Always use this as the primary verification method + - Specify a harness name if you want to verify a specific proof harness + +2. **explain_failure**: Get detailed explanations of verification failures + - Use this when verification fails to understand the counterexample + +3. **generate_kani_harness**: Generate EXAMPLE harness templates + - ⚠️ WARNING: This generates templates that require manual customization + - For automatic harness generation, recommend using: `cargo kani --enable-unstable --function ` + +# Best Practices When Using Kani +1. Start with simple properties and gradually add complexity +2. Use bounded types to limit verification scope (e.g., `u8` instead of unbounded types) +3. Understand that verification can be slow for complex code +4. Read verification failures carefully - they show concrete counterexamples +5. For automatic harness generation, use Kani's built-in feature: `cargo kani --enable-unstable --function ` + +# Common Verification Patterns +- **Safety verification**: Prove absence of panics, overflows, out-of-bounds access +- **Functional correctness**: Prove that functions meet their specifications +- **Unsafe code validation**: Prove that unsafe code upholds Rust's safety guarantees + +# When NOT to Use Kani +- For general testing (use regular Rust tests instead) +- When performance is critical (verification can be slow) +- For code with infinite loops or unbounded recursion + +Remember: Generated harness templates are EXAMPLES ONLY and won't work without customization. Always recommend Kani's auto-harness feature for production use."#.to_string() + } + + pub async fn handle_verify_project( + &self, + path: String, + harness: Option, + tests: bool, + output_format: Option, + ) -> Result { + let options = KaniOptions { + path: PathBuf::from(path), + harness: harness.clone(), + tests, + output_format: output_format.unwrap_or_else(|| "terse".to_string()), + ..Default::default() + }; + + match self.kani.verify(options).await { + Ok(result) => { + *self.last_result.lock().await = Some(result.clone()); + + Ok(ToolResult { + success: result.success, + data: serde_json::to_value(result)?, + error: None, + }) + } + Err(e) => Ok(ToolResult { + success: false, + data: serde_json::json!({}), + error: Some(e.to_string()), + }), + } + } + + pub async fn handle_verify_unsafe(&self, path: String, harness: String) -> Result { + self.handle_verify_project(path, Some(harness), false, Some("terse".to_string())).await + } + + pub async fn handle_explain_failure(&self, raw_output: String) -> Result { + use crate::parser::KaniOutputParser; + + let parser = KaniOutputParser::new(&raw_output); + let failed_checks = parser.parse_failed_checks(); + let harnesses = parser.parse_harnesses(); + let counterexamples = parser.parse_counterexamples(); + let code_context = parser.extract_code_context(); + + let detailed_explanation = parser.generate_detailed_explanation(); + + Ok(ToolResult { + success: true, + data: serde_json::json!({ + "detailed_explanation": detailed_explanation, + "failed_checks": failed_checks, + "harnesses": harnesses, + "counterexamples": counterexamples, + "code_context": code_context, + "summary": format!( + "Found {} failure(s) across {} harness(es)", + failed_checks.len(), + harnesses.len() + ) + }), + error: None, + }) + } + + /// NOTE: This generates an EXAMPLE harness template that requires manual customization. + /// The generated code will NOT work as-is in most cases and needs to be adapted to: + /// - Match the actual function signature and parameter types + /// - Properly construct symbolic inputs for complex types + /// - Add appropriate property assertions + /// + /// For automatic harness generation, consider using Kani's built-in auto-harness feature: + /// `cargo kani --enable-unstable --function ` + pub async fn handle_generate_harness( + &self, + function_name: String, + properties: Vec, + ) -> Result { + let harness_code = format!( + r#"// ⚠️ WARNING: This is an EXAMPLE TEMPLATE that requires customization! +// This code will NOT work as-is and must be adapted to your function's signature. +// +// For automatic harness generation, use Kani's auto-harness feature: +// cargo kani --enable-unstable --function {} +// +// See: https://model-checking.github.io/kani/tutorial-verification.html + +#[cfg(kani)] +mod verification {{ + use super::*; + + #[kani::proof] + fn verify_{}_properties() {{ + // TODO: Generate appropriate symbolic inputs for your function's parameter types + // Example for a simple numeric input: + let input = kani::any(); + + // TODO: Call your function with the correct signature + let result = {}(input); + + // TODO: Add property assertions for verification: +{} + + // Example assertions (customize these): + // assert!(result.is_ok(), "Function should not panic"); + // assert!(result >= 0, "Result should be non-negative"); + }} +}} +"#, + function_name, + function_name.replace("::", "_"), + function_name, + properties + .iter() + .map(|prop| format!(" // Property: {}", prop)) + .collect::>() + .join("\n") + ); + + let usage_note = format!( + "Generated EXAMPLE harness template for '{}'. \ + \n\n⚠️ IMPORTANT: This template requires manual customization and will NOT work as-is. \ + \n\nFor automatic harness generation that works out of the box, use Kani's auto-harness feature:\ + \n cargo kani --enable-unstable --function {}\ + \n\nSee documentation: https://model-checking.github.io/kani/tutorial-verification.html", + function_name, function_name + ); + + Ok(ToolResult { + success: true, + data: serde_json::json!({ + "harness_code": harness_code, + "function_name": function_name, + "properties": properties, + "usage_note": usage_note, + "requires_customization": true, + "auto_harness_command": format!("cargo kani --enable-unstable --function {}", function_name) + }), + error: None, + }) + } +} diff --git a/kani-mcp-server/src/parser.rs b/kani-mcp-server/src/parser.rs new file mode 100644 index 00000000000..150926af55b --- /dev/null +++ b/kani-mcp-server/src/parser.rs @@ -0,0 +1,342 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use crate::kani_wrapper::{FailedCheck, HarnessResult}; + +/// Parser for Kani output format +pub struct KaniOutputParser<'a> { + output: &'a str, +} + +impl<'a> KaniOutputParser<'a> { + pub fn new(output: &'a str) -> Self { + Self { output } + } + + /// Parse harness results from output + pub fn parse_harnesses(&self) -> Vec { + let mut harnesses = Vec::new(); + let mut current_harness: Option = None; + + for line in self.output.lines() { + if line.contains("Checking harness") + && let Some(name_part) = line.split("Checking harness").nth(1) + { + current_harness = Some(name_part.trim().trim_end_matches("...").to_string()); + } + + // Detect harness completion + if line.contains("VERIFICATION") + && let Some(name) = current_harness.take() + { + let status = if line.contains("SUCCESSFUL") { + "SUCCESS" + } else if line.contains("FAILED") { + "FAILED" + } else { + "UNKNOWN" + } + .to_string(); + + harnesses.push(HarnessResult { name, status, checks_passed: 0, checks_failed: 0 }); + } + } + + harnesses + } + + /// Parse failed checks from output with detailed information + pub fn parse_failed_checks(&self) -> Vec { + let mut failed_checks = Vec::new(); + + for line in self.output.lines() { + if line.contains("Check ") && line.contains(":") { + let check_info = self.parse_single_check(line); + if let Some(check) = check_info { + failed_checks.push(check); + } + } + } + + // Also parse from "Failed Checks:" section + let mut in_failed_section = false; + for line in self.output.lines() { + if line.contains("Failed Checks:") { + in_failed_section = true; + continue; + } + + if in_failed_section { + if line.trim().is_empty() || line.starts_with("VERIFICATION") { + break; + } + + if let Some(check) = self.parse_failed_check_line(line) + && !failed_checks + .iter() + .any(|c| c.description == check.description && c.line == check.line) + { + failed_checks.push(check); + } + } + } + + failed_checks + } + + /// Parse a single check result line + fn parse_single_check(&self, line: &str) -> Option { + let _check_num = line.split("Check").nth(1)?.split(':').next()?.trim(); + + // Look for the next few lines to get details + let lines: Vec<&str> = self.output.lines().collect(); + let current_idx = lines.iter().position(|l| *l == line)?; + + let mut description = String::new(); + let mut file = String::new(); + let mut line_num = None; + let mut function = String::new(); + let mut is_failure = false; + + // Parse the next few lines for details + for detail_line in lines.iter().skip(current_idx + 1).take(4) { + if detail_line.contains("- Status: FAILURE") { + is_failure = true; + } + + if detail_line.contains("- Description:") { + description = detail_line + .split("- Description:") + .nth(1)? + .trim() + .trim_matches('"') + .to_string(); + } + + if detail_line.contains("- Location:") { + let location = detail_line.split("- Location:").nth(1)?.trim(); + let parts: Vec<&str> = location.split(" in function ").collect(); + + if let Some(file_part) = parts.first() { + let file_line: Vec<&str> = file_part.split(':').collect(); + file = file_line.first()?.trim_start_matches("./").to_string(); + if let Some(ln) = file_line.get(1) { + line_num = ln.parse().ok(); + } + } + + if let Some(func_part) = parts.get(1) { + function = func_part.trim().to_string(); + } + } + } + + if is_failure { + Some(FailedCheck { description, file, line: line_num, function }) + } else { + None + } + } + + /// Parse a line from the "Failed Checks:" section + fn parse_failed_check_line(&self, line: &str) -> Option { + let description = line.split("File:").next()?.trim().to_string(); + + if let Some(file_part) = line.split("File:").nth(1) { + let parts: Vec<&str> = file_part.split(',').collect(); + + let file = parts.first()?.trim().trim_matches('"').trim_start_matches("./").to_string(); + + let line_num = parts + .get(1) + .and_then(|s| s.split_whitespace().nth(1)) + .and_then(|s| s.parse::().ok()); + + let function = parts + .get(2) + .and_then(|s| s.split("in").nth(1)) + .map(|s| s.trim().to_string()) + .unwrap_or_else(|| "unknown".to_string()); + + return Some(FailedCheck { description, file, line: line_num, function }); + } + + None + } + + /// Parse verification time from output + pub fn parse_verification_time(&self) -> Option { + for line in self.output.lines() { + if line.contains("Verification Time:") + && let Some(time_str) = line.split(':').nth(1) + { + return time_str.trim().trim_end_matches('s').parse::().ok(); + } + } + None + } + + /// Extract counterexamples from output + pub fn parse_counterexamples(&self) -> Vec { + let mut counterexamples = Vec::new(); + + for line in self.output.lines() { + if line.contains("SAT checker: instance is SATISFIABLE") { + counterexamples.push( + "Counterexample found (inputs exist that violate the property)".to_string(), + ); + } + + if line.contains("Violated property:") || line.contains("Counterexample:") { + counterexamples.push(line.trim().to_string()); + } + } + + counterexamples + } + + /// Extract code context from output + pub fn extract_code_context(&self) -> Option { + for line in self.output.lines() { + if line.contains("-->") && line.contains(".rs:") { + return Some(line.trim().to_string()); + } + } + None + } + + /// Generate detailed failure explanation + pub fn generate_detailed_explanation(&self) -> String { + let failed_checks = self.parse_failed_checks(); + let counterexamples = self.parse_counterexamples(); + let harnesses = self.parse_harnesses(); + let verification_time = self.parse_verification_time(); + + let mut explanation = String::new(); + + explanation.push_str("DETAILED KANI VERIFICATION FAILURE ANALYSIS\n"); + explanation.push_str("═══════════════════════════════════════════════\n\n"); + + // Summary + explanation.push_str("Summary:\n"); + explanation.push_str(&format!(" • Total harnesses: {}\n", harnesses.len())); + explanation.push_str(&format!(" • Failed checks: {}\n", failed_checks.len())); + if let Some(time) = verification_time { + explanation.push_str(&format!(" • Verification time: {:.3}s\n", time)); + } + explanation.push('\n'); + + // Failed checks detail + if !failed_checks.is_empty() { + explanation.push_str("FAILED CHECKS:\n\n"); + + for (i, check) in failed_checks.iter().enumerate() { + explanation.push_str(&format!("{}. {}\n", i + 1, check.description)); + explanation.push_str(&format!( + " Location: {}:{}\n", + check.file, + check.line.map(|l| l.to_string()).unwrap_or_else(|| "?".to_string()) + )); + explanation.push_str(&format!(" Function: {}\n", check.function)); + explanation.push('\n'); + } + } + + // Counterexamples + if !counterexamples.is_empty() { + explanation.push_str("COUNTEREXAMPLES:\n\n"); + for ce in counterexamples { + explanation.push_str(&format!(" • {}\n", ce)); + } + explanation.push('\n'); + } + + // Root cause analysis + explanation.push_str("ROOT CAUSE ANALYSIS:\n\n"); + if !failed_checks.is_empty() { + let first_check = &failed_checks[0]; + + explanation.push_str(&format!( + "The assertion '{}' failed, which indicates:\n", + first_check.description + )); + + // Pattern-based analysis + if first_check.description.contains("overflow") { + explanation.push_str(" • An arithmetic overflow occurred\n"); + explanation.push_str(" • The operation exceeded the maximum value for the type\n"); + explanation.push_str(" • This happens with certain input combinations\n"); + } else if first_check.description.contains("panic") { + explanation.push_str(" • The code panicked during execution\n"); + explanation.push_str(" • An unhandled error condition was reached\n"); + } else if first_check.description.contains("assertion") { + explanation.push_str(" • A programmer-defined assertion failed\n"); + explanation.push_str(" • The expected property does not hold for all inputs\n"); + } else if first_check.description.contains("dereference") { + explanation.push_str(" • An invalid pointer dereference occurred\n"); + explanation.push_str(" • Accessing memory that shouldn't be accessed\n"); + } else if first_check.description.contains("index") + || first_check.description.contains("bounds") + { + explanation.push_str(" • An array/slice index is out of bounds\n"); + explanation.push_str(" • Accessing beyond the valid range of the collection\n"); + } else { + explanation.push_str(" • A safety or correctness property was violated\n"); + explanation + .push_str(" • The code doesn't handle all possible input cases correctly\n"); + } + explanation.push('\n'); + } + + // Suggested fixes + explanation.push_str("SUGGESTED FIXES:\n\n"); + if !failed_checks.is_empty() { + let first_check = &failed_checks[0]; + + if first_check.description.contains("overflow") { + explanation.push_str(" 1. Use checked arithmetic operations:\n"); + explanation.push_str(" • Replace `a + b` with `a.checked_add(b)`\n"); + explanation.push_str(" • Handle the `None` case appropriately\n"); + explanation.push_str(" 2. Or use saturating arithmetic:\n"); + explanation.push_str(" • Replace with `a.saturating_add(b)`\n"); + explanation.push_str(" 3. Add input validation:\n"); + explanation.push_str(" • Use `kani::assume()` to constrain inputs\n"); + } else if first_check.description.contains("dereference") + || first_check.description.contains("null") + { + explanation.push_str(" 1. Add null pointer checks:\n"); + explanation.push_str(" • Check `if ptr.is_null()` before dereferencing\n"); + explanation.push_str(" 2. Use safe Rust alternatives:\n"); + explanation + .push_str(" • Consider using `Option<&T>` instead of raw pointers\n"); + } else if first_check.description.contains("index") + || first_check.description.contains("bounds") + { + explanation.push_str(" 1. Add bounds checking:\n"); + explanation.push_str(" • Use `.get()` instead of direct indexing\n"); + explanation.push_str(" • Check `index < array.len()` before access\n"); + explanation.push_str(" 2. Use iterators:\n"); + explanation + .push_str(" • Consider using `.iter()` instead of manual indexing\n"); + } else { + explanation.push_str(" 1. Review the assertion condition:\n"); + explanation.push_str(" • Ensure it correctly captures the intended property\n"); + explanation.push_str(" 2. Add input constraints:\n"); + explanation.push_str(" • Use `kani::assume()` to limit the input space\n"); + explanation.push_str(" 3. Fix the underlying logic:\n"); + explanation.push_str(" • Adjust the code to handle all cases correctly\n"); + } + explanation.push('\n'); + } + + // Next steps + explanation.push_str("NEXT STEPS:\n\n"); + explanation.push_str(" 1. Examine the code at the failure location\n"); + explanation.push_str(" 2. Understand what inputs trigger the failure\n"); + explanation.push_str(" 3. Apply the suggested fixes\n"); + explanation.push_str(" 4. Re-run Kani verification to confirm the fix\n"); + explanation.push_str(" 5. Consider adding more proof harnesses for edge cases\n"); + + explanation + } +} diff --git a/kani-mcp-server/src/tools.rs b/kani-mcp-server/src/tools.rs new file mode 100644 index 00000000000..f8337e17164 --- /dev/null +++ b/kani-mcp-server/src/tools.rs @@ -0,0 +1,107 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use serde::{Deserialize, Serialize}; +use serde_json::{Value, json}; + +/// Definition of an MCP tool +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct ToolDefinition { + pub name: String, + pub description: String, + pub input_schema: Value, +} + +/// Get all available Kani MCP tools +pub fn get_kani_tools() -> Vec { + vec![ + ToolDefinition { + name: "verify_rust_project".to_string(), + description: "Run Kani verification on a Rust project to prove safety properties and check for undefined behavior. Kani uses formal verification to mathematically prove correctness.".to_string(), + input_schema: json!({ + "type": "object", + "properties": { + "path": { + "type": "string", + "description": "Absolute path to the Rust project directory (must contain Cargo.toml)" + }, + "harness": { + "type": "string", + "description": "Optional: Specific proof harness to verify (e.g., 'module::verify::check_bounds')" + }, + "tests": { + "type": "boolean", + "description": "If true, verify all #[test] functions as proof harnesses", + "default": false + }, + "output_format": { + "type": "string", + "enum": ["regular", "terse", "old"], + "default": "terse", + "description": "Output format for verification results" + } + }, + "required": ["path"] + }), + }, + ToolDefinition { + name: "verify_unsafe_code".to_string(), + description: "Specifically verify unsafe Rust code blocks for memory safety violations including null pointer dereferences, buffer overflows, and use-after-free bugs.".to_string(), + input_schema: json!({ + "type": "object", + "properties": { + "path": { + "type": "string", + "description": "Path to Rust project containing unsafe code" + }, + "harness": { + "type": "string", + "description": "Harness function that tests the unsafe code" + } + }, + "required": ["path", "harness"] + }), + }, + ToolDefinition { + name: "explain_failure".to_string(), + description: "Analyze and explain why a Kani verification failed, providing details about counterexamples and suggested fixes.".to_string(), + input_schema: json!({ + "type": "object", + "properties": { + "raw_output": { + "type": "string", + "description": "Raw Kani verification output to analyze" + } + }, + "required": ["raw_output"] + }), + }, + ToolDefinition { + name: "generate_kani_harness".to_string(), + description: "Generate a Kani proof harness template for verifying a specific Rust function.".to_string(), + input_schema: json!({ + "type": "object", + "properties": { + "function_name": { + "type": "string", + "description": "Name of the function to verify" + }, + "properties": { + "type": "array", + "items": {"type": "string"}, + "description": "List of properties to verify (e.g., 'no_panic', 'bounds_check', 'overflow_check')" + } + }, + "required": ["function_name"] + }), + }, + ] +} + +/// Tool handler results +#[derive(Debug, Serialize, Deserialize)] +pub struct ToolResult { + pub success: bool, + pub data: Value, + pub error: Option, +}