iq

I/Q

I/Q -- short for Isabelle/Q -- is an Isabelle/jEdit plugin exposing proof editing/exploration capabilities as an MCP server:

1. Reading and writing theory files through jEdit
2. Querying open documents and document stats (warnings, errors, timing information)
3. Querying command states (e.g. intermediate proof states)
4. Proof search and exploration via sledgehammer, find_theorems, and an overlay-based mechanism for try-running Isar proof steps/scripts without interfering with the user.

The purpose of I/Q is to enable MCP-capable AI agents such as Amazon Q to autonomously or collaboratively conduct interactive theorem proving using Isabelle.

NOTE: I/Q is still a very early prototype. We expect that its mechanisms will need tweaking/expanding. I/Q is mechanism only: It needs to be complemented with behavioral guidance and/or additional knowledge to become an effective proof engineer. If you are curious, please try I/Q and let us know about your use cases and ideas for improvement!

Usage

Prerequisites

We recommend Isabelle2025-2. We have not tested I/Q with another version of Isabelle. The build instructions below assume a Unix-like environment (e.g. Linux, macOS).

Building the plugin

You can build the plugin via make and make install. This compiles the Scala sources and installs the plugin JAR. By default, the JAR is copied to ~/.isabelle/Isabelle2025-2/jedit/jars/, but you can inspect and configure various environment variables; see make help.

Registering the plugin

You need to register the plugin with your agentic AI as an MCP server. For Amazon Q, add the following to your mcp.json:

{
  "I/Q": {
    "command": "python3",
    "args": ["{ROOT_DIRECTORY_OF_PLUGIN}/iq_bridge.py"],
    "env": {},
    "autoApprove": [],
    "description": "MCP server to connect to an Isabelle/jEdit instance and inspect/modify Isabelle theory files, proof states, and session information"
  }
}

Starting I/Q

I/Q starts automatically when you start Isabelle, and you should see it as Plugins → I/Q. If not, the plugin was not successfully registered.

I/Q UI settings

I/Q now exposes a plugin options panel at Plugins → Plugin Options → I/Q for dockable-focused settings:

• Maximum retained log lines for the server-log and PIDE-markup panels
• Maximum retained explore output messages
• Log auto-scroll toggle
• Explore argument auto-fill behavior
• Verbose explore debug logging toggle
• Allowed mutation roots (write/create scope) and allowed read roots

Saving security-root settings applies immediately by restarting only the I/Q MCP server. Isabelle/jEdit does not need to be restarted (connected MCP clients may need to reconnect).

Connecting to I/Q (Raw)

I/Q listens for MCP clients on 127.0.0.1:8765. The provided iq_bridge.py bridges stdin/stdout to the TCP server. For example:

echo '{"jsonrpc": "2.0", "method": "tools/list", "id": "1"}' | python3 ./iq_bridge.py

Note: Most tools require authentication. Call the authenticate tool first (see Security), then issue tool calls on the same session.

Security configuration

I/Q binds exclusively to 127.0.0.1 (localhost). Remote binding is not configurable.

• Session-based authentication: Clients must call the authenticate tool with I/Q's authentication token before any other tool (except tools/list, initialize, and ping which are always available). Authentication persists for the lifetime of the TCP connection. The authentication token is either taken from the IQ_AUTH_TOKEN environment variable (if set), or autogenerated and displayed in the I/Q dockable panel.
• Read-oriented tools (list_files, read_file, get_command_info, get_document_info, open_file, resolve_command_target, get_context_info, get_entities, get_type_at_selection, get_proof_blocks, get_proof_context, get_definitions, get_diagnostics, get_processing_status, get_sorry_positions, explore) are restricted to allowed read roots.
• Mutating tools (open_file with create_if_missing=true, write_file, save_file) are restricted to allowed mutation roots.
• get_command_info with xml_result_file is also treated as a mutating operation and must target an allowed mutation root.
• Canonical tool surface (no compatibility aliases): open_file subsumes file creation, get_context_info subsumes direct goal-state reads, and get_proof_blocks subsumes single-block extraction.

Use these environment variables to configure behavior:

• IQ_AUTH_TOKEN: If set, its value is used as a static authentication token. If not set, a random token is generated and displayed in the I/Q dockable panel.
• IQ_MCP_ALLOWED_ROOTS: Path-list of allowed mutation roots (supports OS path separator, comma, or newline delimiters). Precedence: environment variable → I/Q UI setting → current working directory.
• IQ_MCP_ALLOWED_READ_ROOTS: Path-list of allowed read roots (supports OS path separator, comma, or newline delimiters). Precedence: environment variable → I/Q UI setting → value of IQ_MCP_ALLOWED_ROOTS.
• IQ_MCP_MAX_CLIENT_THREADS: Maximum concurrent MCP client handler threads (default: 16, minimum 2).

The bundled iq_bridge.py is a stdio-to-TCP proxy that forwards JSON-RPC messages, enforces socket read timeouts, and supports log-file rotation:

• IQ_MCP_BRIDGE_HOST: Host to connect to (default: localhost)
• IQ_MCP_BRIDGE_PORT: Port to connect to (default: 8765)
• IQ_MCP_BRIDGE_RESPONSE_TIMEOUT_SEC (default: 300)
• IQ_MCP_BRIDGE_LOG_MAX_BYTES (default: 5242880)
• IQ_MCP_BRIDGE_LOG_FILE (default: iq/bridge_log.txt)

Threat model: The security model aims to protect against unauthorized access from remote hosts and from other local OS users. It does not try to protect against malicious processes running as the same OS user.

Connecting to I/Q via an MCP client

If you connect to I/Q via an MCP-capable AI agent, you should see it learn and use the MCP interface automatically. For example, if you have Amazon Q installed and the I/Q MCP server registered as above, you should see the following:

% q chat
✓ iq loaded in 0.36 s
...
🤖 You are chatting with {MODEL}

> List the names of all theory files currently open in Isabelle
...
> I'll list all the theory files currently open in Isabelle using the I/Q MCP interface.

🛠️  Using tool: list_files from mcp server iq
 ⋮
 ● Running list_files with the param:
 ⋮  {
 ⋮    "arguments": {
 ⋮      "filter_open": true,
 ⋮      "filter_theory": true
 ⋮    },
 ⋮    "name": "list_files"
 ⋮  }

Allow this action? Use 't' to trust (always allow) this tool for the session. [y/n/t]:

> t

 ⋮
 ● Completed in 0.167s


> Here are all the theory files currently open in Isabelle:

... LIST ...

You have XXX theory files open in total, ...

MCP Tools

Authentication

• authenticate: Must be called before any other tool. Pass the IQ_AUTH_TOKEN value. Always available (no prior auth needed).

The following methods are also always available without authentication: initialize, tools/list, ping.

Document tools

1. list_files: List all files tracked by Isabelle with filtering and sorting options
2. get_command_info: Get detailed command information including status, errors, and proof states
3. get_document_info: Comprehensive theory file status with error/warning details
4. open_file: Open an existing file, or create one when create_if_missing=true; optional content and overwrite_if_exists are supported for create flows
5. read_file: Read file content with line range and pattern search support
6. write_file: Write or modify content in theory files with multiple edit modes (str_replace, insert, line replacement)
7. resolve_command_target: Resolve canonical command selection (current, file_offset, file_pattern) to a concrete command with normalized target metadata
8. get_context_info: Read-only context summary at a command target, including proof-context status and nested goal state
9. get_entities: Read-only theory entity listing (lemma/definition/fun/etc.) with line and offset metadata
10. get_type_at_selection: Read-only type introspection around a selected command/offset
11. get_proof_blocks: Read-only proof-block extraction with required scope (selection or file); selection returns the focused block, file returns multiple blocks
12. get_proof_context: Read-only local proof context lookup (print_context) at a command selection
13. get_definitions: Read-only definition lookup for names via get_defs at a command selection
14. get_diagnostics: Error/warning diagnostics for either command selection or full file scope. Always returns a file_summary block with theory-scoped totals (so callers can detect when the diagnostic list is incomplete because parts of the file are unprocessed). Set wait_until_processed=true to block until the theory is fully processed before collecting.
15. get_processing_status: Get current processing status of a file
16. get_sorry_positions: Get positions of sorry placeholders in a file
17. explore: Non-invasive proof exploration at any point in a document, with three query types:
    • query='proof': Execute an Isar method/script candidate (requires arguments with the Isar text, e.g. 'by simp')
    • query='sledgehammer': Run sledgehammer (optional arguments for prover list)
    • query='find_theorems': Search for theorems (requires arguments with the search query, optional max_results)
18. save_file: Save one file or all modified open files
19. set_auto_save: Toggle or query auto-save. When enabled (the default), every write_file edit is persisted to disk immediately, keeping the jEdit buffer and the file-system contents in sync. Omit enabled to query the current state. The setting is shared with the "Auto-save edits" checkbox in the I/Q dockable.

I/R REPL tools

These tools provide an interactive Isabelle/Isar REPL through I/Q (requires the I/R component). Authentication with the I/R daemon is managed internally: I/Q reads the daemon's token from its startup output and passes it to IRClient automatically. No manual token configuration is needed for the I/Q → I/R link.

• repl_connect: Start the I/R daemon and connect. Must be called before other REPL tools.
• repl_init: Create a new REPL importing given theories
• repl_init_from_source: Create a REPL from a source file location (file + offset or pattern)
• repl_fork: Fork a new REPL from the current one at a given state index
• repl_focus: Switch to a REPL by id
• repl_step: Execute Isar text as the next step
• repl_show: Show current REPL info (origin, steps, staleness)
• repl_state: Show proof state at a step index
• repl_text: Print concatenated Isar text of the current REPL
• repl_edit: Replace a step, marking later steps stale
• repl_replay: Re-execute all stale steps
• repl_truncate: Keep steps 0..idx, discard the rest
• repl_back: Revert the last step
• repl_merge: Inline current sub-REPL back into its parent
• repl_remove: Delete a REPL and all its sub-REPLs
• repl_list: List all REPLs with step counts and origins
• repl_sledgehammer: Run sledgehammer on the current proof goal
• repl_find_theorems: Search for theorems
• repl_timeout: Set step timeout for a specific REPL
• repl_raw: Send a raw ML expression to the REPL

Tool Classification

Read-only tools (restricted to allowed read roots): list_files, read_file, get_command_info, get_document_info, open_file (without create_if_missing), resolve_command_target, get_context_info, get_entities, get_type_at_selection, get_proof_blocks, get_proof_context, get_definitions, get_diagnostics, get_processing_status, get_sorry_positions, explore

Mutating tools (restricted to allowed mutation roots): open_file (with create_if_missing=true), write_file, save_file, get_command_info (with xml_result_file)

Behavioral Guidance

For effective use with AI assistants, consider developing textual guidance on how to use I/Q. You find an example in iq_guidance.md. If you find ways to improve/refine this guidance, please let us know!