diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml
index 953ee83037a..e6b76fbbb25 100644
--- a/.github/workflows/nightlydeploy.yml
+++ b/.github/workflows/nightlydeploy.yml
@@ -9,8 +9,11 @@ permissions:
   contents: write
   id-token: write
 
+# The documentation generation for varconds and proof script commands
+# extracts `///` markdown javadocs via therapi, which requires JDK 23+.
+# `--release=21` is still set!
 env:
-  JAVA_VERSION: 21
+  JAVA_VERSION: 25
 
 
 jobs:
@@ -29,7 +32,7 @@ jobs:
         uses: gradle/actions/setup-gradle@v6
 
       - name: Build with Gradle
-        run: ./gradlew --parallel assemble javadoc alldoc
+        run: ./gradlew --parallel assemble javadoc alldoc :key.core:generateVarcondDoc :key.core:generateScriptDoc
 
       - name: Upload ShadowJars (fat and slim)
         uses: actions/upload-artifact@v7
@@ -40,6 +43,14 @@ jobs:
           path: "*/build/libs/*-exe.jar"
           retention-days: 1
 
+      - name: Upload varcond and proof script documentation
+        uses: actions/upload-artifact@v7
+        with:
+          name: varcond-script-docs
+          path: "key.core/build/docs/keydocs/*"
+          retention-days: 30
+          compression-level: '9'
+
       - name: Package
         run: tar cvf key-javadoc.tar.xz build/docs/javadoc
 
