ACL2 MCP Server

⚠️ Early Beta - Development in Progress This is an early beta version that was rapidly developed. While functional and tested, expect rough edges, potential bugs, and breaking changes. Use at your own risk in production environments.

A Model Context Protocol (MCP) server that provides tools for interacting with the ACL2 theorem prover.

Features

This MCP server exposes 15 tools for working with ACL2, including support for persistent sessions that enable incremental development:

Session Management Tools

• start_session: Create a persistent ACL2 session for incremental development
• end_session: End a persistent session and clean up resources
• list_sessions: List all active sessions with their status

Code-based Tools

• prove: Submit ACL2 theorems (defthm) for proof
• evaluate: Evaluate arbitrary ACL2 expressions and definitions
• check_syntax: Check ACL2 code for syntax errors
• admit: Test if an ACL2 event would be admitted without error

All code-based tools support an optional session_id parameter for incremental development.

File-based Tools

• certify_book: Certify an ACL2 book file (loads and verifies all definitions and theorems)
• include_book: Load an ACL2 book and optionally evaluate additional code
• check_theorem: Check a specific theorem in an ACL2 file by name

Query and Verification Tools

• query_event: Query information about a defined function, theorem, or event (uses :pe)
• verify_guards: Verify guards for a function to ensure efficient execution

Session State Management Tools

• undo: Undo the last N events in a session
• save_checkpoint: Save a named checkpoint of the current session state
• restore_checkpoint: Restore a session to a previously saved checkpoint
• get_world_state: Display current session state (recent definitions and theorems)
• retry_proof: Retry a failed proof with different hints

Prerequisites

• Python 3.10 or later
• ACL2 installed and available in PATH

Installation

# Clone the repository
cd acl2-mcp

# Create and activate virtual environment
python3 -m venv venv
source venv/bin/activate  # On Windows: venv\Scripts\activate

# Install the package
pip install -e .

Usage

Running the Server

The server can be run directly:

acl2-mcp

Or via Python:

python -m acl2_mcp.server

Configuring in Claude Desktop

Add this to your Claude Desktop configuration file:

macOS: ~/Library/Application Support/Claude/claude_desktop_config.json Windows: %APPDATA%\Claude\claude_desktop_config.json

{
  "mcpServers": {
    "acl2": {
      "command": "/path/to/acl2-mcp/venv/bin/acl2-mcp"
    }
  }
}

Replace /path/to/acl2-mcp with the actual path to your installation directory.

Configuring in Claude Code

Recommended: Using the CLI (Simplest method)

Claude Code provides a CLI command to add MCP servers: