Skip to content

isabelle-assistant

Directory actions

More options

Directory actions

More options

Latest commit

 

History

History

isabelle-assistant

README.md

Isabelle Assistant

LLM-powered proof assistant for Isabelle/jEdit, built on AWS Bedrock with Anthropic Claude tool-use. Provides interactive chat with LaTeX and Mermaid rendering, proof suggestions, code generation, refactoring, and more — all integrated into the Isabelle/jEdit IDE via a dockable chat panel and context-sensitive right-click menu.

Isabelle Assistant is part of the AutoCorrode project.

Architecture

Isabelle Assistant combines four main layers:

graph TB
    subgraph "Layer 1: UI & jEdit Integration"
        Plugin[AssistantPlugin]
        Dockable[AssistantDockable]
        ContextMenu[AssistantContextMenu]
        ChatAction[ChatAction]
        
        Plugin --> Dockable
        Plugin --> ContextMenu
        Dockable --> ChatAction
    end
    
    subgraph "Layer 2: LLM Orchestration"
        Bedrock[BedrockClient]
        PayloadBuilder[PayloadBuilder]
        ResponseParser[ResponseParser]
        Tools[AssistantTools]
        ToolPerms[ToolPermissions]
        Prompts[PromptLoader]
        
        ChatAction --> Bedrock
        Bedrock --> PayloadBuilder
        Bedrock --> ResponseParser
        Bedrock --> Tools
        Tools --> ToolPerms
        Bedrock --> Prompts
    end
    
    subgraph "Layer 3: Isabelle Context & Proof"
        GoalExt[GoalExtractor]
        ContextFetch[ContextFetcher]
        SuggestAct[SuggestAction]
        RefactorAct[RefactorAction]
        IQInteg[IQIntegration]
        
        Tools --> GoalExt
        Tools --> ContextFetch
        ChatAction --> SuggestAct
        ChatAction --> RefactorAct
        SuggestAct --> IQInteg
        RefactorAct --> IQInteg
    end
    
    subgraph "Layer 4: I/Q Backplane"
        McpClient[IQMcpClient]
        IQServer[I/Q MCP Server]
        
        Tools --> McpClient
        IQInteg --> McpClient
        GoalExt --> McpClient
        McpClient -->|TCP JSON-RPC| IQServer
        IQServer -->|PIDE/Isabelle Runtime| IsabelleCore[Isabelle Core]
    end
    
    style Plugin fill:#e1f5ff
    style Bedrock fill:#ffe1f5
    style McpClient fill:#f5ffe1
    style IQServer fill:#fff5e1
Loading

Layer descriptions:

  1. jEdit UI integration (AssistantPlugin, AssistantDockable, context menus, chat actions)
  2. LLM orchestration (BedrockClient, prompts, tool-use loop, retry/caching)
  3. Isabelle context/proof pipelines (ContextFetcher, GoalExtractor, SuggestAction)
  4. I/Q capability backplane for proof-state operations and verification (IQIntegration, IQMcpClient)

Layering rule: proof execution semantics are owned by I/Q. Assistant-side proof tools should orchestrate and render results, not implement local fallback execution paths. The repository enforces this with a failing layering gate (make check-layering) in the Assistant build/test flow. The gate performs two complementary checks: a per-method body scan for forbidden runtime calls, and a whole-file pass that flags val/def bindings capturing forbidden symbols by reference (to defeat indirection bypasses like val f = IQIntegration.verifyProofAsync). Runtime-boundary inventory is tracked in design-documents/10-assistant-runtime-boundary-inventory.tsv and is expected to remain empty (header-only) for forbidden low-level touchpoints under the layering policy. Read-only UI/context introspection is allowed in designated UI modules for responsive context-menu behavior.

For contributor-level component and threading details, see CONTRIBUTING.md.

Highlights

Freeform Chat

Ask natural language questions about Isabelle/HOL directly in the IDE. The chat panel supports Markdown formatting, syntax-highlighted Isabelle code blocks with one-click insertion, rendered LaTeX mathematics, and Mermaid diagrams (offline via local mmdc).

Freeform chat with the Assistant

With Anthropic Claude models, the LLM has autonomous access to tools for reading theory files, checking proof state, searching for theorems, and verifying proofs — enabling it to ground its responses in the actual content of your development.

LaTeX Rendering

Mathematical notation in chat responses is rendered as LaTeX via JLaTeXMath, both inline ($...$) and display ($$...$$).

LaTeX rendering in chat

