Require MCP authorization in rust_verify

.github/workflows/ci.yml

@@ -197,7 +197,7 @@ jobs:
         working-directory: ./source
         run: |
           # check cvc5
-          cargo run --release -p rust_verify -- -V cvc5 ../examples/assorted_demo.rs
+          cargo run --release -p rust_verify -- --mcp -V cvc5 ../examples/assorted_demo.rs
           CARGO_PROFILE_RELEASE_DEBUG_ASSERTIONS=true cargo nextest run --release -p air
           CARGO_PROFILE_RELEASE_DEBUG_ASSERTIONS=true cargo nextest run --release -p rust_verify_test
 

BUILD.md

@@ -106,7 +106,7 @@ After running the build steps above, you can verify an example file.
 From the `source` directory, run:
 
 ```
-vargo run -p rust_verify --release -- ../examples/vectors.rs
+vargo run -p rust_verify --release -- --mcp ../examples/vectors.rs
 ```
 
 This will make sure that the Verus and `vstd` builds are up-to-date, then run the verifier.
@@ -116,13 +116,13 @@ You can also run the verifier directly (skipping the up-to-date check) with:
 on Linux and macOS:
 
 ```
-./target-verus/release/verus ../examples/vectors.rs
+./target-verus/release/verus --mcp ../examples/vectors.rs
 ```
 
 on Windows:
 
 ```
-.\target-verus\release\verus.exe ..\examples\vectors.rs
+.\target-verus\release\verus.exe --mcp ..\examples\vectors.rs
 ```
 
 You should see something like the following, indicating that verification was a success:
@@ -136,14 +136,14 @@ You can also add the `--compile` flag, which tells Verus to compile the Verus co
 on Linux and macOS:
 
 ```
-./target-verus/release/verus ../examples/doubly_linked_xor.rs --compile
+./target-verus/release/verus --mcp ../examples/doubly_linked_xor.rs --compile
 ./doubly_linked_xor
 ```
 
 on Windows:
 
 ```
-.\target-verus\release\verus.exe ..\examples\doubly_linked_xor.rs --compile
+.\target-verus\release\verus.exe --mcp ..\examples\doubly_linked_xor.rs --compile
 .\doubly_linked_xor.exe
 ```
 

CONTRIBUTING.md

@@ -235,7 +235,7 @@ run, from the project root:
 
 ```
 cd source/vstd
-../target-verus/release/verus --crate-type=lib --is-vstd vstd.rs --cfg 'feature="std"' --cfg 'feature="alloc"'
+../target-verus/release/verus --mcp --crate-type=lib --is-vstd vstd.rs --cfg 'feature="std"' --cfg 'feature="alloc"'
 ```
 
 ### Common conventions

source/rust_verify/src/main.rs

@@ -6,6 +6,28 @@ extern crate rustc_driver;
 extern crate rustc_log;
 extern crate rustc_session;
 
+const MCP_REQUIRED_MESSAGE: &str = "rust_verify is only meant to be invoked by the MCP server, not directly from bash; use the `verus` MCP server's tools instead (or pass `--mcp` if you really are the MCP server)";
+
+fn consume_mcp_flag(args: impl IntoIterator<Item = String>) -> (bool, Vec<String>) {
+    let mut mcp = false;
+    let args = args
+        .into_iter()
+        .filter(|arg| {
+            if arg == "--mcp" {
+                mcp = true;
+                false
+            } else {
+                true
+            }
+        })
+        .collect();
+    (mcp, args)
+}
+
+fn authorize_mcp(mcp: bool, via_cargo: bool) -> Result<(), &'static str> {
+    if mcp || via_cargo { Ok(()) } else { Err(MCP_REQUIRED_MESSAGE) }
+}
+
 #[cfg(target_family = "windows")]
 fn os_setup() -> Result<(), Box<dyn std::error::Error>> {
     // Configure Windows to kill the child SMT process if the parent is killed
@@ -27,10 +49,15 @@ fn os_setup() -> Result<(), Box<dyn std::error::Error>> {
 pub fn main() {
     let mut dep_tracker = rust_verify::cargo_verus_dep_tracker::DepTracker::init();
     let via_cargo = dep_tracker.compare_env(rust_verify::cargo_verus::VERUS_DRIVER_VIA_CARGO, "1");
+    let (mcp, process_args) = consume_mcp_flag(std::env::args());
+    if let Err(message) = authorize_mcp(mcp, via_cargo) {
+        eprintln!("error: {message}");
+        std::process::exit(1);
+    }
     // For now, verus_builtin, vstd, etc. must be rebuilt for each via_cargo crate:
     let via_cargo_rebuild_verus_libs = via_cargo;
 
-    let mut internal_args = std::env::args();
+    let mut internal_args = process_args.clone().into_iter();
     let internal_program = internal_args.next().unwrap();
     let (build_test_mode, has_rustc) = if let Some(first_arg) = internal_args.next() {
         match first_arg.as_str() {
@@ -71,7 +98,8 @@ pub fn main() {
         std::process::exit(1);
     }
 
-    let mut args = if build_test_mode || via_cargo { internal_args } else { std::env::args() };
+    let mut args =
+        if build_test_mode || via_cargo { internal_args } else { process_args.into_iter() };
     let program =
         if build_test_mode || via_cargo { internal_program } else { args.next().unwrap() };
 
@@ -561,3 +589,41 @@ pub fn main() {
         }
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::{MCP_REQUIRED_MESSAGE, authorize_mcp, consume_mcp_flag};
+
+    #[test]
+    fn mcp_flag_is_consumed_before_normal_argument_parsing() {
+        let (mcp, args) =
+            consume_mcp_flag(["rust_verify", "input.rs", "--mcp", "--version"].map(str::to_owned));
+
+        assert!(mcp);
+        assert_eq!(args, ["rust_verify", "input.rs", "--version"]);
+    }
+
+    #[test]
+    fn missing_mcp_flag_is_reported() {
+        let (mcp, args) =
+            consume_mcp_flag(["rust_verify", "input.rs", "--version"].map(str::to_owned));
+
+        assert!(!mcp);
+        assert_eq!(args, ["rust_verify", "input.rs", "--version"]);
+        assert_eq!(authorize_mcp(mcp, false), Err(MCP_REQUIRED_MESSAGE));
+    }
+
+    #[test]
+    fn every_mcp_flag_is_removed() {
+        let (mcp, args) =
+            consume_mcp_flag(["rust_verify", "--mcp", "input.rs", "--mcp"].map(str::to_owned));
+
+        assert!(mcp);
+        assert_eq!(args, ["rust_verify", "input.rs"]);
+    }
+
+    #[test]
+    fn cargo_wrapper_invocation_remains_authorized() {
+        assert_eq!(authorize_mcp(false, true), Ok(()));
+    }
+}

source/rust_verify/src/trait_check.rs

@@ -269,7 +269,7 @@ pub(crate) fn check_trait_conflicts<'tcx>(
     if let Some(mut file) = tc_log_file {
         write!(file, "{}", rust_code).expect("error writing to trait-conflict log file");
     }
-    let rustc_args = [TC_DRIVER_ARG, TCFileLoader::FILENAME, "--error-format=json"];
+    let rustc_args = ["--mcp", TC_DRIVER_ARG, TCFileLoader::FILENAME, "--error-format=json"];
 
     let mut child = std::process::Command::new(std::env::current_exe().unwrap())
         // avoid warning about jobserver fd

source/rust_verify_test/tests/common/mod.rs

@@ -287,7 +287,7 @@ pub fn run_verus(
     #[cfg(target_os = "windows")]
     std::thread::sleep(std::time::Duration::from_millis(1000));
 
-    let mut verus_args = Vec::new();
+    let mut verus_args = vec!["--mcp".to_string()];
     let mut no_external_by_default = false;
     let mut is_core = false;
     let mut use_internal_test_mode = true;
@@ -478,6 +478,7 @@ pub fn run_verus_raw(args: &[&str], dir: &std::path::Path) -> std::process::Outp
     std::process::Command::new(bin)
         .current_dir(dir)
         .env("VERUS_Z3_PATH", z3)
+        .arg("--mcp")
         .args(args)
         .stdout(std::process::Stdio::piped())
         .stderr(std::process::Stdio::piped())

source/verus/src/main.rs

@@ -212,6 +212,11 @@ fn run() -> Result<std::process::ExitStatus, String> {
     } else {
         Command::new(verus_root.join(RUST_VERIFY_FILE_NAME))
     };
+    if !via_cargo {
+        // The wrapper consumed the user-facing flag. Forward authorization so
+        // invoking rust_verify directly cannot bypass the same gate.
+        cmd.arg("--mcp");
+    }
 
     let vstd_kind = get_vstd_kind(&args);
     cmd.env("VSTD_KIND", vstd_kind);

source/vstd_build/src/main.rs

@@ -150,6 +150,7 @@ fn main() {
     let mut child = std::process::Command::new(cmd);
     child.env("RUST_MIN_STACK", (10 * 1024 * 1024).to_string());
     child.env("VSTD_KIND", "IsVstd");
+    child.arg("--mcp");
     child.args(&child_args[..]);
 
     if verbose {