LLM support in KeY UI

key.ui/build.gradle

@@ -42,6 +42,8 @@ dependencies {
     runtimeOnly project(":keyext.slicing")
     runtimeOnly project(":keyext.proofmanagement")
     runtimeOnly project(":keyext.isabelletranslation")
+
+    runtimeOnly project(":keyext.llm")
 }
 
 tasks.register('createExamplesZip', Zip) {

key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java

@@ -306,7 +306,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();

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;
+    }
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java

@@ -121,7 +121,7 @@ default void preInit(MainWindow window, KeYMediator mediator) {
 
         }
 
-        void init(MainWindow window, KeYMediator mediator);
+        default void init(MainWindow window, KeYMediator mediator) {};
     }
 
     /**

key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java

@@ -5,13 +5,17 @@
 
 
 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;
 import javax.swing.*;
 
 import de.uka.ilkd.key.gui.KeYFileChooser;
 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;
@@ -232,6 +236,65 @@ protected void addTitledComponent(String title, JComponent component, String hel
         addRowWithHelp(helpText, label, component);
     }
 
+    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) {
@@ -281,7 +344,7 @@ 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
@@ -294,8 +357,8 @@ protected JTextField addTextField(String title, String text, String info,
      *        buttons
      * @param info arbitrary information about the text field
      * @param validator a validator for checking the entered values
-     * @return the created JSpinner
      * @param <T> the class of the minimum value
+     * @return the created JSpinner
      */
     protected <T extends Number & Comparable<T>> JSpinner addNumberField(String title, T min,
             Comparable<T> max, Number step, String info, final Validator<Number> validator) {

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) {

key.ui/src/main/resources/logback.xml

@@ -46,11 +46,20 @@
             <pattern>[%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n</pattern>
         </encoder>
         <filter class="ch.qos.logback.classic.filter.ThresholdFilter">
-            <level>TRACE</level>
+            <level>DEBUG</level>
         </filter>
     </appender>
+
     <logger name="key.devel" level="DEBUG">
         <appender-ref ref="STDERR"/>
     </logger>
 
+	<logger name="org.apache.hc.client5.http.headers" level="DEBUG">
+		<appender-ref ref="STDERR"/>
+
+	</logger>
+	<logger name="org.apache.hc.client5.http.wire">
+		<appender-ref ref="STDERR"/>
+
+	</logger>
 </configuration>

keyext.llm/build.gradle

@@ -0,0 +1,10 @@
+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")
+}

keyext.llm/src/main/java/org/key_project/key/llm/LlmClient.java

@@ -0,0 +1,81 @@
+/* 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.ArrayList;
+import java.util.Map;
+import java.util.concurrent.Callable;
+
+import com.google.gson.GsonBuilder;
+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;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (11/18/25)
+ */
+public class LlmClient implements Callable<Map<String, Object>> {
+    private final LlmSession llmSession;
+    private final LlmContext context;
+    private final LlmContext.LlmMessage prompt;
+
+    public LlmClient(LlmSession llmSession, LlmContext context, String message) {
+        this.llmSession = llmSession;
+        this.context = context;
+        this.prompt = new LlmContext.LlmMessage("user", message);
+    }
+
+    @Override
+    public Map<String, Object> call() throws Exception {
+        var url = llmSession.getApiEndpoint() + "/chat/completions";
+        var request = new HttpPost(url);
+
+        request.addHeader("Authorization", "Bearer " + llmSession.getAuthToken());
+        request.addHeader("Content-Type", "application/json");
+        request.addHeader("Accept", "application/json");
+
+        var msg = new ArrayList<>(context.getMessages());
+        msg.add(prompt);
+
+        var data = Map.of(
+            "model", llmSession.getModel(),
+            "messages", msg);
+
+        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 GsonHttpClientResponseHandler());
+        }
+    }
+
+
+    private static class GsonHttpClientResponseHandler
+            extends AbstractHttpClientResponseHandler<Map<String, Object>> {
+        @Override
+        public Map<String, Object> handleEntity(HttpEntity entity) throws IOException {
+            String content = null;
+            try {
+                content = EntityUtils.toString(entity);
+            } catch (ParseException e) {
+                throw new RuntimeException(e);
+            }
+            // LoggerFactory.getLogger(LlmClient.class).error("Could not parse json response
+            // {}",content);
+            try {
+                return new GsonBuilder().create().fromJson(content, Map.class);
+            } catch (Exception e) {
+                throw new RuntimeException(e);
+            }
+        }
+    }
+}

keyext.llm/src/main/java/org/key_project/key/llm/LlmContext.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.ArrayList;
+import java.util.List;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (11/19/25)
+ */
+public class LlmContext {
+    private final List<LlmMessage> messages = new ArrayList<>();
+
+    public void addMessage(LlmMessage message) {
+        messages.add(message);
+    }
+
+    public List<LlmMessage> getMessages() {
+        return messages;
+    }
+
+    public record LlmMessage(String role, String content) {
+    }
+}