# zhehou/llm-isabelle architecture

> Architecture diagram of the GitHub repository zhehou/llm-isabelle, generated by GitDiagram from its file tree, README and a sample of source files (last updated 2026-10-01). It is an AI-made overview: check details against the source.

- Interactive diagram: https://gitdiagram.com/zhehou/llm-isabelle
- Repository: https://github.com/zhehou/llm-isabelle

## Overview

Isabellm is a research playground for LLM-guided Isabelle/HOL proofs. The stepwise workflow accepts a goal, proposes and ranks tactics, checks them against Isabelle, and returns a proof result; the planner separately generates Isar outlines and repairs holes with verified progress. The README also describes premise selection, reranking, ATP and counterexample tools, and AFP micro-RAG. Edges reflect shown calls or README-documented capabilities; unsampled subsystems are included where documented, with links omitted when wiring is not evidenced.

Main entry points: [`prover/prover.py`](https://github.com/zhehou/llm-isabelle/blob/main/prover/prover.py) (Stepwise proof engine), [`planner/driver.py`](https://github.com/zhehou/llm-isabelle/blob/main/planner/driver.py) (Outline and fill driver), [`planner/repair.py`](https://github.com/zhehou/llm-isabelle/blob/main/planner/repair.py) (Proof repair), [`isabelle_ui/server.py`](https://github.com/zhehou/llm-isabelle/blob/main/isabelle_ui/server.py) (jEdit web service)

## Diagram (Mermaid)

```mermaid
flowchart TD

subgraph group_stepwise["Stepwise prover"]
  node_step_cli["Prover CLI<br/>[cli.py]"]
  node_step_engine["Stepwise proof engine<br/>[prover.py]"]
  node_tactic_search["Tactic strategies<br/>[tactics.py]"]
end

subgraph group_planner["Isar planner"]
  node_plan_cli["Planner CLI<br/>[cli.py]"]
  node_plan_driver["Outline and fill driver<br/>[driver.py]"]
  node_skeleton["Outline generation<br/>[skeleton.py]"]
  node_context_fill["Exact-context search<br/>[contextual.py]"]
  node_hole_repair["Proof repair<br/>[repair.py]"]
  node_goal_context["Goal context extraction<br/>[goals.py]"]
  node_frontier["Verified frontier<br/>[frontier.py]"]
end

subgraph group_reasoning["Search and retrieval"]
  node_heuristics["Proof heuristics<br/>[heuristics.py]"]
  node_premises["Premise selection<br/>[premises.py]"]
  node_context["Theory context<br/>[context.py]"]
  node_reranker["Tactic reranker<br/>[ranker.py]"]
end

subgraph group_integrations["Runtime integrations"]
  node_llm["LLM routing<br/>[llm.py]"]
  node_isabelle["Isabelle proof engine<br/>[isabelle_api.py]"]
  node_atp["ATP and checkers<br/>[strategies.py]"]
  node_config["Runtime configuration<br/>[config.py]"]
  node_ui["jEdit web service<br/>[server.py]"]
end

node_user(("Proof author"))
node_llm_services{{"LLM providers"}}

node_user -->|"submits goal"| node_step_cli
node_step_cli -->|"invokes prover"| node_step_engine
node_step_engine -->|"generates tactics"| node_tactic_search
node_step_engine -->|"requests candidates"| node_llm
node_step_engine -->|"uses heuristics"| node_heuristics
node_step_engine -->|"selects premises"| node_premises
node_step_engine -->|"boosts facts"| node_context
node_step_engine -->|"ranks candidates"| node_reranker
node_step_engine -->|"checks proof steps"| node_isabelle
node_step_engine -->|"uses proof tools"| node_atp
node_llm -->|"routes generation"| node_llm_services
node_user -->|"requests outline"| node_plan_cli
node_plan_cli -->|"starts planning"| node_plan_driver
node_plan_driver -->|"generates outlines"| node_skeleton
node_plan_driver -->|"fills holes"| node_context_fill
node_plan_driver -->|"repairs proof"| node_hole_repair
node_plan_driver -->|"extracts goal context"| node_goal_context
node_plan_driver -->|"tracks progress"| node_frontier
node_plan_driver -->|"verifies proof"| node_isabelle
node_context_fill -->|"reuses generators"| node_step_engine
node_hole_repair -->|"uses goal details"| node_goal_context
node_hole_repair -->|"checks progress"| node_frontier
node_ui -->|"calls prover"| node_step_engine
node_ui -->|"calls planner"| node_plan_driver
node_step_engine -->|"reads settings"| node_config

click node_step_cli "https://github.com/zhehou/llm-isabelle/blob/main/prover/cli.py"
click node_step_engine "https://github.com/zhehou/llm-isabelle/blob/main/prover/prover.py"
click node_tactic_search "https://github.com/zhehou/llm-isabelle/blob/main/prover/tactics.py"
click node_heuristics "https://github.com/zhehou/llm-isabelle/blob/main/prover/heuristics.py"
click node_premises "https://github.com/zhehou/llm-isabelle/blob/main/prover/premises.py"
click node_context "https://github.com/zhehou/llm-isabelle/blob/main/prover/context.py"
click node_reranker "https://github.com/zhehou/llm-isabelle/blob/main/prover/ranker.py"
click node_llm "https://github.com/zhehou/llm-isabelle/blob/main/prover/llm.py"
click node_isabelle "https://github.com/zhehou/llm-isabelle/blob/main/prover/isabelle_api.py"
click node_atp "https://github.com/zhehou/llm-isabelle/blob/main/prover/strategies.py"
click node_config "https://github.com/zhehou/llm-isabelle/blob/main/prover/config.py"
click node_plan_cli "https://github.com/zhehou/llm-isabelle/blob/main/planner/cli.py"
click node_plan_driver "https://github.com/zhehou/llm-isabelle/blob/main/planner/driver.py"
click node_skeleton "https://github.com/zhehou/llm-isabelle/blob/main/planner/skeleton.py"
click node_context_fill "https://github.com/zhehou/llm-isabelle/blob/main/planner/contextual.py"
click node_hole_repair "https://github.com/zhehou/llm-isabelle/blob/main/planner/repair.py"
click node_goal_context "https://github.com/zhehou/llm-isabelle/blob/main/planner/goals.py"
click node_frontier "https://github.com/zhehou/llm-isabelle/blob/main/planner/frontier.py"
click node_ui "https://github.com/zhehou/llm-isabelle/blob/main/isabelle_ui/server.py"

classDef toneNeutral fill:#f8fafc,stroke:#334155,stroke-width:1.5px,color:#0f172a
classDef toneBlue fill:#dbeafe,stroke:#2563eb,stroke-width:1.5px,color:#172554
classDef toneAmber fill:#fef3c7,stroke:#d97706,stroke-width:1.5px,color:#78350f
classDef toneMint fill:#dcfce7,stroke:#16a34a,stroke-width:1.5px,color:#14532d
classDef toneRose fill:#ffe4e6,stroke:#e11d48,stroke-width:1.5px,color:#881337
classDef toneIndigo fill:#e0e7ff,stroke:#4f46e5,stroke-width:1.5px,color:#312e81
classDef toneTeal fill:#ccfbf1,stroke:#0f766e,stroke-width:1.5px,color:#134e4a
class node_step_cli,node_step_engine,node_tactic_search toneBlue
class node_plan_cli,node_plan_driver,node_skeleton,node_context_fill,node_hole_repair,node_goal_context,node_frontier toneAmber
class node_heuristics,node_premises,node_context,node_reranker toneMint
class node_llm,node_isabelle,node_atp,node_config,node_ui toneRose
class node_user,node_llm_services toneIndigo
```

## Components

### Stepwise prover

- [Prover CLI](https://github.com/zhehou/llm-isabelle/blob/main/prover/cli.py): `prover/cli.py`
- [Stepwise proof engine](https://github.com/zhehou/llm-isabelle/blob/main/prover/prover.py): `prover/prover.py`
- [Tactic strategies](https://github.com/zhehou/llm-isabelle/blob/main/prover/tactics.py): `prover/tactics.py`

### Isar planner

- [Planner CLI](https://github.com/zhehou/llm-isabelle/blob/main/planner/cli.py): `planner/cli.py`
- [Outline and fill driver](https://github.com/zhehou/llm-isabelle/blob/main/planner/driver.py): `planner/driver.py`
- [Outline generation](https://github.com/zhehou/llm-isabelle/blob/main/planner/skeleton.py): `planner/skeleton.py`
- [Exact-context search](https://github.com/zhehou/llm-isabelle/blob/main/planner/contextual.py): `planner/contextual.py`
- [Proof repair](https://github.com/zhehou/llm-isabelle/blob/main/planner/repair.py): `planner/repair.py`
- [Goal context extraction](https://github.com/zhehou/llm-isabelle/blob/main/planner/goals.py): `planner/goals.py`
- [Verified frontier](https://github.com/zhehou/llm-isabelle/blob/main/planner/frontier.py): `planner/frontier.py`

### Search and retrieval

- [Proof heuristics](https://github.com/zhehou/llm-isabelle/blob/main/prover/heuristics.py): `prover/heuristics.py`
- [Premise selection](https://github.com/zhehou/llm-isabelle/blob/main/prover/premises.py): `prover/premises.py`
- [Theory context](https://github.com/zhehou/llm-isabelle/blob/main/prover/context.py): `prover/context.py`
- [Tactic reranker](https://github.com/zhehou/llm-isabelle/blob/main/prover/ranker.py): `prover/ranker.py`

### Runtime integrations

- [LLM routing](https://github.com/zhehou/llm-isabelle/blob/main/prover/llm.py): `prover/llm.py`
- [Isabelle proof engine](https://github.com/zhehou/llm-isabelle/blob/main/prover/isabelle_api.py): `prover/isabelle_api.py`
- [ATP and checkers](https://github.com/zhehou/llm-isabelle/blob/main/prover/strategies.py): `prover/strategies.py`
- [Runtime configuration](https://github.com/zhehou/llm-isabelle/blob/main/prover/config.py): `prover/config.py`
- [jEdit web service](https://github.com/zhehou/llm-isabelle/blob/main/isabelle_ui/server.py): `isabelle_ui/server.py`

### Other components

- **Proof author**
- **LLM providers**

## Connections

- Proof author → Prover CLI: submits goal
- Prover CLI → Stepwise proof engine: invokes prover
- Stepwise proof engine → Tactic strategies: generates tactics (evidence: `prover/prover.py`)
- Stepwise proof engine → LLM routing: requests candidates (evidence: `prover/prover.py`)
- Stepwise proof engine → Proof heuristics: uses heuristics (evidence: `prover/prover.py`)
- Stepwise proof engine → Premise selection: selects premises (evidence: `prover/prover.py`)
- Stepwise proof engine → Theory context: boosts facts (evidence: `prover/prover.py`)
- Stepwise proof engine → Tactic reranker: ranks candidates (evidence: `prover/prover.py`)
- Stepwise proof engine → Isabelle proof engine: checks proof steps (evidence: `prover/prover.py`)
- Stepwise proof engine → ATP and checkers: uses proof tools (evidence: `prover/prover.py`)
- LLM routing → LLM providers: routes generation
- Proof author → Planner CLI: requests outline
- Planner CLI → Outline and fill driver: starts planning
- Outline and fill driver → Outline generation: generates outlines (evidence: `planner/driver.py`)
- Outline and fill driver → Exact-context search: fills holes (evidence: `planner/driver.py`)
- Outline and fill driver → Proof repair: repairs proof (evidence: `planner/driver.py`)
- Outline and fill driver → Goal context extraction: extracts goal context (evidence: `planner/driver.py`)
- Outline and fill driver → Verified frontier: tracks progress (evidence: `planner/driver.py`)
- Outline and fill driver → Isabelle proof engine: verifies proof (evidence: `planner/driver.py`)
- Exact-context search → Stepwise proof engine: reuses generators (evidence: `planner/contextual.py`)
- Proof repair → Goal context extraction: uses goal details (evidence: `planner/repair.py`)
- Proof repair → Verified frontier: checks progress (evidence: `planner/repair.py`)
- jEdit web service → Stepwise proof engine: calls prover (evidence: `isabelle_ui/server.py`)
- jEdit web service → Outline and fill driver: calls planner (evidence: `isabelle_ui/server.py`)
- Stepwise proof engine → Runtime configuration: reads settings (evidence: `prover/prover.py`)