diff --git a/build.gradle b/build.gradle
index 93b792ef77c..c89c5127e6a 100644
--- a/build.gradle
+++ b/build.gradle
@@ -83,7 +83,6 @@ subprojects {
         implementation(libs.slf4j.api)
         testImplementation(libs.logback.classic)
 
-
         compileOnly(libs.jspecify)
         testCompileOnly(libs.jspecify)
         compileOnly(libs.checkerframework.qual)
@@ -316,7 +315,6 @@ subprojects {
             afterEvaluate {
                 description = project.description
                 assert (project.description != null && project.description != "") : "Description of modules are required at maven-central"
-                print(project.description)
             }
             url = 'https://key-project.org/'
 
diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index 7ddff7e2730..8038c479dfe 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -25,6 +25,7 @@ stringtemplate = "4.3.4"
 javapoet = "1.13.0"
 javaparser = "3.28.0-K13.6"
 truth = "1.4.5"
+therapi = "0.13.0"
 
 # UI and CLI
 flatlaf = "3.7.2"
@@ -35,6 +36,7 @@ docking-frames = "1.1.3p1"
 # External tools
 scala-isabelle = "0.4.5"
 
+
 [libraries]
 # SLF4J and logging
 slf4j-api = { module = "org.slf4j:slf4j-api", version.ref = "slf4j" }
@@ -43,6 +45,10 @@ logback-classic = { module = "ch.qos.logback:logback-classic", version.ref = "lo
 # JSpecify (nullability annotations)
 jspecify = { module = "org.jspecify:jspecify", version.ref = "jspecify" }
 
+#Extracting Javadoc
+therapi-processor = { module = "com.github.therapi:therapi-runtime-javadoc-scribe", version.ref = "therapi" }
+therapi-runtime = { module = "com.github.therapi:therapi-runtime-javadoc", version.ref = "therapi" }
+
 # EISOP Checker Framework
 checkerframework-qual = { module = "io.github.eisop:checker-qual", version.ref = "eisop" }
 checkerframework-util = { module = "io.github.eisop:checker-util", version.ref = "eisop" }
diff --git a/key.core/build.gradle b/key.core/build.gradle
index c6584ca35ab..f12b7330bac 100644
--- a/key.core/build.gradle
+++ b/key.core/build.gradle
@@ -24,6 +24,9 @@ dependencies {
     testImplementation(libs.truth)
     testImplementation(project(":key.core"))
 
+    annotationProcessor(libs.therapi.processor)
+    api(libs.therapi.runtime)
+
     // https://mvnrepository.com/artifact/com.fasterxml.jackson.dataformat/jackson-dataformat-yaml
     testImplementation(libs.jackson.dataformat.yaml)
 
@@ -32,7 +35,7 @@ dependencies {
 }
 
 tasks.withType(JavaCompile).configureEach {
-    options.compilerArgs << "-Ajavadoc.packages=de.uka.ilkd.key.scripts"
+    options.compilerArgs << "-Ajavadoc.packages=de.uka.ilkd.key.scripts,de.uka.ilkd.key.rule.conditions"
 }
 
 // The target directory for JavaCC (parser generation)
@@ -67,6 +70,38 @@ tasks.register('generateSMTListings') {
     }
 }
 
+// Generates the markdown documentation of all variable conditions (varconds),
+// see de.uka.ilkd.key.doc.VarcondDoc.
+tasks.register('generateVarcondDoc', JavaExec) {
+    group = 'documentation'
+    description = 'Generates the markdown documentation of all variable conditions (varconds).'
+    classpath = sourceSets.main.runtimeClasspath
+    mainClass = 'de.uka.ilkd.key.doc.VarcondDoc'
+    def mdFile = layout.buildDirectory.file("docs/keydocs/varconds.md")
+    def jsonFile = layout.buildDirectory.file("docs/keydocs/varconds.json")
+    outputs.file(mdFile)
+    outputs.file(jsonFile)
+    doFirst {
+        args = [mdFile.get().asFile.absolutePath, jsonFile.get().asFile.absolutePath ]
+    }
+}
+
+// Generates the markdown documentation of all proof script commands,
+// see de.uka.ilkd.key.doc.ScriptDoc.
+tasks.register('generateScriptDoc', JavaExec) {
+    group = 'documentation'
+    description = 'Generates the markdown documentation of all proof script commands.'
+    classpath = sourceSets.main.runtimeClasspath
+    mainClass = 'de.uka.ilkd.key.doc.ScriptDoc'
+    def mdFile = layout.buildDirectory.file("docs/keydocs/script-commands.md")
+    def jsonFile = layout.buildDirectory.file("docs/keydocs/script-commands.json")
+    outputs.file(mdFile)
+    outputs.file(jsonFile)
+    doFirst {
+        args = [mdFile.get().asFile.absolutePath, jsonFile.get().asFile.absolutePath ]
+    }
+}
+
 tasks.register('generateSolverPropsList') {
     def pack = "de/uka/ilkd/key/smt/solvertypes"
     def resourcesDir = "${project.projectDir}/src/main/resources"
diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java
new file mode 100644
index 00000000000..f73fbbbcb1b
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/doc/AbstractDocGenerator.java
@@ -0,0 +1,202 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2, 
+ * or (at your option) any later version.
+ * SPDX-License-Identifier: GPL-2.0-or-later */
+package de.uka.ilkd.key.doc;
+
+import java.io.IOException;
+import java.io.PrintStream;
+import java.io.PrintWriter;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.Map;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ * Base class for the documentation generators of KeY's taclet language constructs, e.g., for the
+ * variable conditions ({@link VarcondDoc}) and the proof script commands ({@link ScriptDoc}). It
+ * provides the shared handling of the output target and the post-processing of javadoc text.
+ *
+ * @author Alexander Weigl
+ * @version 1 (23.08.26)
+ */
+public abstract class AbstractDocGenerator {
+
+    /// Runs this generator. If a command line argument is given, the markdown output is written
+    /// to that file together with a JSON dump ([#generateJsonData()]) next to it; otherwise the
+    /// markdown is printed to stdout.
+    ///
+    /// @param mdFile an optional single argument with the path of the output file
+    /// @param jsonFile
+    /// @throws IOException if the output file cannot be written
+    protected void run(String mdFile, String jsonFile) throws IOException {
+        Path mdPath = Path.of(mdFile);
+        if (mdPath.getParent() != null) {
+            Files.createDirectories(mdPath.getParent());
+        }
+
+        try (var out = new PrintStream(Files.newOutputStream(mdPath), false)) {
+            generateDocumentation(out);
+        }
+
+
+        Object data = generateJsonData();
+
+        if (data != null) {
+            Path jsonPath = Paths.get(jsonFile);
+            if (jsonPath.getParent() != null) {
+                Files.createDirectories(jsonPath.getParent());
+            }
+            try (var out = new PrintWriter(Files.newOutputStream(jsonPath), false)) {
+                JsonWriter.toJson(data, out);
+            }
+        }
+    }
+
+    /// Writes the documentation of this generator in markdown format.
+    protected abstract void generateDocumentation(PrintStream out);
+
+    /// Returns the documentation data of this generator in a structured form, which is serialized
+    /// into a JSON dump next to the markdown file. Returns `null` if this generator does not
+    /// support a JSON dump.
+    ///
+    /// @return the structured documentation data, or `null`
+    protected @Nullable Object generateJsonData() {
+        return null;
+    }
+
+    /// Converts a javadoc comment into markdown by replacing common HTML tags and inline tags
+    /// with their markdown equivalents.
+    ///
+    /// @param it the javadoc comment, may be null
+    /// @return the comment as markdown
+    protected static String cleanJavadoc(@Nullable String it) {
+        if (it == null) {
+            it = "";
+        }
+        return it.replace("<tt>", "`")
+                .replace("<ul>", "\n")
+                .replace("</ul>", "\n")
+                .replace("<ul>", "\n")
+                .replace("<li>", "* ")
+                .replace("</li>", "")
+                .replace("{@link", "`")
+                .replace("}", "`")
+                .replace("<code>", "`")
+                .replace("</tt>", "`")
+                .replace("</code>", "`")
+                .replace("<b>", "**")
+                .replace("</b>", "**");
+    }
+
+    /// Indents each line of the given text by the given prefix.
+    ///
+    /// @param spaces the indentation prefix
+    /// @param it the text to indent
+    /// @return the indented text
+    protected static String indent(String spaces, String it) {
+        return spaces + it.replace("\n", "\n" + spaces);
+    }
+}
+
+
+/**
+ * A minimal, dependency-free JSON serializer supporting the data structures used by the
+ * documentation generators: {@link Map}s, {@link Iterable}s, strings, numbers, booleans, and
+ * {@code null}. Other objects are serialized via their {@link Object#toString()}.
+ *
+ * @author Alexander Weigl
+ * @version 1 (10.10.26)
+ */
+final class JsonWriter {
+
+    private JsonWriter() {
+    }
+
+    /**
+     * Serializes the given value into a pretty-printed JSON string.
+     *
+     * @param value the value to serialize
+     * @param out target to write into
+     */
+    public static void toJson(@Nullable Object value, PrintWriter out) {
+        write(out, value, 0);
+    }
+
+    private static void write(PrintWriter sb, @Nullable Object value, int depth) {
+        switch (value) {
+            case null -> sb.append("null");
+            case String s -> writeString(sb, s);
+            case Boolean b -> sb.print(b);
+            case Number n -> sb.print(n);
+            case Map<?, ?> map -> writeObject(sb, map, depth);
+            case Iterable<?> iterable -> writeArray(sb, iterable, depth);
+            default -> writeString(sb, value.toString());
+        }
+    }
+
+    private static void writeObject(PrintWriter sb, Map<?, ?> map, int depth) {
+        sb.append("{\n");
+        var it = map.entrySet().iterator();
+        while (it.hasNext()) {
+            var entry = it.next();
+            indent(sb, depth + 1);
+            writeString(sb, String.valueOf(entry.getKey()));
+            sb.append(": ");
+            write(sb, entry.getValue(), depth + 1);
+            if (it.hasNext()) {
+                sb.append(',');
+            }
+            sb.append('\n');
+        }
+        indent(sb, depth);
+        sb.append('}');
+    }
+
+    private static void writeArray(PrintWriter sb, Iterable<?> iterable, int depth) {
+        sb.append("[\n");
+        var it = iterable.iterator();
+        while (it.hasNext()) {
+            indent(sb, depth + 1);
+            write(sb, it.next(), depth + 1);
+            if (it.hasNext()) {
+                sb.append(',');
+            }
+            sb.append('\n');
+        }
+        indent(sb, depth);
+        sb.append(']');
+    }
+
+    private static void writeString(PrintWriter sb, String s) {
+        sb.append('"');
+        for (var i = 0; i < s.length(); i++) {
+            char c = s.charAt(i);
+            switch (c) {
+                case '"' -> sb.append("\\\"");
+                case '\\' -> sb.append("\\\\");
+                case '\n' -> sb.append("\\n");
+                case '\r' -> sb.append("\\r");
+                case '\t' -> sb.append("\\t");
+                case '\b' -> sb.append("\\b");
+                case '\f' -> sb.append("\\f");
+                default -> {
+                    if (c < 0x20) {
+                        sb.append("\\u%04x".formatted((int) c));
+                    } else {
+                        sb.append(c);
+                    }
+                }
+            }
+        }
+        sb.append('"');
+    }
+
+    private static void indent(PrintWriter sb, int depth) {
+        sb.append("  ".repeat(depth));
+    }
+}
+\newLocalVars(varDeclsSV: VARIABLE, updateBeforeSV: VARIABLE, updateFrameSV: VARIABLE, bodySV: VARIABLE)
+
diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java
new file mode 100644
index 00000000000..69b610f9c25
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/doc/ScriptDoc.java
@@ -0,0 +1,80 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2, 
+ * or (at your option) any later version.
+ * SPDX-License-Identifier: GPL-2.0-or-later */
+package de.uka.ilkd.key.doc;
+
+import java.io.PrintStream;
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+
+import de.uka.ilkd.key.scripts.ProofScriptCommand;
+import de.uka.ilkd.key.scripts.ProofScriptEngine;
+import de.uka.ilkd.key.scripts.meta.ProofScriptArgument;
+
+/**
+ * Generates the markdown documentation of all proof script commands (loaded via
+ * {@link ProofScriptEngine#loadCommands()}), based on their self-documentation.
+ *
+ * @author Alexander Weigl
+ * @version 1 (23.08.26)
+ */
+public class ScriptDoc extends AbstractDocGenerator {
+
+    public static void main(String[] args) throws Exception {
+        new ScriptDoc().run(args[0], args[1]);
+    }
+
+    @Override
+    protected void generateDocumentation(PrintStream out) {
+        for (var command : sortedCommands()) {
+            out.println();
+            out.println();
+            out.format("### `%s`\n\n", command.getName());
+            out.println(cleanJavadoc(command.getDocumentation()));
+        }
+    }
+
+    @Override
+    protected Object generateJsonData() {
+        var commands = new ArrayList<Map<String, Object>>();
+        for (var command : sortedCommands()) {
+            var data = new LinkedHashMap<String, Object>();
+            data.put("name", command.getName());
+            data.put("category", command.getCategory());
+            data.put("deprecated", command.getClass().isAnnotationPresent(Deprecated.class));
+            data.put("documentation", cleanJavadoc(command.getDocumentation()));
+
+            var arguments = new ArrayList<Map<String, Object>>();
+            for (ProofScriptArgument meta : command.getArguments()) {
+                var argument = new LinkedHashMap<String, Object>();
+                argument.put("name", meta.getName());
+                argument.put("type", meta.getType().getSimpleName());
+                argument.put("kind",
+                    meta.isFlag() ? "flag" : meta.isOption() ? "option" : "positional");
+                argument.put("required", meta.isRequired());
+                if (meta.isPositional()) {
+                    argument.put("position", meta.getArgumentPosition());
+                }
+                if (meta.isPositionalVarArgs() || meta.isOptionalVarArgs()) {
+                    argument.put("varargs", true);
+                }
+                argument.put("description", meta.getDocumentation());
+                arguments.add(argument);
+            }
+            data.put("arguments", arguments);
+            commands.add(data);
+        }
+        return Map.of("commands", commands);
+    }
+
+    /// Returns all loaded proof script commands sorted by their name.
+    private List<ProofScriptCommand> sortedCommands() {
+        var commands = new ArrayList<>(ProofScriptEngine.loadCommands().values());
+        commands.sort(Comparator.comparing(ProofScriptCommand::getName));
+        return commands;
+    }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java
new file mode 100644
index 00000000000..46f1660cd23
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/doc/VarcondDoc.java
@@ -0,0 +1,147 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2, 
+ * or (at your option) any later version.
+ * SPDX-License-Identifier: GPL-2.0-or-later */
+package de.uka.ilkd.key.doc;
+
+import java.io.PrintStream;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Comparator;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+import de.uka.ilkd.key.nparser.varexp.TacletBuilderCommand;
+import de.uka.ilkd.key.nparser.varexp.TacletBuilderCommandInfo;
+import de.uka.ilkd.key.nparser.varexp.TacletBuilderManipulators;
+
+import com.github.therapi.runtimejavadoc.CommentFormatter;
+import com.google.common.collect.Streams;
+
+/**
+ * Generates the markdown documentation of all variable conditions (varconds) registered in
+ * {@link TacletBuilderManipulators}, extracted from the javadocs of the implementing classes.
+ *
+ * @author Alexander Weigl
+ * @version 1 (23.08.26)
+ */
+public class VarcondDoc extends AbstractDocGenerator {
+
+    public static void main(String[] args) throws Exception {
+        new VarcondDoc().run(args[0], args[1]);
+    }
+
+    @Override
+    protected void generateDocumentation(PrintStream out) {
+        for (var entry : collectVarconds().entrySet()) {
+            String name = entry.getKey();
+            List<TacletBuilderCommandInfo> cmds = entry.getValue();
+
+            out.println();
+            out.println();
+            out.format("### `%s`\n\n", name);
+
+            final var generalDocumentation = cmds.getFirst().getGeneralDocumentation();
+            out.println(
+                cleanJavadoc(new CommentFormatter().format(generalDocumentation.getComment())));
+
+            out.format("\n**Signatures**\n\n");
+            for (TacletBuilderCommandInfo cmd : cmds) {
+
+                final var arguments = Streams.zip(
+                    Arrays.stream(cmd.argNames()),
+                    Arrays.stream(cmd.argumentTypes()).map(Enum::toString),
+                    "%s: %s"::formatted)
+                        .collect(Collectors.joining(", "));
+                out.printf("* `%s(%s)`\n", name, arguments);
+
+                if (cmd.isNegationSupported()) {
+                    out.printf("* `\\not%s(%s)`\n", name, arguments);
+                }
+
+                out.println();
+                final var argumentInformation = cmd.getArgumentInformation();
+
+                out.println(
+                    indent("   ", cleanJavadoc(argumentInformation.getComment().toString())));
+                out.println();
+                argumentInformation.getParams().stream()
+                        .map(tag -> "   * `%s` %s".formatted(tag.getName(), tag.getComment()))
+                        .forEach(out::println);
+                out.println();
+            }
+        }
+    }
+
+    @Override
+    protected Object generateJsonData() {
+        var varconds = new ArrayList<Map<String, Object>>();
+        for (var entry : collectVarconds().entrySet()) {
+            String name = entry.getKey();
+            List<TacletBuilderCommandInfo> cmds = entry.getValue();
+
+            var varcond = new LinkedHashMap<String, Object>();
+            varcond.put("name", name);
+            final var generalDocumentation = cmds.getFirst().getGeneralDocumentation();
+            varcond.put("description",
+                cleanJavadoc(new CommentFormatter().format(generalDocumentation.getComment())));
+
+            var signatures = new ArrayList<Map<String, Object>>();
+            for (TacletBuilderCommandInfo cmd : cmds) {
+                final var argumentInformation = cmd.getArgumentInformation();
+                var params = argumentInformation.getParams();
+
+                var signature = new LinkedHashMap<String, Object>();
+                signature.put("negated", cmd.isNegationSupported());
+                signature.put("description",
+                    cleanJavadoc(argumentInformation.getComment().toString()));
+
+                var arguments = new ArrayList<Map<String, Object>>();
+                for (var i = 0; i < cmd.argumentTypes().length; i++) {
+                    var argument = new LinkedHashMap<String, Object>();
+                    argument.put("name", cmd.argNames()[i]);
+                    argument.put("type", cmd.argumentTypes()[i].toString());
+                    if (i < params.size()) {
+                        final var comment = params.get(i).getComment();
+                        argument.put("description",
+                            cleanJavadoc(comment == null ? null : comment.toString()));
+                    }
+                    arguments.add(argument);
+                }
+                signature.put("arguments", arguments);
+                signatures.add(signature);
+            }
+            varcond.put("signatures", signatures);
+            varconds.add(varcond);
+        }
+        return Map.of("varconds", varconds);
+    }
+
+    /// Collects all registered variable conditions, grouped and sorted by their trigger name;
+    /// within a group, the signatures are sorted by the number of declared argument types
+    /// (descending).
+    private LinkedHashMap<String, List<TacletBuilderCommandInfo>> collectVarconds() {
+        Function<String, String> normalizeCmdName =
+            (String it) -> it.startsWith("\\") ? it.replace("\\\\", "\\") : "\\" + it;
+        Function<TacletBuilderCommandInfo, String> getTriggerName = TacletBuilderCommandInfo::name;
+
+        var grouped = TacletBuilderManipulators.getConditionBuilders().stream()
+                .map(TacletBuilderCommand::getInformation)
+                .collect(Collectors.groupingBy(getTriggerName.andThen(normalizeCmdName)));
+        Comparator<TacletBuilderCommandInfo> reversed =
+            Comparator.comparing((TacletBuilderCommandInfo it) -> it.argumentTypes().length)
+                    .reversed();
+
+        var result = new LinkedHashMap<String, List<TacletBuilderCommandInfo>>();
+        grouped.keySet().stream().sorted().forEach(
+            name -> {
+                var cmds = grouped.get(name);
+                cmds.sort(reversed);
+                result.put(name, cmds);
+            });
+        return result;
+    }
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractConditionBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractConditionBuilder.java
index 87d292ddc0b..bf371d002e6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractConditionBuilder.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractConditionBuilder.java
@@ -4,7 +4,7 @@
  * SPDX-License-Identifier: GPL-2.0-or-later */
 package de.uka.ilkd.key.nparser.varexp;
 
-import org.jspecify.annotations.NonNull;
+import org.key_project.prover.rules.VariableCondition;
 
 /**
  * @author Alexander Weigl
@@ -12,8 +12,12 @@
  */
 public abstract class AbstractConditionBuilder extends AbstractTacletBuilderCommand
         implements ConditionBuilder {
-    protected AbstractConditionBuilder(@NonNull String triggerName,
-            @NonNull ArgumentType... argumentsTypes) {
-        super(triggerName, argumentsTypes);
+    protected AbstractConditionBuilder(TacletBuilderCommandInfo info) {
+        super(info);
+    }
+
+    public AbstractConditionBuilder(String name, Class<? extends VariableCondition> clazz,
+            boolean negationSupported, ArgumentType... types) {
+        super(TacletBuilderCommandInfo.createVarcondInfo(name, clazz, negationSupported, types));
     }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractTacletBuilderCommand.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractTacletBuilderCommand.java
index 9c0783554c8..79090c9f933 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractTacletBuilderCommand.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/AbstractTacletBuilderCommand.java
@@ -4,7 +4,6 @@
  * SPDX-License-Identifier: GPL-2.0-or-later */
 package de.uka.ilkd.key.nparser.varexp;
 
-import org.jspecify.annotations.NonNull;
 
 /**
  * Simple default implementation for {@link TacletBuilderCommand}.
@@ -13,36 +12,26 @@
  * @version 1 (12/9/19)
  */
 public abstract class AbstractTacletBuilderCommand implements TacletBuilderCommand {
-    private final @NonNull String triggerName;
-    private final @NonNull ArgumentType[] argumentsTypes;
+    protected final TacletBuilderCommandInfo info;
 
-    /**
-     * Construct this class with the parameters for {@link #isSuitableFor(String)} and
-     * {@link #getArgumentTypes()}.
-     *
-     * @param triggerName the name of this command.
-     * @param argumentsTypes the argument type of this command.
-     */
-    protected AbstractTacletBuilderCommand(@NonNull String triggerName,
-            @NonNull ArgumentType... argumentsTypes) {
-        this.triggerName = triggerName;
-        this.argumentsTypes = argumentsTypes;
+    protected AbstractTacletBuilderCommand(TacletBuilderCommandInfo info) {
+        this.info = info;
     }
 
     @Override
-    public boolean isSuitableFor(@NonNull String name) {
-        if (triggerName.equalsIgnoreCase(name)) {
+    public boolean isSuitableFor(String name) {
+        if (info.name().equalsIgnoreCase(name)) {
             return true;
         }
-        if (name.startsWith("\\")) // handling leading backslashes
-        {
+        // handling leading backslashes
+        if (name.startsWith("\\")) {
             return isSuitableFor(name.substring(1));
         }
         return false;
     }
 
     @Override
-    public ArgumentType[] getArgumentTypes() {
-        return argumentsTypes;
+    public TacletBuilderCommandInfo getInformation() {
+        return info;
     }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java
index 0a20eb11606..e681c95db69 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java
@@ -13,14 +13,19 @@
 
 /**
  * Argument types for {@link TacletBuilderCommand}s.
+ * Each {@link ArgumentType} has an expected class for the type of the argument.
  *
  * @author Alexander Weigl
  * @version 1 (12/9/19)
  * @see TacletBuilderCommand
  */
 public enum ArgumentType {
-    TYPE_RESOLVER(TypeResolver.class), SORT(Sort.class), TERM(JTerm.class),
-    JAVA_TYPE(KeYJavaType.class), VARIABLE(ParsableVariable.class), STRING(String.class);
+    TYPE_RESOLVER(TypeResolver.class),
+    SORT(Sort.class),
+    TERM(JTerm.class),
+    JAVA_TYPE(KeYJavaType.class),
+    VARIABLE(ParsableVariable.class),
+    STRING(String.class);
 
     public final Class<?> clazz;
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java
index 96872e61a4d..3e248f6fcda 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java
@@ -13,39 +13,26 @@
 
 public class ConstructorBasedBuilder extends AbstractConditionBuilder {
     private final Class<? extends VariableCondition> clazz;
-    private final boolean negationSupported;
 
     public ConstructorBasedBuilder(String name, Class<? extends VariableCondition> clazz,
             ArgumentType... types) {
-        this(name, lastArgumentOfFirstContructorIsBoolean(clazz), clazz, types);
+        this(TacletBuilderCommandInfo.createVarcondInfo(name, clazz, types), clazz);
     }
 
-    private static boolean lastArgumentOfFirstContructorIsBoolean(
+    public ConstructorBasedBuilder(TacletBuilderCommandInfo info,
             Class<? extends VariableCondition> clazz) {
-        try {
-            Class<?>[] types = clazz.getConstructors()[0].getParameterTypes();
-            return types[types.length - 1] == Boolean.class
-                    || types[types.length - 1] == Boolean.TYPE;
-        } catch (ArrayIndexOutOfBoundsException e) {
-            return false;
-        }
-    }
-
-    public ConstructorBasedBuilder(String name, boolean negationSupported,
-            Class<? extends VariableCondition> clazz, ArgumentType... types) {
-        super(name, types);
+        super(info);
         this.clazz = clazz;
-        this.negationSupported = negationSupported;
     }
 
     @Override
     public VariableCondition build(Object[] arguments, List<String> parameters, boolean negated) {
-        if (negated && !negationSupported) {
+        if (negated && !info.isNegationSupported()) {
             throw new RuntimeException(clazz.getName() + " does not support negation.");
         }
 
         Object[] args = arguments;
-        if (negationSupported) {
+        if (info.isNegationSupported()) {
             args = Arrays.copyOf(arguments, arguments.length + 1);
             args[args.length - 1] = negated;
         }
@@ -59,4 +46,9 @@ public VariableCondition build(Object[] arguments, List<String> parameters, bool
         }
         throw new RuntimeException();
     }
+
+    @Override
+    public TacletBuilderCommandInfoImpl getInformation() {
+        return (TacletBuilderCommandInfoImpl) super.getInformation();
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommand.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommand.java
index a72227f8035..e6b7f3e6675 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommand.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommand.java
@@ -28,6 +28,9 @@ public interface TacletBuilderCommand {
      */
     boolean isSuitableFor(@NonNull String name);
 
+    /// Returns information about this command.
+    TacletBuilderCommandInfo getInformation();
+
     /**
      * Defines the amount and type of expected arguments. For example, if you want describe a
      * sub-type test (instanceOf) you would need two sorts {@code new ArgumentType[]{SORT,SORT} } as
@@ -39,7 +42,9 @@ public interface TacletBuilderCommand {
      *
      * @see ArgumentType
      */
-    ArgumentType[] getArgumentTypes();
+    default ArgumentType[] getArgumentTypes() {
+        return getInformation().argumentTypes();
+    }
 
     /**
      * Applying this command on the given taclet builder.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java
new file mode 100644
index 00000000000..9287004aead
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderCommandInfo.java
@@ -0,0 +1,339 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2, 
+ * or (at your option) any later version.
+ * SPDX-License-Identifier: GPL-2.0-or-later */
+package de.uka.ilkd.key.nparser.varexp;
+
+import java.lang.reflect.Constructor;
+import java.util.Arrays;
+import java.util.List;
+
+import com.github.therapi.runtimejavadoc.ClassJavadoc;
+import com.github.therapi.runtimejavadoc.MethodJavadoc;
+import com.github.therapi.runtimejavadoc.ParamJavadoc;
+import com.github.therapi.runtimejavadoc.RuntimeJavadoc;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
+/// Describes a single "variable condition" (varcond) or taclet-builder command that can be
+/// used inside taclet definitions, together with metadata needed to parse, validate, and
+/// document its usage.
+///
+/// An instance of this interface bundles together:
+///
+/// - the command's [`name`][#name()] as it appears in taclet source files,
+/// - the expected [`argument types`][#argumentTypes()],
+/// - whether the command [`supports negation`][#isNegationSupported()] (i.e. an
+/// additional trailing `boolean` constructor argument),
+/// - and Javadoc-derived documentation for both the command itself and its individual
+/// arguments, extracted via reflection from the backing implementation class.
+///
+/// Instances are typically created via the [#createVarcondInfo] factory methods rather
+/// than by implementing this interface directly.
+///
+/// @author Alexander Weigl
+/// @version 1 (23.08.26)
+@NullMarked
+public interface TacletBuilderCommandInfo {
+
+    /// Returns the name of this command as used in taclet source files.
+    ///
+    /// @return the command name, never `null`
+    String name();
+
+    /// Returns the declared types of the arguments accepted by this command, in the order
+    /// they must appear in the taclet source.
+    ///
+    /// @return the array of argument types
+    ArgumentType[] argumentTypes();
+
+    /// Returns the names of the arguments as declared in the backing implementation's
+    /// constructor (or as documented via Javadoc, if available).
+    ///
+    /// Resolving the argument names requires reflecting on the implementation class and is
+    /// performed lazily on first access.
+    ///
+    /// @return the array of argument names, in the same order as [#argumentTypes()]
+    String[] argNames();
+
+    /// Indicates whether this command supports an optional trailing negation flag, i.e.
+    /// whether the backing implementation class has a constructor whose parameters are the
+    /// declared [`argument types`][#argumentTypes()] followed by an additional
+    /// `boolean` parameter.
+    ///
+    /// @return `true` if negation is supported, `false` otherwise
+    boolean isNegationSupported();
+
+    /// Returns the class-level Javadoc documentation extracted from the backing
+    /// implementation class. This is typically used as the general description of what the
+    /// command does.
+    ///
+    /// @return the class-level Javadoc, never `null`
+    ClassJavadoc getGeneralDocumentation();
+
+    /// Returns the Javadoc documentation of the specific constructor that matches this
+    /// command's argument types (and negation flag, if supported). This is typically used
+    /// to document the individual arguments of the command.
+    ///
+    /// @return the matching constructor's Javadoc, or a documentation object with empty
+    /// fields if no Javadoc could be resolved
+    MethodJavadoc getArgumentInformation();
+
+    /// Creates a [TacletBuilderCommandInfo] for a command whose negation support is
+    /// determined automatically by inspecting the constructors of `clazz`.
+    ///
+    /// @param name the name of the command as used in taclet source files
+    /// @param clazz the implementation class backing this command
+    /// @param types the expected argument types, in declaration order
+    /// @return a new [TacletBuilderCommandInfo] instance
+    static TacletBuilderCommandInfo createVarcondInfo(String name, Class<?> clazz,
+            ArgumentType... types) {
+        return new TacletBuilderCommandInfoImpl(name, types, clazz, null);
+    }
+
+    /// Creates a [TacletBuilderCommandInfo] for a command with an explicitly specified
+    /// negation support flag, instead of determining it via reflection.
+    ///
+    /// @param name the name of the command as used in taclet source files
+    /// @param clazz the implementation class backing this command
+    /// @param negationSupported whether the command supports a trailing negation argument
+    /// @param types the expected argument types, in declaration order
+    /// @return a new [TacletBuilderCommandInfo] instance
+    static TacletBuilderCommandInfo createVarcondInfo(String name, Class<?> clazz,
+            Boolean negationSupported, ArgumentType... types) {
+        return new TacletBuilderCommandInfoImpl(name, types, clazz, negationSupported);
+    }
+}
+
+
+/// Default implementation of [TacletBuilderCommandInfo].
+///
+/// Argument names and documentation are resolved lazily, on first access, by reflecting on
+/// the backing implementation class ([#clazz]) and looking up its runtime Javadoc via
+/// [RuntimeJavadoc].
+class TacletBuilderCommandInfoImpl implements TacletBuilderCommandInfo {
+    /// The name of the command as used in taclet source files.
+    public final String name;
+    /// The expected argument types, in declaration order.
+    private final ArgumentType[] argTypes;
+    /// The implementation class backing this command, used for reflection-based lookups.
+    private final Class<?> clazz;
+    /// Whether this command supports a trailing negation argument. `null` until
+    /// lazily resolved via [#isNegationSupported()].
+    private @Nullable Boolean isNegationSupported;
+    /// The resolved argument names, or `null` until [#findDocumentation()] has run.
+    private String @Nullable [] argNames;
+    /// The resolved class-level Javadoc, or `null` until [#findDocumentation()] has run.
+    private @Nullable ClassJavadoc generalDocumentation;
+    /// The resolved constructor Javadoc, or `null` until [#findDocumentation()] has run.
+    private @Nullable MethodJavadoc argumentDocumentation;
+
+    /// Creates a new command descriptor.
+    ///
+    /// @param name the name of the command as used in taclet source files
+    /// @param types the expected argument types, in declaration order
+    /// @param clazz the implementation class backing this command
+    /// @param negationSupported whether the command supports a trailing negation argument,
+    /// or `null` to determine this lazily via reflection
+    public TacletBuilderCommandInfoImpl(String name, ArgumentType[] types, Class<?> clazz,
+            @Nullable Boolean negationSupported) {
+        this.name = name;
+        argTypes = types;
+        this.clazz = clazz;
+        isNegationSupported = negationSupported;
+    }
+
+    @Override
+    public String name() {
+        return name;
+    }
+
+    @Override
+    public ArgumentType[] argumentTypes() {
+        return argTypes;
+    }
+
+    @Override
+    public String[] argNames() {
+        if (argNames == null) {
+            findDocumentation();
+        }
+        return argNames;
+    }
+
+    @Override
+    public boolean isNegationSupported() {
+        if (isNegationSupported == null) {
+            isNegationSupported = lastArgumentOfFirstConstructorIsBoolean(clazz, argTypes);
+        }
+        return isNegationSupported;
+    }
+
+    @Override
+    public ClassJavadoc getGeneralDocumentation() {
+        if (generalDocumentation == null) {
+            findDocumentation();
+        }
+        return generalDocumentation;
+    }
+
+    @Override
+    public MethodJavadoc getArgumentInformation() {
+        if (argumentDocumentation == null) {
+            findDocumentation();
+        }
+        return argumentDocumentation;
+    }
+
+    /// Computes the parameter types of the constructor that this command's arguments (and,
+    /// if applicable, its negation flag) would map to.
+    ///
+    /// @return the array of expected constructor parameter types
+    Class<?>[] getConstructorClasses() {
+        return getConstructorClasses(argTypes, isNegationSupported());
+    }
+
+    /// Resolves and caches [#argNames], [#generalDocumentation], and
+    /// [#argumentDocumentation] by reflecting on [#clazz] and looking up its
+    /// matching constructor's runtime Javadoc.
+    ///
+    /// If no constructor matching [#getConstructorClasses()] can be found, argument
+    /// names are filled with empty strings and empty documentation placeholders are used
+    /// instead of failing.
+    private void findDocumentation() {
+        ClassJavadoc classDoc = RuntimeJavadoc.getJavadoc(clazz.getName());
+        if (classDoc == null) {
+            // The class was not processed by the therapi javadoc scribe; use empty
+            // documentation instead of failing.
+            classDoc = ClassJavadoc.createEmpty(clazz.getName());
+        }
+        generalDocumentation = classDoc;
+
+        final var constr = findConstructor(clazz, getConstructorClasses());
+        if (constr == null) {
+            argNames = new String[argTypes.length];
+            Arrays.fill(argNames, "");
+            argumentDocumentation =
+                MethodJavadoc.createEmpty((Constructor<?>) null);
+            return;
+        }
+
+        final var constructorDeclaration = classDoc.getConstructors()
+                .stream().filter(it -> it.matches(constr)).findAny();
+
+        final var parameters = constr.getParameters();
+        argNames = new String[argTypes.length];
+        for (int i = 0; i < argTypes.length && i < parameters.length; i++) {
+            argNames[i] = parameters[i].getName();
+        }
+
+        constructorDeclaration.ifPresent(it -> {
+            List<ParamJavadoc> params = it.getParams();
+            for (int i = 0; i < argNames.length && i < params.size(); i++) {
+                argNames[i] = params.get(i).getName();
+            }
+        });
+
+        argumentDocumentation = constructorDeclaration
+                .orElse(MethodJavadoc.createEmpty((Constructor<?>) null));
+        // endregion
+    }
+
+
+    /// Determines whether the backing implementation class supports an optional trailing
+    /// negation flag, i.e. whether it has a constructor whose parameters are the declared
+    /// [`argument types`][#argumentTypes()] followed by an additional `boolean` parameter.
+    ///
+    /// First, a constructor is searched whose parameter types are compatible with the
+    /// declared [ArgumentType]s; if that succeeds, the presence of the trailing `boolean`
+    /// decides negation support. If no type-compatible constructor can be found — the
+    /// [ArgumentType]s only loosely approximate the actual parameter types (e.g.,
+    /// `\isConstant` declares an [ArgumentType.VARIABLE], but `ConstantCondition`'s
+    /// constructor takes a `JAbstractSortedOperator`) — the check falls back to the
+    /// original, lenient behavior: the last parameter of the first declared public
+    /// constructor must be a `boolean`.
+    ///
+    /// @param clazz the implementation class to inspect
+    /// @param argTypes the declared argument types
+    /// @return `true` if negation is supported, `false` otherwise
+    private static boolean lastArgumentOfFirstConstructorIsBoolean(
+            Class<?> clazz, ArgumentType[] argTypes) {
+        if (findTypedConstructor(clazz, getConstructorClasses(argTypes, true)) != null) {
+            return true;
+        }
+        if (findTypedConstructor(clazz, getConstructorClasses(argTypes, false)) != null) {
+            return false;
+        }
+        try {
+            Class<?>[] types = clazz.getConstructors()[0].getParameterTypes();
+            return types[types.length - 1] == Boolean.class
+                    || types[types.length - 1] == Boolean.TYPE;
+        } catch (ArrayIndexOutOfBoundsException e) {
+            return false;
+        }
+    }
+
+    /// Searches a constructor of `clazz` whose parameter types are compatible with
+    /// `constructorClasses`: each actual parameter type must be assignable to the
+    /// expected class, i.e. be a subtype of it.
+    ///
+    /// @param clazz the implementation class to inspect
+    /// @param constructorClasses the expected parameter classes
+    /// @return the matching constructor, or `null` if none is type-compatible
+    private static @Nullable Constructor<?> findTypedConstructor(Class<?> clazz,
+            Class<?>[] constructorClasses) {
+        c: for (var constructor : clazz.getConstructors()) {
+            if (constructor.getParameterCount() != constructorClasses.length)
+                continue;
+            final var parameterTypes = constructor.getParameterTypes();
+            for (var i = 0; i < parameterTypes.length; i++) {
+                if (!constructorClasses[i].isAssignableFrom(parameterTypes[i])) {
+                    continue c;
+                }
+            }
+            return constructor;
+        }
+        return null;
+    }
+
+    /// Looks up a constructor of `clazz` for documentation purposes: a type-compatible
+    /// constructor is preferred; if none exists, a constructor with the same number of
+    /// parameters is used, since the [ArgumentType] classes only approximate the actual
+    /// parameter types.
+    ///
+    /// @param clazz the implementation class to inspect
+    /// @param constructorClasses the expected parameter classes
+    /// @return the best matching constructor, or `null` if none is found
+    private static @Nullable Constructor<?> findConstructor(Class<?> clazz,
+            Class<?>[] constructorClasses) {
+        var constructor = findTypedConstructor(clazz, constructorClasses);
+        if (constructor != null) {
+            return constructor;
+        }
+        for (var c : clazz.getConstructors()) {
+            if (c.getParameterCount() == constructorClasses.length) {
+                return c;
+            }
+        }
+        return null;
+    }
+
+    /// Builds the array of constructor parameter types corresponding to `argTypes`,
+    /// optionally appending `boolean.class` for negation support.
+    ///
+    /// @param argTypes the declared argument types
+    /// @param isNegationSupported whether a trailing `boolean` parameter should be
+    /// appended for negation support
+    /// @return the resulting array of constructor parameter types
+    static Class<?>[] getConstructorClasses(ArgumentType[] argTypes, boolean isNegationSupported) {
+        Class<?>[] clazzes = new Class[argTypes.length + (isNegationSupported ? 1 : 0)];
+        for (int i = 0; i < argTypes.length; i++) {
+            clazzes[i] = argTypes[i].clazz;
+        }
+
+        if (isNegationSupported)
+            clazzes[clazzes.length - 1] = Boolean.TYPE;
+        return clazzes;
+    }
+
+}
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java
index 99c439548ff..753d2261880 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java
@@ -15,17 +15,19 @@
 import de.uka.ilkd.key.logic.op.JOperatorSV;
 import de.uka.ilkd.key.logic.op.ProgramSV;
 import de.uka.ilkd.key.logic.sort.GenericSort;
+import de.uka.ilkd.key.rule.NewVarcond;
 import de.uka.ilkd.key.rule.conditions.*;
 import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder;
 
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.VariableCondition;
-
-import org.jspecify.annotations.NonNull;
+import org.key_project.prover.rules.conditions.NewDependingOn;
+import org.key_project.prover.rules.conditions.NotFreeIn;
 
 import static de.uka.ilkd.key.nparser.varexp.ArgumentType.SORT;
 import static de.uka.ilkd.key.nparser.varexp.ArgumentType.TYPE_RESOLVER;
+import static de.uka.ilkd.key.nparser.varexp.TacletBuilderCommandInfo.createVarcondInfo;
 import static de.uka.ilkd.key.rule.conditions.TypeComparisonCondition.Mode.*;
 
 /**
@@ -37,6 +39,7 @@
  */
 public class TacletBuilderManipulators {
     // region Factories
+
     // Short cut for argument types
     private static final ArgumentType TR = TYPE_RESOLVER;
     private static final ArgumentType KJT = ArgumentType.JAVA_TYPE;
@@ -51,20 +54,14 @@ public class TacletBuilderManipulators {
     private static final ArgumentType T = ArgumentType.TERM;
 
 
-    /**
-     *
-     */
     public static final AbstractConditionBuilder ABSTRACT_OR_INTERFACE =
         new ConstructorBasedBuilder("isAbstractOrInterface", AbstractOrInterfaceType.class, TR);
 
     public static final AbstractConditionBuilder FINAL_TYPE =
         new ConstructorBasedBuilder("isFinal", FinalTypeVarCond.class, TR);
 
-    /**
-     *
-     */
     public static final AbstractConditionBuilder SAME =
-        new AbstractConditionBuilder("same", TR, TR) {
+        new AbstractConditionBuilder("same", TypeComparisonCondition.class, true, TR, TR) {
             @Override
             public TypeComparisonCondition build(Object[] arguments, List<String> parameters,
                     boolean negated) {
@@ -74,11 +71,8 @@ public TypeComparisonCondition build(Object[] arguments, List<String> parameters
             }
         };
 
-    /**
-     *
-     */
     public static final AbstractConditionBuilder IS_SUBTYPE =
-        new AbstractConditionBuilder("sub", TR, TR) {
+        new AbstractConditionBuilder("sub", TypeComparisonCondition.class, true, TR, TR) {
             @Override
             public TypeComparisonCondition build(Object[] arguments, List<String> parameters,
                     boolean negated) {
@@ -92,9 +86,9 @@ public TypeComparisonCondition build(Object[] arguments, List<String> parameters
      *
      */
     public static final AbstractConditionBuilder STRICT =
-        new AbstractConditionBuilder("scrictSub", TR, TR) {
+        new AbstractConditionBuilder("scrictSub", TypeComparisonCondition.class, false, TR, TR) {
             @Override
-            public boolean isSuitableFor(@NonNull String name) {
+            public boolean isSuitableFor(String name) {
                 if (super.isSuitableFor(name)) {
                     return true;
                 }
@@ -117,7 +111,8 @@ public TypeComparisonCondition build(Object[] arguments, List<String> parameters
      *
      */
     public static final AbstractConditionBuilder DISJOINT_MODULO_NULL =
-        new AbstractConditionBuilder("disjointModuloNull", TR, TR) {
+        new AbstractConditionBuilder("disjointModuloNull", TypeComparisonCondition.class, false, TR,
+            TR) {
             @Override
             public TypeComparisonCondition build(Object[] arguments, List<String> parameters,
                     boolean negated) {
@@ -139,7 +134,8 @@ public TypeComparisonCondition build(Object[] arguments, List<String> parameters
      *
      */
     public static final AbstractTacletBuilderCommand NEW_JAVATYPE =
-        new AbstractTacletBuilderCommand("new", SV, KJT) {
+        new AbstractTacletBuilderCommand(
+            createVarcondInfo("new", NewVarcond.class, false, SV, KJT)) {
             @Override
             public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
                     List<String> parameters, boolean negated) {
@@ -152,7 +148,8 @@ public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
         };
 
     public static final AbstractTacletBuilderCommand NEW_VAR =
-        new AbstractTacletBuilderCommand("new", SV, SORT) {
+        new AbstractTacletBuilderCommand(
+            createVarcondInfo("new", NewVarcond.class, false, SV, SORT)) {
             @Override
             public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
                     List<String> parameters, boolean negated) {
@@ -169,8 +166,8 @@ public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
         "newLocalVars", NewLocalVarsCondition.class, SV, SV, SV, SV);
 
     static class NotFreeInTacletBuilderCommand extends AbstractTacletBuilderCommand {
-        public NotFreeInTacletBuilderCommand(@NonNull ArgumentType... argumentsTypes) {
-            super("notFreeIn", argumentsTypes);
+        public NotFreeInTacletBuilderCommand(ArgumentType... argumentsTypes) {
+            super(createVarcondInfo("notFreeIn", NotFreeIn.class, true, argumentsTypes));
         }
 
         @Override
@@ -196,7 +193,8 @@ public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
 
     private static final List<TacletBuilderCommand> tacletBuilderCommands = new ArrayList<>(32);
     public static final AbstractTacletBuilderCommand NEW_TYPE_OF =
-        new AbstractTacletBuilderCommand("newTypeOf", SV, SV) {
+        new AbstractTacletBuilderCommand(
+            createVarcondInfo("newTypeOf", NewVarcond.class, false, SV, SV)) {
 
             @Override
             public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
@@ -210,7 +208,8 @@ public void apply(TacletBuilder<?> tacletBuilder, Object[] arguments,
             }
         };
     public static final AbstractTacletBuilderCommand NEW_DEPENDING_ON =
-        new AbstractTacletBuilderCommand("newDependingOn", SV, SV) {
+        new AbstractTacletBuilderCommand(
+            createVarcondInfo("newDependingOn", NewDependingOn.class, false, SV, SV)) {
             @Override
             public void apply(TacletBuilder<?> tb, Object[] arguments, List<String> parameters,
                     boolean negated) {
@@ -237,7 +236,8 @@ public void apply(TacletBuilder<?> tb, Object[] arguments, List<String> paramete
     public static final AbstractConditionBuilder ARRAY =
         new ConstructorBasedBuilder("isArray", ArrayTypeCondition.class, SV);
     public static final AbstractConditionBuilder REFERENCE_ARRAY =
-        new AbstractConditionBuilder("isReferenceArray", SV) {
+        new AbstractConditionBuilder("isReferenceArray", ArrayComponentTypeCondition.class, true,
+            SV) {
             @Override
             public VariableCondition build(Object[] arguments, List<String> parameters,
                     boolean negated) {
@@ -253,7 +253,7 @@ public VariableCondition build(Object[] arguments, List<String> parameters,
     public static final AbstractConditionBuilder THIS_REFERENCE =
         new ConstructorBasedBuilder("isThisReference", IsThisReference.class, SV);
     public static final AbstractConditionBuilder REFERENCE =
-        new AbstractConditionBuilder("isReference", TR) {
+        new AbstractConditionBuilder("isReference", TypeCondition.class, true, TR) {
             @Override
             public VariableCondition build(Object[] arguments, List<String> parameters,
                     boolean negated) {
@@ -262,7 +262,7 @@ public VariableCondition build(Object[] arguments, List<String> parameters,
             }
         };
     public static final AbstractConditionBuilder ENUM_TYPE =
-        new ConstructorBasedBuilder("reference", EnumTypeCondition.class, SV, SV, SV);
+        new ConstructorBasedBuilder("reference", EnumTypeCondition.class, SV);
     public static final AbstractConditionBuilder CONTAINS_ASSIGNMENT =
         new ConstructorBasedBuilder("containsAssignment", ContainsAssignmentCondition.class, SV);
     public static final AbstractConditionBuilder FIELD_TYPE =
@@ -303,8 +303,8 @@ public VariableCondition build(Object[] arguments, List<String> parameters,
     static class JavaTypeToSortConditionBuilder extends AbstractConditionBuilder {
         private final boolean elmen;
 
-        public JavaTypeToSortConditionBuilder(@NonNull String triggerName, boolean forceElmentary) {
-            super(triggerName, SV, SORT);
+        public JavaTypeToSortConditionBuilder(String triggerName, boolean forceElmentary) {
+            super(triggerName, JavaTypeToSortCondition.class, false, SV, SORT);
             this.elmen = forceElmentary;
         }
 
@@ -333,7 +333,7 @@ public VariableCondition build(Object[] arguments, List<String> parameters,
         new ConstructorBasedBuilder("hasLabel", TermLabelCondition.class, TSV, S);
     // endregion
     public static final AbstractConditionBuilder STORE_TERM_IN =
-        new AbstractConditionBuilder("storeTermIn", SV, T) {
+        new AbstractConditionBuilder("storeTermIn", StoreTermInCondition.class, false, SV, T) {
             @Override
             public VariableCondition build(Object[] arguments, List<String> parameters,
                     boolean negated) {
@@ -351,7 +351,7 @@ public VariableCondition build(Object[] arguments, List<String> parameters,
     public static final AbstractConditionBuilder GET_FREE_INVARIANT = new ConstructorBasedBuilder(
         "\\getFreeInvariant", LoopFreeInvariantCondition.class, PV, SV, SV);
     public static final AbstractConditionBuilder GET_VARIANT =
-        new AbstractConditionBuilder("\\getVariant", PV, SV) {
+        new AbstractConditionBuilder("\\getVariant", LoopVariantCondition.class, false, PV, SV) {
             @Override
             public VariableCondition build(Object[] arguments, List<String> parameters,
                     boolean negated) {
@@ -360,7 +360,7 @@ public VariableCondition build(Object[] arguments, List<String> parameters,
             }
         };
     public static final AbstractConditionBuilder IS_LABELED =
-        new AbstractConditionBuilder("isLabeled", PV) {
+        new AbstractConditionBuilder("isLabeled", IsLabeledCondition.class, true, PV) {
             @Override
             public IsLabeledCondition build(Object[] arguments, List<String> parameters,
                     boolean negated) {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/package-info.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/package-info.java
new file mode 100644
index 00000000000..de15cc91730
--- /dev/null
+++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/package-info.java
@@ -0,0 +1,9 @@
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (23.08.26)
+ */
+@NullMarked
+package de.uka.ilkd.key.nparser.varexp;
+
+import org.jspecify.annotations.NullMarked;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java
index 31cc211f35d..40892e17faa 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AbstractOrInterfaceType.java
@@ -21,6 +21,12 @@ public final class AbstractOrInterfaceType extends VariableConditionAdapter {
     private final TypeResolver resolver;
     private final boolean negated;
 
+    /**
+     * Instantiates a new abstract-or-interface condition.
+     *
+     * @param tr the type resolver for the type to check
+     * @param negation whether the condition is negated ({@code \not isAbstractOrInterface})
+     */
     public AbstractOrInterfaceType(TypeResolver tr, boolean negation) {
         this.resolver = tr;
         this.negated = negation;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java
index 9aa8df14667..99559995871 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/AlternativeVariableCondition.java
@@ -22,6 +22,12 @@ public final class AlternativeVariableCondition extends VariableConditionAdapter
 
     private final VariableConditionAdapter delegate0, delegate1;
 
+    /**
+     * Instantiates a new alternative (disjunction) of two variable conditions.
+     *
+     * @param delegate0 the first of the two conditions
+     * @param delegate1 the second of the two conditions
+     */
     public AlternativeVariableCondition(VariableConditionAdapter delegate0,
             VariableConditionAdapter delegate1) {
         this.delegate0 = delegate0;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ArrayLengthCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ArrayLengthCondition.java
index 039f9675eb6..238124fa313 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ArrayLengthCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ArrayLengthCondition.java
@@ -15,12 +15,25 @@
 import org.key_project.logic.op.sv.SchemaVariable;
 
 
+/**
+ * A variable condition for the taclet construct {@code \isArrayLength}, checking that a schema
+ * variable is instantiated with the implicit array length attribute.
+ *
+ * @author Michael Kirsten
+ */
 public final class ArrayLengthCondition extends VariableConditionAdapter {
 
     private final SchemaVariable reference;
     private final boolean negation;
 
 
+    /**
+     * Instantiates a new array length condition.
+     *
+     * @param reference the schema variable which must be instantiated with the array length
+     *        attribute of some array type
+     * @param negation whether the condition is negated ({@code \not isArrayLength})
+     */
     public ArrayLengthCondition(SchemaVariable reference, boolean negation) {
         this.reference = reference;
         this.negation = negation;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ConstantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ConstantCondition.java
index 3181fde6b07..f938376ab5d 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ConstantCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ConstantCondition.java
@@ -26,6 +26,13 @@ public class ConstantCondition extends VariableConditionAdapter {
     private final JAbstractSortedOperator t;
     private final boolean negated;
 
+    /**
+     * Instantiates a new constant condition.
+     *
+     * @param t the term or formula schema variable which must be instantiated with a constant
+     *        (zero-arity) term
+     * @param negated whether the condition is negated ({@code \not isConstant})
+     */
     public ConstantCondition(JAbstractSortedOperator t, boolean negated) {
         this.t = t;
         this.negated = negated;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentFields.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentFields.java
index a6f5910f3c1..4e94eb2934b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentFields.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentFields.java
@@ -22,6 +22,13 @@ public final class DifferentFields extends VariableConditionAdapter {
 
     private final SchemaVariable var1, var2;
 
+    /**
+     * Instantiates a new different-fields condition.
+     *
+     * @param var1 the first schema variable; both instantiations must differ in their top-level
+     *        unique function symbol
+     * @param var2 the second schema variable
+     */
     public DifferentFields(SchemaVariable var1, SchemaVariable var2) {
         this.var1 = var1;
         this.var2 = var2;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentInstantiationCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentInstantiationCondition.java
index 187b5132bf1..d3a81a81284 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentInstantiationCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DifferentInstantiationCondition.java
@@ -13,10 +13,22 @@
 import org.key_project.logic.op.sv.SchemaVariable;
 
 
+/**
+ * A variable condition for the taclet construct {@code \different}, ensuring that two schema
+ * variables are instantiated with distinct elements.
+ *
+ * @author Michael Kirsten
+ */
 public final class DifferentInstantiationCondition extends VariableConditionAdapter {
 
     private final SchemaVariable var1, var2;
 
+    /**
+     * Instantiates a new different-instantiation condition.
+     *
+     * @param var1 the first schema variable
+     * @param var2 the second schema variable; both must not be instantiated with the same element
+     */
     public DifferentInstantiationCondition(SchemaVariable var1, SchemaVariable var2) {
         this.var1 = var1;
         this.var2 = var2;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java
index 9e714dd60de..a0ddf1788bb 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java
@@ -27,11 +27,26 @@
 import org.key_project.prover.rules.instantiation.MatchResultInfo;
 
 
+/**
+ * A variable condition for the taclet construct {@code \dropEffectlessElementaries}: given an
+ * update and a target term, it computes the update with all elementary updates removed that do not
+ * affect (are not "relevant" for) the target term, and binds the result to a third schema variable.
+ *
+ * @author Michael Kirsten
+ */
 public final class DropEffectlessElementariesCondition implements VariableCondition {
     private final UpdateSV u;
     private final SchemaVariable x;
     private final SchemaVariable result;
 
+    /**
+     * Instantiates a new drop-effectless-elementaries condition.
+     *
+     * @param u the update schema variable whose instantiation is simplified
+     * @param x the schema variable holding the target term which determines the relevant locations
+     * @param x2 the schema variable to which the simplified update application
+     *        {@code u(x)} is bound
+     */
     public DropEffectlessElementariesCondition(UpdateSV u, SchemaVariable x, SchemaVariable x2) {
         this.u = u;
         this.x = x;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java
index 9aad185f8ea..02769045351 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java
@@ -23,6 +23,13 @@
 import org.key_project.util.collection.Pair;
 
 
+/**
+ * A variable condition for the taclet construct {@code \dropEffectlessStores}: it removes all
+ * {@code store} operations from a heap term that are overwritten by later {@code store} operations
+ * on the same location, and binds the simplified heap to a result schema variable.
+ *
+ * @author Michael Kirsten
+ */
 public final class DropEffectlessStoresCondition implements VariableCondition {
     private final TermSV h;
     private final TermSV o;
@@ -30,6 +37,16 @@ public final class DropEffectlessStoresCondition implements VariableCondition {
     private final TermSV x;
     private final TermSV result;
 
+    /**
+     * Instantiates a new drop-effectless-stores condition.
+     *
+     * @param h the term schema variable for the heap on which the store operation is performed
+     * @param o the term schema variable for the object of the store operation
+     * @param f the term schema variable for the field of the store operation
+     * @param x the term schema variable for the value written by the store operation
+     * @param result the term schema variable to which the heap with all effectless stores removed
+     *        is bound
+     */
     public DropEffectlessStoresCondition(TermSV h, TermSV o, TermSV f, TermSV x, TermSV result) {
         this.h = h;
         this.o = o;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java
index 479d698190a..5d224fc122c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java
@@ -19,12 +19,28 @@
 import org.key_project.prover.rules.instantiation.MatchResultInfo;
 
 
+/**
+ * A variable condition for the taclet construct {@code \equalUnique}: checks that two term schema
+ * variables are instantiated with (distinct) applications of functions marked as {@code unique},
+ * and if so binds a formula schema variable to the equation of both terms.
+ *
+ * @author Michael Kirsten
+ */
 public final class EqualUniqueCondition implements VariableCondition {
     private final TermSV t;
     private final TermSV t2;
     private final FormulaSV res;
 
 
+    /**
+     * Instantiates a new equal-unique condition.
+     *
+     * @param t the first term schema variable; its instantiation must be the application of a
+     *        unique function
+     * @param t2 the second term schema variable; its instantiation must be the application of a
+     *        unique function
+     * @param res the formula schema variable to which the equation {@code t = t2} is bound
+     */
     public EqualUniqueCondition(TermSV t, TermSV t2, FormulaSV res) {
         this.t = t;
         this.t2 = t2;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java
index 3aac2f76438..fbc5cf47584 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java
@@ -34,6 +34,13 @@ public final class FieldTypeToSortCondition implements VariableCondition {
     private final SchemaVariable exprOrTypeSV;
     private final GenericSort sort;
 
+    /**
+     * Instantiates a new field-type condition.
+     *
+     * @param exprOrTypeSV the expression or type schema variable whose instantiation must be a
+     *        field constant
+     * @param sort the generic sort which is instantiated with the referred type of the field
+     */
     public FieldTypeToSortCondition(final JOperatorSV exprOrTypeSV, final GenericSort sort) {
         this.exprOrTypeSV = exprOrTypeSV;
         this.sort = sort;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FinalTypeVarCond.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FinalTypeVarCond.java
index 1e70a06df11..8ca23730f80 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FinalTypeVarCond.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FinalTypeVarCond.java
@@ -30,6 +30,12 @@ public final class FinalTypeVarCond extends VariableConditionAdapter {
     private final TypeResolver resolver;
     private final boolean negated;
 
+    /**
+     * Instantiates a new final-type condition.
+     *
+     * @param tr the type resolver for the type to check
+     * @param negation whether the condition is negated ({@code \not isFinal})
+     */
     public FinalTypeVarCond(TypeResolver tr, boolean negation) {
         this.resolver = tr;
         this.negated = negation;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FreeLabelInVariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FreeLabelInVariableCondition.java
index 8cb9d637c9e..3036ca51a6a 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FreeLabelInVariableCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FreeLabelInVariableCondition.java
@@ -15,6 +15,12 @@
 import org.key_project.logic.op.sv.SchemaVariable;
 
 
+/**
+ * A variable condition for the taclet construct {@code \freeLabelIn}, checking whether a program
+ * label occurs freely in a Java program (block).
+ *
+ * @author Michael Kirsten
+ */
 public final class FreeLabelInVariableCondition extends VariableConditionAdapter {
 
     private final SchemaVariable label;
@@ -22,6 +28,14 @@ public final class FreeLabelInVariableCondition extends VariableConditionAdapter
     private final boolean negated;
     private final FreeLabelFinder freeLabelFinder = new FreeLabelFinder();
 
+    /**
+     * Instantiates a new free-label-in condition.
+     *
+     * @param label the schema variable which must be instantiated with a program label
+     * @param statement the schema variable which must be instantiated with a program element
+     *        (statement)
+     * @param negated whether the condition is negated ({@code \not freeLabelIn})
+     */
     public FreeLabelInVariableCondition(SchemaVariable label, SchemaVariable statement,
             boolean negated) {
         this.label = label;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java
index ed8cbf111b1..26eb90ef761 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java
@@ -35,6 +35,14 @@ public class HasLoopInvariantCondition implements VariableCondition {
     private final ProgramSV loopStmtSV;
     private final SchemaVariable modalitySV;
 
+    /**
+     * Instantiates a new has-loop-invariant condition.
+     *
+     * @param loopStmtSV the program schema variable which must be instantiated with a loop
+     *        statement
+     * @param modalitySV the schema variable for the modality kind determining the applicable heap
+     *        context
+     */
     public HasLoopInvariantCondition(ProgramSV loopStmtSV, SchemaVariable modalitySV) {
         this.loopStmtSV = loopStmtSV;
         this.modalitySV = modalitySV;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/InStrictFp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/InStrictFp.java
index 3a109b01923..72a58a73056 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/InStrictFp.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/InStrictFp.java
@@ -23,6 +23,11 @@ public final class InStrictFp extends VariableConditionAdapter {
 
     private final boolean negated;
 
+    /**
+     * Instantiates a new strict-fp condition.
+     *
+     * @param negation whether the condition is negated ({@code \not isInStrictFp})
+     */
     public InStrictFp(boolean negation) {
         this.negated = negation;
     }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java
index a572aa2c281..0a16db06fb9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java
@@ -29,6 +29,13 @@ public class IsLabeledCondition implements VariableCondition {
     private final boolean negated;
     private final ProgramSV stmtSV;
 
+    /**
+     * Instantiates a new is-labeled condition.
+     *
+     * @param stmtSV the program schema variable which must be instantiated with a labeled
+     *        statement
+     * @param negated whether the condition is negated ({@code \not isLabeled})
+     */
     public IsLabeledCondition(ProgramSV stmtSV, boolean negated) {
         this.stmtSV = stmtSV;
         this.negated = negated;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsThisReference.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsThisReference.java
index 973ae44c29e..5e790c5a459 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsThisReference.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsThisReference.java
@@ -17,13 +17,21 @@
 
 
 /**
- * This variable condition checks if a given type denotes an abstract class or interface type.
+ * This variable condition checks if a program variable is instantiated with a {@code this}
+ * reference.
  */
 public final class IsThisReference extends VariableConditionAdapter {
 
     private final boolean negated;
     private final ParsableVariable var;
 
+    /**
+     * Instantiates a new this-reference condition.
+     *
+     * @param var the program schema variable which must be instantiated with a {@code this}
+     *        reference
+     * @param negation whether the condition is negated ({@code \not isThisReference})
+     */
     public IsThisReference(ParsableVariable var, boolean negation) {
         this.negated = negation;
         this.var = var;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java
index 1a2c856b070..208210d7a81 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java
@@ -36,6 +36,14 @@ public final class JavaTypeToSortCondition implements VariableCondition {
     private final boolean elemSort;
 
 
+    /**
+     * Instantiates a new java-type-to-sort condition.
+     *
+     * @param exprOrTypeSV the expression or type schema variable whose instantiation determines
+     *        the sort
+     * @param sort the generic sort which is instantiated with the sort of the instantiation
+     * @param elemSort whether the elementary sort is to be used for array types
+     */
     public JavaTypeToSortCondition(final JOperatorSV exprOrTypeSV, final GenericSort sort,
             final boolean elemSort) {
         this.exprOrTypeSV = exprOrTypeSV;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java
index 7234a7bddf7..b11432ab50f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java
@@ -22,6 +22,14 @@ public final class LocalVariableCondition extends VariableConditionAdapter {
     private final SchemaVariable var;
     private final boolean neg;
 
+    /**
+     * Instantiates a new local-variable condition.
+     *
+     * @param var the schema variable which must be instantiated with a local (non-member) program
+     *        variable
+     * @param neg whether the condition is negated ({@code \not isLocalVariable})
+     * @throws IllegalArgumentException if the given schema variable is not a {@link ProgramSV}
+     */
     public LocalVariableCondition(SchemaVariable var, boolean neg) {
         this.var = var;
         this.neg = neg;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java
index f7f1ed52f3c..2707f55bb3b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java
@@ -38,6 +38,15 @@ public class LoopFreeInvariantCondition implements VariableCondition {
     private final SchemaVariable modalitySV;
     private final SchemaVariable invSV;
 
+    /**
+     * Instantiates a new free-loop-invariant condition.
+     *
+     * @param loopStmtSV the program schema variable which must be instantiated with a loop
+     *        statement
+     * @param modalitySV the schema variable for the modality kind determining the applicable heap
+     *        context
+     * @param invSV the schema variable to which the free loop invariant is bound
+     */
     public LoopFreeInvariantCondition(ProgramSV loopStmtSV, SchemaVariable modalitySV,
             SchemaVariable invSV) {
         this.loopStmtSV = loopStmtSV;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java
index 833f4e1ccb7..fad27789b67 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java
@@ -37,6 +37,15 @@ public class LoopInvariantCondition implements VariableCondition {
     private final SchemaVariable modalitySV;
     private final SchemaVariable invSV;
 
+    /**
+     * Instantiates a new loop-invariant condition.
+     *
+     * @param loopStmtSV the program schema variable which must be instantiated with a loop
+     *        statement
+     * @param modalitySV the schema variable for the modality kind determining the applicable heap
+     *        context
+     * @param invSV the schema variable to which the loop invariant is bound
+     */
     public LoopInvariantCondition(ProgramSV loopStmtSV, SchemaVariable modalitySV,
             SchemaVariable invSV) {
         this.loopStmtSV = loopStmtSV;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java
index fc23a3bbd37..7e515e0d8a2 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopVariantCondition.java
@@ -26,6 +26,13 @@ public class LoopVariantCondition implements VariableCondition {
     private final SchemaVariable loopStmtSV;
     private final SchemaVariable variantSV;
 
+    /**
+     * Instantiates a new loop-variant condition.
+     *
+     * @param loopStmtSV the program schema variable which must be instantiated with a loop
+     *        statement
+     * @param variantSV the schema variable to which the loop variant is bound
+     */
     public LoopVariantCondition(ProgramSV loopStmtSV, SchemaVariable variantSV) {
         this.loopStmtSV = loopStmtSV;
         this.variantSV = variantSV;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java
index d2a5b206b84..b3d4256a218 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java
@@ -95,6 +95,14 @@ public MayExpandMethodCondition(SchemaVariable receiver, SchemaVariable methname
         this.args = args;
     }
 
+    /**
+     * Instantiate a new variable condition for class-local method calls without an explicit
+     * receiver.
+     *
+     * @param methodName non-null program schema var for the methodname
+     * @param args non-null program schema var for the arguments of the call
+     * @param negation {@code true} iff the condition is to be negated
+     */
     public MayExpandMethodCondition(SchemaVariable methodName, SchemaVariable args,
             boolean negation) {
         this(null, methodName, args, negation);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java
index 051650ad602..a6c7a12bb56 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MetaDisjointCondition.java
@@ -19,12 +19,24 @@
 import org.key_project.util.collection.ImmutableSet;
 
 
+/**
+ * A variable condition for the taclet construct {@code \metaDisjoint}, checking that the two
+ * instantiations of the given term schema variables denote provably disjoint location sets.
+ *
+ * @author Michael Kirsten
+ */
 public final class MetaDisjointCondition extends VariableConditionAdapter {
 
     private final TermSV var1;
     private final TermSV var2;
 
 
+    /**
+     * Instantiates a new meta-disjoint condition.
+     *
+     * @param s1 the first term schema variable; its instantiation is interpreted as a location set
+     * @param s2 the second term schema variable; its instantiation is interpreted as a location set
+     */
     public MetaDisjointCondition(TermSV s1, TermSV s2) {
         this.var1 = s1;
         this.var2 = s2;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java
index e8c2e4376c9..4adda6d3749 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ModelFieldCondition.java
@@ -43,6 +43,12 @@ public class ModelFieldCondition extends VariableConditionAdapter {
     private final SchemaVariable field;
     private final boolean negated;
 
+    /**
+     * Instantiates a new model-field condition.
+     *
+     * @param field the schema variable which must be instantiated with a Java field
+     * @param negated whether the condition is negated ({@code \not isModelField})
+     */
     public ModelFieldCondition(SchemaVariable field, boolean negated) {
         this.field = field;
         this.negated = negated;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java
index c6f426a1a43..66a0e621ec9 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewJumpLabelCondition.java
@@ -30,6 +30,15 @@ public final class NewJumpLabelCondition implements VariableCondition {
 
     private final ProgramSV labelSV;
 
+    /**
+     * Instantiates a new jump-label condition.
+     *
+     * @param sv the program schema variable of sort {@code LABEL} which must be instantiated with
+     *        a label not occurring elsewhere in the context program or the schema variable
+     *        instantiations
+     * @throws IllegalArgumentException if the given schema variable is not a program schema
+     *         variable of sort {@code LABEL}
+     */
     public NewJumpLabelCondition(SchemaVariable sv) {
         if (!(sv instanceof ProgramSV psv) || psv.sort() != ProgramSVSort.LABEL) {
             throw new IllegalArgumentException(
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java
index 3b35c3f71c2..c022d91d3fe 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java
@@ -61,6 +61,17 @@ public class NewLocalVarsCondition implements VariableCondition {
      */
     private final SchemaVariable bodySV;
 
+    /**
+     * Instantiates a new local-variables condition.
+     *
+     * @param varDeclsSV the schema variable to which the variable declarations for the "before"
+     *        versions of the variables written by the loop are bound
+     * @param updateBeforeSV the schema variable to which the update
+     *        {@code {...||i_before := i||...}} is bound
+     * @param updateFrameSV the schema variable to which the reverse update
+     *        {@code {...||i := i_before||...}} is bound
+     * @param bodySV the schema variable holding the loop body
+     */
     public NewLocalVarsCondition(SchemaVariable varDeclsSV, SchemaVariable updateBeforeSV,
             SchemaVariable updateFrameSV, SchemaVariable bodySV) {
         this.varDeclsSV = varDeclsSV;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java
index e30eaa52b16..d340d97dcc6 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ObserverCondition.java
@@ -17,12 +17,28 @@
 import org.key_project.prover.rules.instantiation.SVInstantiations;
 
 
+/**
+ * A variable condition for the taclet construct {@code \isObserver}, checking that a term schema
+ * variable is instantiated with an observer function and that the heap argument of the observer is
+ * the given heap term. If the heap schema variable is not yet instantiated, it is bound to the
+ * observer's heap argument.
+ *
+ * @author Michael Kirsten
+ */
 public final class ObserverCondition implements VariableCondition {
 
     private final TermSV obs;
     private final TermSV heap;
 
 
+    /**
+     * Instantiates a new observer condition.
+     *
+     * @param obs the term schema variable which must be instantiated with an observer function
+     *        application (an {@link IObserverFunction})
+     * @param heap the term schema variable for the heap on which the observer is evaluated; it is
+     *        automatically instantiated with the observer's heap argument if not yet instantiated
+     */
     public ObserverCondition(TermSV obs, TermSV heap) {
         this.obs = obs;
         this.heap = heap;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java
index d5ee7e09bb8..040833bb0f1 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java
@@ -23,6 +23,14 @@
 import org.key_project.prover.rules.instantiation.MatchResultInfo;
 import org.key_project.prover.rules.instantiation.SVInstantiations;
 
+/**
+ * A variable condition for the taclet construct {@code \simplifyIfThenElseUpdate}: it turns two
+ * updates guarded by a condition {@code phi} into a single parallel update whose right-hand sides
+ * are {@code if phi then r1 else r2} expressions, and binds the common condition to a formula
+ * schema variable.
+ *
+ * @author Michael Kirsten
+ */
 public class SimplifyIfThenElseUpdateCondition implements VariableCondition {
 
     private final FormulaSV phi;
@@ -32,7 +40,16 @@ public class SimplifyIfThenElseUpdateCondition implements VariableCondition {
     private final SchemaVariable result;
 
 
-
+    /**
+     * Instantiates a new simplify-if-then-else-update condition.
+     *
+     * @param phi the formula schema variable guarding the two updates
+     * @param u1 the update schema variable applied if {@code phi} holds
+     * @param u2 the update schema variable applied if {@code phi} does not hold
+     * @param commonFormula the formula schema variable to which the guard {@code phi} is bound
+     * @param result the schema variable to which the merged update
+     *        {@code if phi then u1 else u2} is bound
+     */
     public SimplifyIfThenElseUpdateCondition(FormulaSV phi, UpdateSV u1, UpdateSV u2,
             FormulaSV commonFormula, SchemaVariable result) {
         super();
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java
index ec55d75549b..1d463b661de 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StaticFieldCondition.java
@@ -31,6 +31,12 @@ public class StaticFieldCondition extends VariableConditionAdapter {
     private final SchemaVariable field;
     private final boolean negated;
 
+    /**
+     * Instantiates a new static-field condition.
+     *
+     * @param field the schema variable which must be instantiated with a Java field
+     * @param negated whether the condition is negated ({@code \not isStaticField})
+     */
     public StaticFieldCondition(SchemaVariable field, boolean negated) {
         this.field = field;
         this.negated = negated;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java
index 3cd28c7f4c9..6f92a1e43db 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreStmtInCondition.java
@@ -34,6 +34,13 @@ public class StoreStmtInCondition implements VariableCondition {
     private final ProgramSV storeInSV;
     private final JTerm term;
 
+    /**
+     * Instantiates a new store-statement-in condition.
+     *
+     * @param resultVarSV the program schema variable to which the extracted statement is bound
+     * @param term the term whose Java block contains the statement to store; the statement is
+     *        substituted with the current schema variable instantiations first
+     */
     public StoreStmtInCondition(ProgramSV resultVarSV, JTerm term) {
         this.storeInSV = resultVarSV;
         this.term = term;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java
index 80df4473aa3..b15377be4ae 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/StoreTermInCondition.java
@@ -25,6 +25,13 @@ public class StoreTermInCondition implements VariableCondition {
     private final SchemaVariable storeInSV;
     private final JTerm term;
 
+    /**
+     * Instantiates a new store-term-in condition.
+     *
+     * @param resultVarSV the schema variable to which the (substituted) term is bound
+     * @param term the term to store; it is substituted with the current schema variable
+     *        instantiations first
+     */
     public StoreTermInCondition(SchemaVariable resultVarSV, JTerm term) {
         this.storeInSV = resultVarSV;
         this.term = term;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java
index 686c5040e07..ad9a021f944 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SubFormulaCondition.java
@@ -28,6 +28,12 @@ public class SubFormulaCondition extends VariableConditionAdapter {
     private final FormulaSV a;
     private final boolean negated;
 
+    /**
+     * Instantiates a new sub-formula condition.
+     *
+     * @param a the formula schema variable whose instantiation is checked for formula sub-terms
+     * @param negated whether the condition is negated ({@code \not hasSubFormulas})
+     */
     public SubFormulaCondition(FormulaSV a, boolean negated) {
         this.a = a;
         this.negated = negated;
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java
index 3d2ad379330..45176d2bb21 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TermLabelCondition.java
@@ -27,6 +27,13 @@ public class TermLabelCondition extends VariableConditionAdapter {
     private final Name ln;
     private final boolean negated;
 
+    /**
+     * Instantiates a new term-label condition.
+     *
+     * @param l the term-label schema variable whose instantiations are searched for the label
+     * @param t the name of the term label to look for
+     * @param negated whether the condition is negated ({@code \not hasLabel})
+     */
     public TermLabelCondition(TermLabelSV l, String t, boolean negated) {
         this.l = l;
         this.ln = new Name(t);
diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java
index 504137f765e..6d7e09c7217 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java
@@ -71,6 +71,11 @@ public static class GenericSortResolver extends TypeResolver {
 
         private final GenericSort gs;
 
+        /**
+         * Instantiates a new resolver for the instantiation of a generic sort.
+         *
+         * @param gs the generic sort whose instantiation is resolved
+         */
         public GenericSortResolver(GenericSort gs) {
             this.gs = gs;
         }
@@ -101,6 +106,11 @@ public static class NonGenericSortResolver extends TypeResolver {
 
         private final Sort s;
 
+        /**
+         * Instantiates a new resolver for a non-generic (concrete) sort.
+         *
+         * @param s the sort to resolve
+         */
         public NonGenericSortResolver(Sort s) {
             this.s = s;
         }
@@ -131,6 +141,12 @@ public static class ElementTypeResolverForSV extends TypeResolver {
 
         private final SchemaVariable resolveSV;
 
+        /**
+         * Instantiates a new resolver for the element type of the instantiation of a schema
+         * variable.
+         *
+         * @param sv the schema variable whose instantiation's element type is resolved
+         */
         public ElementTypeResolverForSV(SchemaVariable sv) {
             this.resolveSV = sv;
         }
@@ -179,6 +195,12 @@ public static class ContainerTypeResolver extends TypeResolver {
 
         private final SchemaVariable memberSV;
 
+        /**
+         * Instantiates a new resolver for the container type of the instantiation of a schema
+         * variable.
+         *
+         * @param sv the schema variable whose instantiation's container type is resolved
+         */
         public ContainerTypeResolver(SchemaVariable sv) {
             this.memberSV = sv;
         }
@@ -243,6 +265,11 @@ public String toString() {
     private static class ParametricSortResolver extends TypeResolver {
         private final ParametricSortInstance psi;
 
+        /**
+         * Instantiates a new resolver for the instantiation of a parametric sort instance.
+         *
+         * @param psi the parametric sort instance whose instantiation is resolved
+         */
         public ParametricSortResolver(ParametricSortInstance psi) {
             this.psi = psi;
         }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java
index 89590cfdf0d..4e0d6993027 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/BranchesCommand.java
@@ -176,6 +176,10 @@ private Node findNodeByNumber(Proof proof, int serial) throws ScriptException {
         throw new ScriptException();
     }
 
+    @Documentation(category = "Auxiliary", value = """
+            Selects or removes a branch in the proof tree, or restricts the automatic strategy
+            to a selected branch.
+            """)
     public static class Parameters {
         @Argument
         @Documentation("The operation mode: 'push', 'pop', 'select', or 'single'")
diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java
index ada1dc76f1f..3619594161f 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java
@@ -122,6 +122,9 @@ private TacletApp makeRuleApp(Parameters p, EngineState state) throws ScriptExce
 
     }
 
+    @Documentation(category = "Auxiliary", value = """
+            Expands method and class invariant definitions at a given location in the goal.
+            """)
     public static class Parameters {
         @Option(value = "on")
         @Documentation("A term pattern to match the expansion location against")
diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/RewriteCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/RewriteCommand.java
index 1b7462e992a..09c98b6a3ef 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/scripts/RewriteCommand.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/RewriteCommand.java
@@ -252,6 +252,9 @@ private JTerm getSubTerm(JTerm t, IntIterator pit) {
         }
     }
 
+    @Documentation(category = "Auxiliary", value = """
+            Rewrites all occurrences of a term pattern into a replacement term.
+            """)
     public static class Parameters {
         @Option(value = "find")
         @Documentation("The term pattern to search for and replace")
diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/SchemaVarCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/SchemaVarCommand.java
index a03deed85fe..32b1770d101 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/scripts/SchemaVarCommand.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/SchemaVarCommand.java
@@ -18,7 +18,9 @@
 import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
 
 /**
+ * Defines a schema variable that can be used in subsequent script commands.
  *
+ * @deprecated use the abbreviation mechanism of the KeY parser instead.
  */
 @Deprecated
 public class SchemaVarCommand extends AbstractCommand {
diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/SequentWithHoles.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/SequentWithHoles.java
index 8ff63cf5291..de90d176f04 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/scripts/SequentWithHoles.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/SequentWithHoles.java
@@ -20,6 +20,11 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+/// A sequent whose antecedent and succedent formulas may contain holes (placeholders).
+/// It is used to express term patterns with holes in proof script commands, which are
+/// matched against (parts of) the current goals.
+///
+/// @author Alexander Weigl
 @NullMarked
 public class SequentWithHoles {
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/SetCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/SetCommand.java
index 8a55d458608..0d60d135aa5 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/scripts/SetCommand.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/SetCommand.java
@@ -168,6 +168,10 @@ public String getName() {
         return "set";
     }
 
+    @Documentation(category = "Control", value = """
+            Configures the automatic strategy and further proof settings by assigning
+            key-value pairs, e.g. `set oss false` or `set steps 100`.
+            """)
     public static class Parameters {
 
         @Documentation("Enable/disable one-step simplification")
diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/TermWithHoles.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/TermWithHoles.java
index 30e9e65265b..b2b4cf8d87b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/scripts/TermWithHoles.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/TermWithHoles.java
@@ -38,6 +38,12 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+/// A term that may contain holes (wildcards) and focus or ellipsis markers, written with
+/// the placeholders `?` (term hole), `?fml` (formula hole), `?focus` (focus point) and
+/// `?find` (ellipsis). Such patterns are used by proof script commands (e.g. `rewrite`,
+/// `expand`, `focus`) to match terms and formulas of the current goal.
+///
+/// @author Alexander Weigl
 @NullMarked
 public class TermWithHoles {
 
diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java
index 18d694523ae..70992d6905b 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/meta/ArgumentsLifter.java
@@ -6,10 +6,16 @@
 
 import java.lang.reflect.Field;
 import java.lang.reflect.Modifier;
-import java.util.*;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Comparator;
+import java.util.List;
 
 import de.uka.ilkd.key.scripts.ProofScriptCommand;
 
+import com.github.therapi.runtimejavadoc.ClassJavadoc;
+import com.github.therapi.runtimejavadoc.CommentFormatter;
+import com.github.therapi.runtimejavadoc.RuntimeJavadoc;
 import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 
@@ -81,7 +87,7 @@ public static String generateCommandUsage(String commandName, Class<?> parameter
     }
 
     public static String extractDocumentation(String command, Class<?> commandClazz,
-            Class<?> parameterClazz) {
+            @Nullable Class<?> parameterClazz) {
         StringBuilder sb = new StringBuilder();
 
         Deprecated dep = commandClazz.getAnnotation(Deprecated.class);
@@ -90,22 +96,35 @@ public static String extractDocumentation(String command, Class<?> commandClazz,
                 "**Caution! This proof script command is deprecated, and may be removed soon!**\n\n");
         }
 
+        ClassJavadoc jdocCommand = RuntimeJavadoc.getJavadoc(commandClazz);
+
         Documentation docCommand = commandClazz.getAnnotation(Documentation.class);
         if (docCommand != null) {
             sb.append(docCommand.value());
             sb.append("\n\n");
+        } else if (jdocCommand != null && jdocCommand.getComment() != null) {
+            // the javadoc is only available if the class was compiled with a JDK that
+            // understands the doc comment style used in the source (e.g., JDK 23+ for ///)
+            sb.append(jdocCommand.getComment());
+            sb.append("\n\n");
         }
 
         if (parameterClazz == null) {
             return sb.toString();
         }
 
+        ClassJavadoc jdocParams = RuntimeJavadoc.getJavadoc(parameterClazz);
+
         Documentation docAn = parameterClazz.getAnnotation(Documentation.class);
         if (docAn != null) {
             sb.append(docAn.value());
             sb.append("\n\n");
+        } else if (jdocParams != null && jdocParams.getComment() != null) {
+            sb.append(jdocParams.getComment());
+            sb.append("\n\n");
         }
 
+
         sb.append("#### Usage: \n`").append(generateCommandUsage(command, parameterClazz))
                 .append("`\n\n");
 
@@ -114,13 +133,23 @@ public static String extractDocumentation(String command, Class<?> commandClazz,
         sb.append("#### Parameters:\n");
         for (ProofScriptArgument meta : args) {
             sb.append("\n\n");
+
+            var documentation = meta.getDocumentation();
+            if (documentation.isEmpty() && jdocParams != null) {
+                documentation = jdocParams.getFields().stream()
+                        .filter(it -> it.getName().equals(meta.getField().getName()))
+                        .findFirst()
+                        .map(field -> new CommentFormatter().format(field.getComment()))
+                        .orElse("");
+            }
+
             if (meta.isPositional()) {
                 sb.append("* `%s` *(%s%s positional argument, type %s)*:<br>%s".formatted(
                     meta.getName(),
                     meta.isRequired() ? "" : "optional ",
                     ordinalStr(meta.getArgumentPosition() + 1),
                     meta.getField().getType().getSimpleName(),
-                    meta.getDocumentation()));
+                    documentation));
             }
 
             if (meta.isOption()) {
@@ -128,28 +157,28 @@ public static String extractDocumentation(String command, Class<?> commandClazz,
                     meta.getName(),
                     meta.isRequired() ? "" : "optional ",
                     meta.getField().getType().getSimpleName(),
-                    meta.getDocumentation()));
+                    documentation));
             }
 
             if (meta.isFlag()) {
                 sb.append("* `%s` *(flag)*:<br>%s".formatted(
                     meta.getName(),
-                    meta.getDocumentation()));
+                    documentation));
             }
 
             if (meta.isPositionalVarArgs()) {
-                sb.append("* `%s...` (%s): %s".formatted(
+                sb.append("* `%s...` (%s): %s<br>%s".formatted(
                     meta.getName(),
                     meta.getPositionalVarargs().as(),
                     meta.getPositionalVarargs().startIndex(),
-                    meta.getDocumentation()));
+                    documentation));
             }
 
             if (meta.isOptionalVarArgs()) {
                 sb.append("* `%s...`: *(options prefixed by `%s`, type %s)*:<br>%s".formatted(
                     meta.getName(), meta.getOptionalVarArgs().prefix(),
                     meta.getOptionalVarArgs().as().getSimpleName(),
-                    meta.getDocumentation()));
+                    documentation));
             }
 
         }
@@ -189,39 +218,6 @@ public static String extractCategory(Class<? extends ProofScriptCommand> command
 
     private static @NonNull List<ProofScriptArgument> getSortedProofScriptArguments(
             Class<?> parameterClazz) {
-        // Comparator<ProofScriptArgument> optional =
-        // Comparator.comparing(ProofScriptArgument::isOption);
-        // Comparator<ProofScriptArgument> positional =
-        // Comparator.comparing(ProofScriptArgument::isPositional);
-        // Comparator<ProofScriptArgument> flagal =
-        // Comparator.comparing(ProofScriptArgument::isFlag);
-        // Comparator<ProofScriptArgument> allargsal =
-        // Comparator.comparing(ProofScriptArgument::isPositionalVarArgs);
-        // Comparator<ProofScriptArgument> byRequired =
-        // Comparator.comparing(ProofScriptArgument::isRequired);
-        // Comparator<ProofScriptArgument> byName =
-        // Comparator.comparing(ProofScriptArgument::getName);
-        //
-        // Comparator<ProofScriptArgument> byPos = Comparator.comparing(it -> {
-        // if (it.isPositionalVarArgs()) {
-        // it.getPositionalVarargs().startIndex();
-        // }
-        // if (it.isPositional()) {
-        // it.getArgument().value();
-        // }
-        //
-        // return -1;
-        // });
-        //
-        //
-        // var comp = optional
-        // .thenComparing(flagal)
-        // .thenComparing(positional)
-        // .thenComparing(allargsal)
-        // .thenComparing(byRequired)
-        // .thenComparing(byPos)
-        // .thenComparing(byName);
-
         var args = Arrays.stream(parameterClazz.getDeclaredFields())
                 .map(ProofScriptArgument::new)
                 .sorted(Comparator.comparing(ProofScriptArgument::orderString))