Mermaid Rendering

Mermaid diagrams in fenced blocks are rendered to images offline using local Mermaid CLI (mmdc):

graph TD
  A[Assumptions] --> B[Derived Fact]
  B --> C[Goal]
Loading

If mmdc is unavailable, the Assistant shows a graceful fallback message and preserves the original Mermaid source block.

For sandboxed or restricted environments where subprocess execution must be disabled, set: -Dassistant.mermaid.disable_subprocess=true

Explain

Explain any Isabelle command, definition, or error at the cursor or in a selection. The LLM receives the surrounding theory context for targeted explanations.

Explaining Isabelle code

Refactor to Isar

Convert apply-style proof scripts to structured Isar proofs. The generated Isar proof is automatically verified against Isabelle (when I/Q is available) and retried with error feedback if verification fails.

Refactoring to Isar

Generate Documentation

Generate documentation comments for definitions, theorems, and other Isabelle commands. The LLM inspects the command type and surrounding context to produce appropriate documentation.

Generating documentation

Generate Introduction Rules

Generate introduction and elimination rules for inductive definitions and datatypes.

Generating introduction rules

Generate Test Cases

Generate QuickCheck-style test cases and examples for definitions.

Generating test cases

Configuration

All settings are accessible via Plugins → Plugin Options → Isabelle Assistant or the :set chat command. Configure AWS region, model selection, verification timeouts, and more.

Settings panel

Getting Started

Once the plugin is installed (see Setup) and a model is selected (Plugins → Plugin Options → Isabelle Assistant, or :set model <model-id> in the chat panel), a typical first-run flow is:

  1. Open a .thy file — the Assistant panel appears docked, with a welcome card and clickable :help link.
  2. Put your cursor inside a lemma or definition and type :explain in the chat. The Assistant explains the code under your cursor.
  3. To generate a proof, put the cursor on an open goal and type :suggest (or :sledgehammer if I/Q is installed).
  4. To check that a proof works, type :verify by simp (or any method) in the chat.

Every feature is discoverable from the chat: type :help for the full command list, or :help <command> (e.g., :help suggest) for per-command details. Right-click inside a .thy file to access the same actions via the Isabelle Assistant submenu.

Troubleshooting

Symptom What to check
Chat returns "Network connection failed" ~/.aws/credentials exists, or AWS_ACCESS_KEY_ID / AWS_SECRET_ACCESS_KEY are set.
Chat returns "AWS credentials are invalid or insufficient" Your IAM role needs bedrock:InvokeModel for the region's Anthropic models (see bedrock:ListFoundationModels).
Chat returns "AI model is not available" Run :models to list regional models, then :set model <id> to pick one.
Chat returns "AWS service limit reached" Wait and retry, or request a Bedrock quota increase in the AWS console.
Chat returns "Operation timed out" Increase the relevant timeout via :set verify_timeout <ms> or in Plugin Options.
Welcome card shows "No model configured" Model ID is empty. Use :models to see candidates, then :set model <id>.
Right-click submenu is missing The file's mode must be isabelle — only .thy files trigger the Assistant context menu.
Proof verification is "Unverified" I/Q is not installed, or the theory does not import Assistant_Support / Isar_Explore. See Setup.

Check the current plugin version at any time with :version. Hover over the I/Q badge in the top-left of the Assistant panel to see which capabilities are enabled.

Prerequisites

Setup

  1. Download dependencies:

    ./fetch-deps.sh

  2. Build and install (includes the I/Q plugin for proof verification):

    make install

  3. Restart Isabelle/jEdit. The Assistant panel appears as a dockable.

  4. Configure your model via Plugins → Plugin Options → Isabelle Assistant, or :set model <model-id> in the chat.

For full feature support, import the Assistant support theory in your development:

imports "Isabelle_Assistant.Assistant_Support"

This provides Eisbach (for tactic generation) and Isar_Explore (for I/Q integration). The status-bar model label shows the current support level:

  • Ready — Assistant_Support imported, all features available.
  • Partial — Eisbach is available but I/Q is not imported, or vice versa.
  • No I/Q — variant of Partial shown when I/Q specifically is unavailable.
  • LLM Only — neither I/Q nor Eisbach detected; chat and LLM features still work.

Features

Context Menu

Right-click in any .thy file to access the Isabelle Assistant submenu. Available actions adapt to context — proof state, text selection, cursor position, error presence, and I/Q availability.

Feature Overview

Category Feature Description I/Q
Understanding Explain Explain code at cursor or selection
Explain Error Analyze error messages
Show Type Display type information at cursor
Summarize Theory Summarize theory content
Explain Counterexample Explain nitpick/quickcheck counterexamples
Proof Suggest Proof Step LLM proof suggestions with optional sledgehammer for verification
Suggest Strategy High-level proof strategy recommendations
Sledgehammer Run external ATP provers ✓
Nitpick Search for counterexamples ✓
Quickcheck Test conjectures with random examples ✓
Try Methods Try simp/auto/blast/force/fastforce ✓
Trace Simplifier Trace simp/auto rewriting steps ✓
Print Context Show proof context (assumptions, goals) ✓
Refactoring Refactor to Isar Convert apply-style to structured Isar for verification
Tidy Clean up formatting and cartouches for verification
Extract Lemma Extract proof steps into a separate lemma for verification
Generation Doc Comment Generate documentation comments
Intro/Elim Rules Generate introduction and elimination rules
Test Cases Generate QuickCheck-style test cases
Suggest Name Suggest descriptive names for definitions/lemmas/theorems
Suggest Tactic Generate Eisbach methods
Analysis Analyze Patterns Analyze proof patterns and suggest improvements
Find Theorems Search for matching theorems ✓
Navigation List Theories List open theory files
Read Theory Display theory content
Search in Theory Search for patterns within a theory
Theory Dependencies Show theory import graph

Verification Badges

When I/Q is available, generated proofs are automatically verified against Isabelle before display. Failed proofs are retried with error feedback. Results show verification badges:

  • ✓ Verified — proof checked by Isabelle
  • ⚡ Sledgehammer — found by external provers
  • ? Unverified — not checked (I/Q unavailable)
  • ✗ Failed — verification failed after retries

Verification cache semantics: only successful verification outcomes are cached. Failed, timeout, and unavailable outcomes are not cached, so retries always re-run verification.

Tool Use (Anthropic Models)

With Anthropic Claude models, the LLM can autonomously use tools during chat. The current build exposes around 50 tools, grouped by capability:

  • Theory I/O. read_theory, list_theories, search_theories, search_in_theory, search_all_theories, get_file_stats, edit_theory, create_theory, open_theory, set_cursor_position.
  • Proof state. get_goal_state, get_subgoal, get_proof_context, get_proof_block, get_proof_outline, get_context_info, get_command_text, get_type, get_sorry_positions, get_processing_status.
  • Library search & diagnostics. find_theorems, get_definitions, get_dependencies, get_entities, get_errors, get_warnings, get_diagnostics.
  • Verification & counterexamples. verify_proof, run_sledgehammer, run_nitpick, run_quickcheck, find_counterexample, try_methods, execute_step, trace_simplifier.
  • Web. web_search.
  • Interactive & planning. ask_user, plan_approach.
  • Persistence & workflow. task_list_add, task_list_done, task_list_irrelevant, task_list_next, task_list_show, task_list_get, memory_add, memory_delete, memory_delete_topic, memory_list_topics, memory_list, memory_get, memory_search.

The authoritative list of wire names is the ToolId enum in src/ToolId.scala; per-tool descriptions and parameters live on the tools registry in src/AssistantTools.scala. AssistantToolsTest.scala exercises dispatch for every wired tool, so that test suite is the practical source of truth for which tools are fully integrated in a given build.

Implementation note: assistant tool names are stable user-facing abstractions. Internally they route to canonical I/Q MCP capabilities (get_context_info, scoped get_proof_blocks, and open_file creation mode), without assistant-side reimplementation of Isabelle runtime semantics.

Tool execution is gated by a per-tool permission system with four levels:

  • Allow: execute without prompt
  • Ask at First Use: prompt once per session, then remember the decision
  • Ask Always: prompt every time
  • Deny: hide tool from the model and reject invocations

Defaults are conservative: read-only tools are Allow, I/Q compute tools are Ask at First Use, and side-effecting tools (edit_theory, create_theory, open_theory) are Ask Always.

Permission prompts include the target resource and a sanitized argument summary so the user can approve with concrete context. Sensitive argument names — those containing token, secret, password, auth, credential, or api_key — are redacted in the prompt summary.

Additional safety checks:

  • create_theory only accepts valid Isabelle theory file names (no path separators / traversal)
  • file creation is restricted to the current buffer directory
  • edit_theory and create_theory preserve user-provided leading/trailing whitespace in inserted content

Chat Commands

Type :help in the chat to see all commands. Commands are prefixed with :.

