Prevail mcp

CMakeLists.txt

@@ -100,6 +100,8 @@ string(REGEX REPLACE "([][+.*()^$?|\\\\])" "\\\\\\1" prevail_source_dir_escaped
 
 file(GLOB_RECURSE prevail_LIB_SRC CONFIGURE_DEPENDS "${prevail_source_dir}/src/*.cpp")
 list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/main\\.cpp$")
+list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/prevail_mcp\\.cpp$")
+list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/mcp/.*")
 list(FILTER prevail_LIB_SRC EXCLUDE REGEX "${prevail_source_dir_escaped}/src/test/.*")
 
 add_library(prevail ${prevail_LIB_SRC})
@@ -193,6 +195,37 @@ else ()
     RUNTIME_OUTPUT_DIRECTORY "${prevail_binary_dir}")
 endif ()
 
+# MCP server
+option(prevail_ENABLE_MCP "Build MCP server" OFF)
+if (prevail_ENABLE_MCP)
+  FetchContent_Declare(nlohmann_json
+    GIT_REPOSITORY "https://github.com/nlohmann/json.git"
+    GIT_TAG "v3.12.0"
+    GIT_SHALLOW ON
+  )
+  FetchContent_MakeAvailable(nlohmann_json)
+
+  file(GLOB prevail_MCP_SRC CONFIGURE_DEPENDS "${prevail_source_dir}/src/mcp/*.cpp")
+  add_library(prevail_mcp_lib STATIC ${prevail_MCP_SRC})
+  target_link_libraries(prevail_mcp_lib PUBLIC prevail nlohmann_json::nlohmann_json)
+  target_include_directories(prevail_mcp_lib PUBLIC
+    "${prevail_source_dir}/src"
+  )
+
+  add_executable(prevail_mcp "${prevail_source_dir}/src/prevail_mcp.cpp")
+  target_link_libraries(prevail_mcp PRIVATE prevail_mcp_lib ${CMAKE_DL_LIBS})
+  if (CMAKE_CONFIGURATION_TYPES)
+    set_target_properties(prevail_mcp PROPERTIES
+      RUNTIME_OUTPUT_DIRECTORY_DEBUG "${prevail_binary_dir}"
+      RUNTIME_OUTPUT_DIRECTORY_RELEASE "${prevail_binary_dir}"
+      RUNTIME_OUTPUT_DIRECTORY_RELWITHDEBINFO "${prevail_binary_dir}"
+    )
+  else ()
+    set_target_properties(prevail_mcp PROPERTIES
+      RUNTIME_OUTPUT_DIRECTORY "${prevail_binary_dir}")
+  endif ()
+endif ()
+
 # Tests
 if (prevail_ENABLE_TESTS)
   FetchContent_Declare(Catch2
@@ -219,6 +252,11 @@ if (prevail_ENABLE_TESTS)
 
   target_link_libraries(tests PRIVATE prevail ebpf_yaml_lib bpf_conformance_core Catch2::Catch2WithMain Threads::Threads yaml-cpp::yaml-cpp)
 
+  if (prevail_ENABLE_MCP)
+    target_link_libraries(tests PRIVATE prevail_mcp_lib)
+    target_compile_definitions(tests PRIVATE PREVAIL_HAS_MCP)
+  endif ()
+
   if (CMAKE_CONFIGURATION_TYPES)
     set_target_properties(tests run_yaml PROPERTIES
       RUNTIME_OUTPUT_DIRECTORY_DEBUG "${prevail_binary_dir}"
@@ -249,6 +287,7 @@ install(TARGETS prevail libbtf GSL
 install(DIRECTORY "${prevail_source_dir}/src/"
   DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/prevail"
   FILES_MATCHING PATTERN "*.hpp" PATTERN "*.h"
+  PATTERN "mcp/*" EXCLUDE
   PATTERN "test/*" EXCLUDE
 )
 

README.md

@@ -99,6 +99,12 @@ $ bin/prevail ebpf-samples/cilium/bpf_lxc.o 2/1
 PASS: 2/1
 ```
 
+### MCP Server
+
+An MCP server (`prevail_mcp`) exposes the verifier's analysis as structured JSON
+tools for LLM agents. Build with `cmake --build build --target prevail_mcp`.
+See [src/mcp/README.md](src/mcp/README.md) for details.
+
 <details><summary>Usage</summary>
 
 ```text

docs/README.md

@@ -14,6 +14,7 @@ This documentation provides a comprehensive guide to understanding the Prevail e
 | [Memory Model](memory-model.md) | Stack, packet, context, and shared memory handling |
 | [Type System](type-system.md) | Type domains and type-guided verification |
 | [Failure Slicing](failure-slicing.md) | Minimal diagnostic slices for verification failures |
+| [MCP Server](../src/mcp/README.md) | Structured verification queries for LLM agents |
 | [Building](building.md) | Build instructions for all platforms |
 | [Testing](testing.md) | Test infrastructure and conformance testing |
 | [Glossary](glossary.md) | Terminology and definitions |
@@ -94,6 +95,8 @@ Prevail verifies that eBPF programs:
 ```text
 src/
 ├── main.cpp        # CLI entry point
+├── mcp/            # MCP server (structured verification queries for LLM agents)
+├── prevail_mcp.cpp # MCP server entry point
 ├── ir/             # Intermediate representation
 │   ├── syntax.hpp  # Instruction definitions
 │   └── cfg_builder.cpp
@@ -127,7 +130,18 @@ src/
 
 When verification fails, you can use an LLM to help diagnose the issue.
 
-**Quick start** (with GitHub Copilot CLI):
+**Using the MCP server** (recommended — structured data, no text parsing):
+
+Build and start `prevail_mcp` (see [MCP Server](../src/mcp/README.md)):
+
+```bash
+cmake --build build --target prevail_mcp
+# Add to your MCP client (Copilot CLI: /mcp add, VS Code: .vscode/mcp.json)
+```
+
+Then ask your LLM: *"Use get_slice to diagnose the verification failure in program.o"*
+
+**Using prevail with verbose output** (text-based):
 
 ```text
 Using docs/llm-context.md, run ./bin/prevail <your-program.o> <section> -v and diagnose the failure.
@@ -138,7 +152,15 @@ Using docs/llm-context.md, run ./bin/prevail <your-program.o> <section> -v and d
 2. Copy the contents of `docs/llm-context.md` into your LLM conversation
 3. Paste the verification error and ask for diagnosis
 
-See [llm-context.md](llm-context.md) for the context document and [test-data/llm-context-tests.md](../test-data/llm-context-tests.md) for validated test cases.
+**Using prevail with failure slicing** (most concise text output):
+
+```bash
+./bin/prevail program.o section --failure-slice
+```
+
+See [llm-context.md](llm-context.md) for the diagnostic reference,
+[test-data/llm-context-tests.md](../test-data/llm-context-tests.md) for validated test cases,
+and [MCP Server](../src/mcp/README.md) for the structured query tools.
 
 ### Contributing New Failure Patterns
 

docs/llm-context.md

@@ -490,6 +490,20 @@ Typical fixes:
 
 When analyzing failures, you may need more context. Here's how to request it:
 
+### MCP Server (Recommended for LLM Agents)
+
+If the `prevail_mcp` MCP server is available, use it for structured queries instead
+of parsing text output. The MCP server exposes the same analysis data as `prevail -v`
+and `prevail --failure-slice` through JSON tool calls:
+
+- **`get_slice`** — Backward slice with register relevance (replaces manual `-v` parsing)
+- **`get_invariant`** — Query pre/post state at specific PCs
+- **`get_instruction`** — Full detail for specific instructions
+- **`check_constraint`** — Test hypotheses about the verifier's state
+- **`get_source_mapping`** — Map between C source lines and BPF instructions
+
+See [src/mcp/README.md](../src/mcp/README.md) for the full tool reference.
+
 ### Verbose Output
 
 Run with `-v` flag for verbose output showing invariants at each step:
@@ -506,6 +520,14 @@ Request the full disassembly to see surrounding instructions:
 ./bin/prevail <elf-file> <section> --asm <disasm-file>
 ```
 
+### Failure Slicing
+
+Run with `--failure-slice` for a minimal diagnostic showing only causal instructions:
+
+```bash
+./bin/prevail <elf-file> <section> --failure-slice
+```
+
 ### Specific Invariant
 
 Ask the user to share: