diff --git a/key.core.symbolic_execution/src/main/java/module-info.java b/key.core.symbolic_execution/src/main/java/module-info.java
index e0f66a0149c..85d5f648cdd 100644
--- a/key.core.symbolic_execution/src/main/java/module-info.java
+++ b/key.core.symbolic_execution/src/main/java/module-info.java
@@ -1,5 +1,7 @@
+import de.uka.ilkd.key.proof.init.DefaultProfileResolver;
 import de.uka.ilkd.key.proof.init.POExtension;
 import de.uka.ilkd.key.symbolic_execution.po.TruthValuePOExtension;
+import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfileDefaultProfileResolver;
 
 /**
  *
@@ -8,4 +10,4 @@
  */
 module org.key_project.symbolic_execution{exports de.uka.ilkd.key.symbolic_execution;exports de.uka.ilkd.key.symbolic_execution.model;exports de.uka.ilkd.key.symbolic_execution.po;exports de.uka.ilkd.key.symbolic_execution.profile;exports de.uka.ilkd.key.symbolic_execution.strategy;exports de.uka.ilkd.key.symbolic_execution.strategy.breakpoint;exports de.uka.ilkd.key.symbolic_execution.util;requires java.xml;requires org.key_project.core;requires org.key_project.ncore;requires org.key_project.util;requires java.desktop;requires org.slf4j;requires org.jspecify;
 
-provides POExtension with TruthValuePOExtension;}
+provides DefaultProfileResolver with SymbolicExecutionJavaProfileDefaultProfileResolver;provides POExtension with TruthValuePOExtension;}
diff --git a/key.core.testgen/src/main/java/module-info.java b/key.core.testgen/src/main/java/module-info.java
index 9a2d85a8960..32db629691d 100644
--- a/key.core.testgen/src/main/java/module-info.java
+++ b/key.core.testgen/src/main/java/module-info.java
@@ -1,16 +1,11 @@
+import de.uka.ilkd.key.macros.ProofMacro;
+import de.uka.ilkd.key.testgen.macros.TestGenMacro;
+
 /**
  *
  * @author Alexander Weigl
  * @version 1 (04.04.24)
  */
-module org.key_project.core.testgen {
-    requires org.key_project.core;
-    requires org.slf4j;
-    requires org.key_project.util;
-    requires org.key_project.ncore;
-    requires org.jspecify;
-    exports de.uka.ilkd.key.testgen.smt.testgen;
-    exports de.uka.ilkd.key.testgen.macros;
-    exports de.uka.ilkd.key.testgen.smt.counterexample;
-    exports de.uka.ilkd.key.testgen.settings;
-}
\ No newline at end of file
+module org.key_project.core.testgen{requires org.key_project.core;requires org.slf4j;requires org.key_project.util;requires org.key_project.ncore;requires org.jspecify;exports de.uka.ilkd.key.testgen.smt.testgen;exports de.uka.ilkd.key.testgen.macros;exports de.uka.ilkd.key.testgen.smt.counterexample;exports de.uka.ilkd.key.testgen.settings;
+
+provides ProofMacro with TestGenMacro;}
diff --git a/key.core.testgen/src/main/resources/services/de.uka.ilkd.key.macros.ProofMacro b/key.core.testgen/src/main/resources/services/de.uka.ilkd.key.macros.ProofMacro
index 4480e78c800..0eb775fb6b3 100644
--- a/key.core.testgen/src/main/resources/services/de.uka.ilkd.key.macros.ProofMacro
+++ b/key.core.testgen/src/main/resources/services/de.uka.ilkd.key.macros.ProofMacro
@@ -2,4 +2,4 @@
 # Macros to appear in the context menu
 #
 
-de.uka.ilkd.key.macros.TestGenMacro
+de.uka.ilkd.key.testgen.macros.TestGenMacro
diff --git a/keyext.exploration/src/main/java/module-info.java b/keyext.exploration/src/main/java/module-info.java
index 92d8ba9ed2c..322ba9b2bfd 100644
--- a/keyext.exploration/src/main/java/module-info.java
+++ b/keyext.exploration/src/main/java/module-info.java
@@ -1,14 +1,10 @@
+import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
+
 /**
  *
  * @author Alexander Weigl
  * @version 1 (31.03.24)
  */
