diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml
index 5a49ffa612d..388010ea6ca 100644
--- a/.github/workflows/nightlydeploy.yml
+++ b/.github/workflows/nightlydeploy.yml
@@ -31,10 +31,12 @@ jobs:
       - name: Build with Gradle
         run: ./gradlew --parallel assemble javadoc alldoc
 
-      - name: Upload ShadowJar
+      - name: Upload ShadowJars (fat and slim)
         uses: actions/upload-artifact@v7
         with:
           name: shadowjars
+          # matches the fat jar (key-*-exe.jar) and the slim jar
+          # (key-*-slim-exe.jar) of key.ui, plus any other module artifacts
           path: "*/build/libs/*-exe.jar"
           retention-days: 1
 
@@ -61,6 +63,8 @@ jobs:
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
+          # key-*-exe.jar matches both the fat jar (key-*-exe.jar) and the
+          # slim jar (key-*-slim-exe.jar) built by :key.ui:shadowJar / :key.ui:slimJar.
           gh release create --generate-notes --title "Nightly Release" \
              --prerelease --notes-start-tag KEY-3.0.0-rc \
              nightly key.ui/build/libs/key-*-exe.jar key-javadoc.tar.xz
diff --git a/README.md b/README.md
index afefe0b4eff..537267bd233 100644
--- a/README.md
+++ b/README.md
@@ -75,6 +75,12 @@ Assuming you are in the directory of this README file, you can create a runnable
    ./gradlew :key.ui:shadowJar
    ```
    The file is generated in `key.ui/build/libs/key-*-exe.jar`.
+   A slim variant without the optional keyext extensions and the bundled examples is created with
+   ```sh
+   ./gradlew :key.ui:slimJar
+   ```
+   The file is generated in `key.ui/build/libs/key-*-slim-exe.jar`.
+   Both jars are also built as part of `./gradlew assemble`.
 
 5. A distribution is build with
    ```sh
diff --git a/build.gradle b/build.gradle
index b6a7211b062..9b46c6d2c67 100644
--- a/build.gradle
+++ b/build.gradle
@@ -392,7 +392,9 @@ tasks.register('alldoc', Javadoc){
     def projects = subprojects
     //key.ui javadoc is broken
     source projects.collect { it.sourceSets.main.allJava }
-    classpath = files(projects.collect { it.sourceSets.main.compileClasspath })
+    classpath = files(projects
+            .collect { it.sourceSets.main.compileClasspath }
+    )
     destinationDir = layout.buildDirectory.dir("docs/javadoc").getOrNull().getAsFile()
 
 
diff --git a/dist/build.gradle b/dist/build.gradle
new file mode 100644
index 00000000000..a7846fe220b
--- /dev/null
+++ b/dist/build.gradle
@@ -0,0 +1,52 @@
+plugins {
+    id 'application'
+    id 'java-library'
+    id 'com.gradleup.shadow' version "8.3.8"
+}
+
+description = "KeY distribution with start scripts for the standalone command line tools"
+
+def mainClasses = [
+        key           : "de.uka.ilkd.key.core.Main",
+        pm            : "org.key_project.proofmanagement.Main",
+        "ci-tool"     : "io.github.wadoon.keycitool.CheckerKt",
+]
+
+mainClasses.each { name, mainClass ->
+    def task = tasks.register("create${name.capitalize()}StartScripts", CreateStartScripts) {
+        mainClassName = mainClass
+        applicationName = name
+        outputDir = file("$buildDir/scripts")
+        classpath = sourceSets.main.runtimeClasspath
+    }
+    installDist.dependsOn(task)
+}
+
+repositories {
+    mavenCentral()
+    maven {
+        url = uri("https://central.sonatype.com/repository/maven-snapshots/")
+    }
+}
+
+dependencies {
+    implementation(project(":key.ui"))
+    implementation(project(":keyext.proofmanagement"))
+
+    // third-party plugins
+    runtimeOnly("io.github.wadoon.key:key-citool:1.7.0-SNAPSHOT") {
+        exclude group: "org.key-project", module: ''
+        exclude group: "org.slf4j", module: ''
+    }
+}
+
+
+distributions {
+    main {
+        distributionBaseName = "key"
+        contents {
+            from("$rootDir/README.md")
+            from("$rootDir/LICENSE.TXT")
+        }
+    }
+}
\ No newline at end of file
diff --git a/key.ui/build.gradle b/key.ui/build.gradle
index a380ab55e48..ddf6382d425 100644
--- a/key.ui/build.gradle
+++ b/key.ui/build.gradle
@@ -1,3 +1,5 @@
+import com.github.jengelman.gradle.plugins.shadow.tasks.ShadowJar
+
 import java.nio.file.Files
 import java.nio.file.Paths
 
@@ -40,6 +42,20 @@ dependencies {
     runtimeOnly project(":keyext.isabelletranslation")
 }
 
+// Slim runtime classpath: the full runtimeClasspath minus the optional keyext
+// extension modules. Used to produce the slim shadowJar (see task "slimJar").
+configurations {
+    slimRuntimeClasspath {
+        extendsFrom runtimeClasspath
+        exclude group: 'org.key-project', module: 'keyext.ui.testgen'
+        exclude group: 'org.key-project', module: 'keyext.caching'
+        exclude group: 'org.key-project', module: 'keyext.exploration'
+        exclude group: 'org.key-project', module: 'keyext.slicing'
+        exclude group: 'org.key-project', module: 'keyext.proofmanagement'
+        exclude group: 'org.key-project', module: 'keyext.isabelletranslation'
+    }
+}
+
 tasks.register('createExamplesZip', Zip) {
     description = 'Create "examples.zip" containing all KeY examples'
     destinationDirectory = layout.buildDirectory.dir("resources/main/").getOrNull()
@@ -60,6 +76,34 @@ shadowJar {
     mergeServiceFiles()
 }
 
+// A slim variant of the shadowJar that omits the optional keyext extension
+// modules and the bundled examples.zip. Produces "key-slim-exe.jar".
+tasks.register('slimJar', ShadowJar) {
+    group = "shadow"
+    description = "Create a slim executable jar 'key-slim-exe.jar' without the keyext extensions and without examples.zip"
+    archiveClassifier.set("slim-exe")
+    archiveBaseName.set("key")
+
+    from(sourceSets.named('main').map { it.output })
+    configurations = project.configurations.named('slimRuntimeClasspath').map { [it] }
+
+    manifest {
+        attributes 'Main-Class': 'de.uka.ilkd.key.core.Main'
+    }
+
+    filesMatching("META-INF/services/**") {
+        duplicatesStrategy = DuplicatesStrategy.INCLUDE // needed for mergeServices
+    }
+    mergeServiceFiles()
+
+    // no examples.zip in the slim distribution
+    exclude 'examples.zip'
+}
+
+tasks.named('assemble') {
+    dependsOn tasks.named('slimJar')
+}
+
 distZip {
     archiveBaseName.set("key")
 }
diff --git a/scripts/jenkins/deployAll.sh b/scripts/jenkins/deployAll.sh
index 6d68d70bbd0..e2186e8668f 100755
--- a/scripts/jenkins/deployAll.sh
+++ b/scripts/jenkins/deployAll.sh
@@ -1,5 +1,5 @@
 #!/bin/sh
-./gradlew --parallel clean compileTest :key.ui:shadowJar :key.ui:distZip
+./gradlew --parallel clean compileTest :key.ui:shadowJar :key.ui:slimJar :key.ui:distZip
 
 if [ $? -gt 0 ]; then
   exit $?
diff --git a/settings.gradle b/settings.gradle
index 91c91de2d1e..6f32ac0b580 100644
--- a/settings.gradle
+++ b/settings.gradle
@@ -32,6 +32,9 @@ include "keyext.slicing"
 include "keyext.caching"
 include "keyext.isabelletranslation"
 
+
+include 'dist'
+
 // ENABLE NULLNESS here or on the CLI
 // This flag is activated to enable the checker framework.
 // System.setProperty("ENABLE_NULLNESS", "true")