Command Description
:help Show all commands
:explain [target] Explain code at location
:explain-error Explain error at cursor
:explain-counterexample Explain counterexample
:suggest [target] Suggest proof steps
:suggest-name Suggest descriptive names for definitions/lemmas/theorems
:suggest-strategy Recommend proof strategy
:suggest-tactic Generate Eisbach method
:tidy Clean up formatting
:refactor Convert to Isar
:extract Extract lemma from selection
:find <pattern> Search for theorems
:sledgehammer Run sledgehammer
:nitpick Run nitpick
:quickcheck Run quickcheck
:try-methods Try common proof methods
:trace Trace simplifier
:print-context Show proof context
:show-type Show type at cursor
:summarize Summarize current theory
:analyze Analyze proof patterns
:generate-doc Generate documentation
:generate-intro Generate intro rule
:generate-elim Generate elim rule
:generate-tests Generate test cases
:verify <proof> Verify proof text
:theories List open theories
:read <theory> Show theory content
:deps <theory> Show theory dependencies
:search <theory> <pattern> Search in theory
:models Refresh available models
:set [key [value]] View/change settings
:version Show plugin name and version

Target Syntax

Commands like :explain and :suggest accept optional targets:

  • cursor or current — current cursor position (default)
  • selection — current text selection
  • Theory.thy:42 — specific line in a theory
  • Theory.thy:10-20 — line range
  • Theory.thy:lemma_name — named element
  • cursor+5, cursor-3 — relative offset

Keyboard Shortcuts

The plugin provides keyboard shortcuts for quick access to common features:

Shortcut Action
Ctrl+Shift+P (Cmd+Shift+P on macOS) Suggest Proof Step
Ctrl+Shift+E (Cmd+Shift+E on macOS) Explain Code
Ctrl+Shift+H (Cmd+Shift+H on macOS) Run Sledgehammer
Ctrl+Shift+C (Cmd+Shift+C on macOS) Focus Chat Input

These shortcuts can be customized via Utilities → Global Options → Shortcuts. If they conflict with existing bindings, jEdit will show a conflict dialog on first use.

Configuration

Access via Plugins → Plugin Options → Isabelle Assistant or :set in chat.

Setting Default Description
region us-east-1 AWS region
model (none) Bedrock model ID (main chat + tool-use model)
planning_model (use main) Optional separate Bedrock model for :plan requests
summarization_model (use main) Optional separate Bedrock model for context summarization
cris true Cross-Region Inference (CRIS); alias: use_cris
max_tokens 4000 Max response tokens per request
max_context_tokens 60000 Max context-window budget (tokens) used for history management
max_tool_iterations 10 Max tool-use iterations per turn (Anthropic)
max_retries 3 Verification retry attempts
verify_timeout 30000 Verification timeout (ms)
verify_suggestions true Verify proofs via I/Q
use_sledgehammer false Run sledgehammer in parallel with suggestions; alias: sledgehammer
sledgehammer_timeout 15000 Sledgehammer timeout (ms)
quickcheck_timeout 5000 Quickcheck timeout (ms)
nitpick_timeout 5000 Nitpick timeout (ms)
max_verify_candidates 5 Max suggestions to verify
find_theorems_limit 20 Max theorems for context
find_theorems_timeout 10000 Find theorems timeout (ms)
trace_timeout 10 Simplifier trace timeout (s)
trace_depth 3 Simplifier trace depth
auto_summarize true Automatically summarize older chat history when context grows
summarization_threshold 0.75 Trigger auto-summarization when context usage exceeds this fraction (0.5 – 0.95)

AWS Credentials

Credentials are read from the standard AWS credential chain:

  • Environment variables (AWS_ACCESS_KEY_ID, AWS_SECRET_ACCESS_KEY)
  • Credentials file (~/.aws/credentials)
  • IAM instance profile (on EC2)

Cross-Region Inference (CRIS)

Enabled by default. Automatically prefixes Anthropic model IDs with us. or eu. based on the selected region.

Development

make help       # Show available targets
make build      # Build the plugin
make test       # Compile and run the full strict unit test suite (CI-gating)
make install    # Build and install (includes I/Q)
make clean      # Remove build artifacts
make debug      # Show build configuration

make test is intentionally strict:

  • It fails on any test compile/runtime failure.
  • It rejects pending/ignored tests and broad exception-swallowing in test sources.
  • It enforces ownership checks for critical modules.

License

This project is licensed under the MIT License. See the LICENSE file.