-module keyext.exploration {
-    requires transitive org.key_project.ui;
-    requires org.key_project.core;
-    requires org.jspecify;
-    requires java.desktop;
-    requires org.key_project.ncore;
-    requires org.key_project.util;
-    requires dockingframes.common;
-}
\ No newline at end of file
+module keyext.exploration{requires transitive org.key_project.ui;requires org.key_project.core;requires org.jspecify;requires java.desktop;requires org.key_project.ncore;requires org.key_project.util;requires dockingframes.common;
+
+provides KeYGuiExtension with org.key_project.exploration.ExplorationExtension;}
diff --git a/keyext.proofmanagement/src/main/java/module-info.java b/keyext.proofmanagement/src/main/java/module-info.java
index 0342bf50e2f..974ce1e0f1a 100644
--- a/keyext.proofmanagement/src/main/java/module-info.java
+++ b/keyext.proofmanagement/src/main/java/module-info.java
@@ -1,15 +1,12 @@
+import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
+
 /**
  *
  * @author Alexander Weigl
  * @version 1 (31.03.24)
  */
-module keyext.proofmanagement {
-    requires org.key_project.ui;
-    requires org.jspecify;
-    requires java.desktop;
-    requires org.slf4j;
-    requires org.key_project.core;
-    requires org.key_project.util;
-    requires org.key_project.ncore;
-    /* not available requires ST4; */
-}
\ No newline at end of file
+module keyext.proofmanagement{requires org.key_project.ui;requires org.jspecify;requires java.desktop;requires org.slf4j;requires org.key_project.core;requires org.key_project.util;requires org.key_project.ncore;
+/* not available requires ST4; */
+
+
+provides KeYGuiExtension with org.key_project.proofmanagement.ProofManagementExt;}
diff --git a/keyext.slicing/src/main/java/module-info.java b/keyext.slicing/src/main/java/module-info.java
index 744e7eac2ce..e27dea16fb9 100644
--- a/keyext.slicing/src/main/java/module-info.java
+++ b/keyext.slicing/src/main/java/module-info.java
@@ -1,19 +1,10 @@
+import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
+
 /**
  *
  * @author Alexander Weigl
  * @version 1 (31.03.24)
  */
-module keyext.slicing {
-    requires org.key_project.core;
-    requires org.key_project.ui;
-    requires java.desktop;
-    requires org.jspecify;
-    requires org.slf4j;
-    requires com.miglayout.core;
-    requires org.key_project.util;
-    requires org.key_project.ncore;
-    requires dockingframes.common;
-    requires dockingframes.core;
-    exports org.key_project.slicing;
-    exports org.key_project.slicing.analysis;
-}
\ No newline at end of file
+module keyext.slicing{requires org.key_project.core;requires org.key_project.ui;requires java.desktop;requires org.jspecify;requires org.slf4j;requires com.miglayout.core;requires org.key_project.util;requires org.key_project.ncore;requires dockingframes.common;requires dockingframes.core;exports org.key_project.slicing;exports org.key_project.slicing.analysis;
+
+provides KeYGuiExtension with org.key_project.slicing.SlicingExtension;}
diff --git a/keyext.ui.testgen/src/main/java/module-info.java b/keyext.ui.testgen/src/main/java/module-info.java
index 77a6820bc89..d6853b53e37 100644
--- a/keyext.ui.testgen/src/main/java/module-info.java
+++ b/keyext.ui.testgen/src/main/java/module-info.java
@@ -1,13 +1,10 @@
+import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
+
 /**
  *
  * @author Alexander Weigl
  * @version 1 (31.03.24)
  */
-module keyext.ui.testgen {
-    requires java.desktop;
-    requires org.key_project.ui;
-    requires org.slf4j;
-    requires org.key_project.core;
-    requires org.key_project.core.testgen;
-    requires org.jspecify;
-}
\ No newline at end of file
+module keyext.ui.testgen{requires java.desktop;requires org.key_project.ui;requires org.slf4j;requires org.key_project.core;requires org.key_project.core.testgen;requires org.jspecify;
+
+provides KeYGuiExtension with de.uka.ilkd.key.gui.testgen.TestgenExtension;}