diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java
index bee675efa4..67b4483d3c 100644
--- a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java
+++ b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java
@@ -679,7 +679,7 @@ public int getIndex() {
     /**
      * temporary indexed ProgramElementName
      */
-    private static class TempIndProgramElementName extends IndProgramElementName {
+    public static class TempIndProgramElementName extends IndProgramElementName {
         TempIndProgramElementName(String basename, int index, NameCreationInfo creationInfo) {
             super(basename + TEMP_INDEX_SEPARATOR + index, basename, index, creationInfo);
         }
@@ -695,7 +695,7 @@ private static class TempIndProgramElementName extends IndProgramElementName {
     /**
      * regular indexed ProgramElementName
      */
-    private static class PermIndProgramElementName extends IndProgramElementName {
+    public static class PermIndProgramElementName extends IndProgramElementName {
         static final char SEPARATOR = '_';
 
         PermIndProgramElementName(String basename, int index, NameCreationInfo creationInfo) {
diff --git a/key.ncore.java/build.gradle b/key.ncore.java/build.gradle
new file mode 100644
index 0000000000..299489a7fc
--- /dev/null
+++ b/key.ncore.java/build.gradle
@@ -0,0 +1,23 @@
+sourceSets {
+    generator {
+        java {
+            srcDir("src/generator/java")
+        }
+    }
+    main {
+        java { srcDir("src/generated/java") }
+    }
+}
+
+dependencies {
+    implementation project(':key.core')
+    generatorImplementation(project(":key.core"))
+
+
+    implementation("info.picocli:picocli:4.7.7")
+
+    def JP_VERSION = "3.28.0-K13.5"
+    implementation("org.key-project.proofjava:javaparser-core:$JP_VERSION")
+    implementation("org.key-project.proofjava:javaparser-symbol-solver-core:$JP_VERSION")
+    testImplementation("com.google.truth:truth:1.4.5")
+}
\ No newline at end of file
diff --git a/key.ncore.java/src/adt/java-ast.java b/key.ncore.java/src/adt/java-ast.java
new file mode 100644
index 0000000000..19932f42a2
--- /dev/null
+++ b/key.ncore.java/src/adt/java-ast.java
@@ -0,0 +1,633 @@
+// Imports are copied to every file
+import org.jspecify.annotations.Nullable;
+import de.uka.ilkd.key.speclang.jml.pretranslation.*;
+import de.uka.ilkd.key.java.ast.PositionInfo;
+import org.key_project.util.collection.*;
+
+@Root
+abstract class JavaSourceElement implements Visitable {
+    @EqEx @Nullable PositionInfo positionInfo;
+}
+
+class CompilationUnit extends JavaNonTerminalProgramElement {
+    @Nullable PackageSpecification packageSpec;
+    List<Import> imports;
+    List<TypeDeclaration> typeDeclarations;
+}
+
+class ContextStatementBlock extends StatementBlock { }
+
+abstract class Declaration { }
+
+abstract class ExpressionContainer { }
+
+class Import extends JavaNonTerminalProgramElement {
+    boolean isMultiImport;
+    TypeReferenceInfix reference;
+}
+
+abstract class JavaNonTerminalProgramElement extends JavaProgramElement {}
+
+abstract class JavaProgramElement extends JavaSourceElement {}
+
+abstract class Label {}
+
+abstract class LoopInitializer {}
+
+abstract class NamedProgramElement {}
+
+class PackageSpecification extends JavaNonTerminalProgramElement {
+
+    PackageReference reference;
+}
+
+abstract class ParameterContainer {}
+
+abstract class ProgramElement {}
+
+abstract class ProgramVariableName {}
+
+abstract class Reference {}
+
+abstract class ScopeDefiningElement {}
+
+abstract class Statement {}
+
+class StatementBlock extends JavaStatement {}
+
+abstract class StatementContainer {}
+
+abstract class TerminalProgramElement {}
+
+abstract class TypeScope {}
+
+abstract class VariableScope {}
+
+class CcatchBreakLabelParameterDeclaration extends CcatchNonstandardParameterDeclaration {}
+
+class CcatchBreakWildcardParameterDeclaration extends CcatchNonstandardParameterDeclaration {}
+
+class CcatchContinueLabelParameterDeclaration extends CcatchNonstandardParameterDeclaration {}
+
+class CcatchContinueParameterDeclaration extends CcatchNonstandardParameterDeclaration {}
+
+class CcatchContinueWildcardParameterDeclaration extends CcatchNonstandardParameterDeclaration {}
+
+abstract class CcatchNonstandardParameterDeclaration extends JavaNonTerminalProgramElement {}
+
+class CcatchReturnParameterDeclaration extends CcatchNonstandardParameterDeclaration {}
+
+class CcatchReturnValParameterDeclaration extends CcatchNonstandardParameterDeclaration {}
+
+class ArrayDeclaration extends TypeDeclaration {}
+
+class ClassDeclaration extends TypeDeclaration {
+
+    Extends extending;
+
+    Implements implementing;
+
+    boolean isInnerClass;
+
+    boolean isLocalClass;
+
+    boolean isAnonymousClass;
+}
+
+class ClassInitializer extends JavaDeclaration {
+
+    StatementBlock body;
+}
+
+class ConstructorDeclaration extends MethodDeclaration {}
+
+class EnumClassDeclaration extends ClassDeclaration {}
+
+class Extends extends InheritanceSpecification {}
+
+class FieldDeclaration extends VariableDeclaration {
+
+    List<FieldSpecification> fieldSpecs;
+}
+
+class FieldSpecification extends VariableSpecification {}
+
+class Implements extends InheritanceSpecification {}
+
+abstract class InheritanceSpecification extends JavaNonTerminalProgramElement {
+
+    List<TypeReference> supertypes;
+}
+
+class InterfaceDeclaration extends TypeDeclaration {
+
+    Extends extending;
+}
+
+abstract class JavaDeclaration extends JavaNonTerminalProgramElement {
+
+    ImmutableList<de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLConstruct> attachedJml;
+
+    List<Modifier> modArray;
+}
+
+class LocalVariableDeclaration extends VariableDeclaration {
+
+    List<VariableSpecification> varSpecs;
+}
+
+abstract class MemberDeclaration {}
+
+class MethodDeclaration extends JavaDeclaration {
+
+    TypeReference returnType;
+
+    Comment[] voidComments;
+
+    ProgramElementName name;
+
+    List<ParameterDeclaration> parameters;
+
+    Throws exceptions;
+
+    StatementBlock body;
+
+    JMLModifiers jmlModifiers;
+
+    boolean parentIsInterfaceDeclaration;
+}
+
+abstract class Modifier extends JavaProgramElement {}
+
+class ParameterDeclaration extends VariableDeclaration {
+    List<VariableSpecification> varSpec;
+}
+
+class SuperArrayDeclaration extends TypeDeclaration {}
+
+class Throws extends JavaNonTerminalProgramElement {
+
+    List<TypeReference> exceptions;
+}
+
+abstract class TypeDeclaration extends JavaDeclaration {
+
+    ProgramElementName name;
+
+    ProgramElementName fullName;
+
+    List<MemberDeclaration> members;
+
+    boolean parentIsInterfaceDeclaration;
+
+    boolean isLibrary;
+
+    JMLModifiers jmlModifiers;
+}
+
+abstract class TypeDeclarationContainer {}
+
+abstract class VariableDeclaration extends JavaDeclaration {
+
+    TypeReference typeReference;
+
+    boolean parentIsInterfaceDeclaration;
+}
+
+class VariableSpecification extends JavaNonTerminalProgramElement {
+
+    Expression initializer;
+
+    int dimensions;
+
+    Type type;
+
+    IProgramVariable programVariable;
+}
+
+class AnnotationUseSpecification extends Modifier {
+
+    TypeReference tr;
+}
+
+
+class ArrayInitializer extends JavaNonTerminalProgramElement {
+    KeYJavaType kjt;
+}
+abstract class Expression {}
+
+abstract class ExpressionStatement {}
+
+abstract class Operator extends JavaNonTerminalProgramElement {}
+
+class ParenthesizedExpression extends Operator {
+    Expression child;
+}
+
+class PassiveExpression extends Operator{
+    Expression child;
+}
+
+abstract class Literal extends JavaProgramElement {
+    String value;
+}
+
+abstract class AbstractIntegerLiteral extends Literal {
+}
+
+class BooleanLiteral extends Literal {}
+
+class CharLiteral extends AbstractIntegerLiteral {}
+
+class DoubleLiteral extends Literal {}
+
+class EmptyMapLiteral extends Literal {}
+
+class EmptySeqLiteral extends Literal {}
+
+class EmptySetLiteral extends Literal {}
+
+class FloatLiteral extends Literal {
+    String value;
+}
+
+class FreeLiteral extends Literal {}
+
+class IntLiteral extends AbstractIntegerLiteral {}
+
+class LongLiteral extends AbstractIntegerLiteral {}
+
+class RealLiteral extends Literal {}
+
+class StringLiteral extends Literal {}
+
+class Assignment extends Operator {
+    AssignmentKind kind;
+    Expression left;
+    Expression right;
+}
+
+
+class BinaryOperator extends Operator {
+    BinaryOperatorKind kind;
+    Expression left;
+    Expression right;
+}
+
+class UnaryOperator implements Operator {
+    UnaryOperatorKind kind;
+    Expression child;
+
+}
+
+class LogicalFunctionOperator extends Operator {
+    LogicFunction function;
+    List<Expression> arguments;
+}
+
+class Conditional extends Operator {
+    Expression condition;
+    Expression thenExpr;
+    Expression elseExpr;
+}
+
+class DLEmbeddedExpression extends Operator {}
+
+class ExactInstanceof extends TypeOperator {}
+
+class Instanceof extends TypeOperator {}
+
+class New extends TypeOperator {
+
+    ClassDeclaration anonymousClass;
+
+    ReferencePrefix accessPath;
+}
+
+class NewArray extends TypeOperator {
+
+    int dimensions;
+
+    ArrayInitializer arrayInitializer;
+}
+
+class TypeCast extends TypeOperator {}
+
+abstract class TypeOperator extends Operator {
+
+    TypeReference typeReference;
+}
+
+
+class ArrayLengthReference extends JavaNonTerminalProgramElement {
+
+    ReferencePrefix prefix;
+}
+
+class ArrayReference extends JavaNonTerminalProgramElement {
+
+    ReferencePrefix prefix;
+
+    List<Expression> inits;
+}
+
+abstract class ConstructorReference {}
+
+class ExecutionContext extends JavaNonTerminalProgramElement {
+
+    TypeReference classContext;
+
+    ReferencePrefix runtimeInstance;
+}
+
+class FieldReference extends VariableReference {
+
+    ReferencePrefix prefix;
+}
+
+abstract class IExecutionContext {}
+
+abstract class MemberReference {}
+
+class MetaClassReference extends JavaNonTerminalProgramElement {
+
+    TypeReference typeReference;
+}
+
+abstract class MethodName {}
+
+abstract class MethodOrConstructorReference {}
+
+class MethodReference extends JavaNonTerminalProgramElement {
+
+    ReferencePrefix prefix;
+
+    MethodName name;
+
+    List<? extends Expression> arguments;
+}
+
+abstract class NameReference {}
+
+class PackageReference extends JavaNonTerminalProgramElement {
+
+    ReferencePrefix prefix;
+
+    ProgramElementName name;
+}
+
+abstract class PackageReferenceContainer {}
+
+abstract class ReferencePrefix {}
+
+abstract class ReferenceSuffix {}
+
+class SchemaTypeReference extends TypeReferenceImp {}
+
+class SchematicFieldReference extends FieldReference {
+
+    SchemaVariable schemaVariable;
+}
+
+abstract class SpecialConstructorReference extends JavaNonTerminalProgramElement {
+
+    List<Expression> arguments;
+}
+
+class SuperConstructorReference extends SpecialConstructorReference {
+
+    ReferencePrefix prefix;
+}
+
+class SuperReference extends JavaNonTerminalProgramElement {}
+
+class ThisConstructorReference extends SpecialConstructorReference {}
+
+class ThisReference extends JavaNonTerminalProgramElement {}
+
+class TypeRef extends TypeReferenceImp {}
+
+abstract class TypeReference {}
+
+abstract class TypeReferenceContainer {}
+
+abstract class TypeReferenceImp extends JavaNonTerminalProgramElement {
+
+    ReferencePrefix prefix;
+
+    int dimensions;
+
+    ProgramElementName name;
+}
+
+abstract class TypeReferenceInfix {}
+
+class VariableReference extends JavaNonTerminalProgramElement {
+
+    ProgramVariable variable;
+}
+
+class Assert extends JavaStatement {
+    Expression expression;
+    @Nullable String message;
+}
+
+abstract class Branch {}
+
+abstract class BranchStatement extends JavaStatement {}
+
+class Break extends LabelJumpStatement {}
+
+class Case extends Branch {
+    Expression expression;
+    List<Statement> body;
+}
+
+class Default extends Branch {
+    List<Statement> body;
+}
+
+
+abstract class CatchClause {}
+
+class SingleCatch {
+    ParameterDeclaration parameter;
+    StatementBlock body;
+}
+
+class CatchAllStatement extends CatchClause {}
+class Ccatch extends CatchClause {}
+
+class Continue extends LabelJumpStatement {}
+
+class Do extends LoopStatement {}
+
+class Else extends BranchImp {
+
+    Statement body;
+}
+
+class EmptyStatement extends JavaProgramElement {}
+
+class EnhancedFor extends LoopStatement {}
+
+class Exec extends BranchStatement {}
+
+abstract class ExpressionJumpStatement extends JumpStatement {
+    Expression expression;
+}
+
+class Finally extends BranchImp {
+
+    StatementBlock body;
+}
+
+class For extends LoopStatement {}
+
+class ForUpdates extends JavaNonTerminalProgramElement {
+
+    List<Expression> updates;
+}
+
+class Guard extends JavaNonTerminalProgramElement {
+
+    Expression expr;
+}
+
+abstract class IForUpdates {}
+abstract class IGuard {}
+abstract class ILoopInit {}
+
+class If extends BranchStatement {
+    Expression condition;
+    Statement thenBranch;
+    Statement elseBranch;
+}
+
+abstract class JavaStatement extends JavaNonTerminalProgramElement {}
+
+class JmlAssert extends JavaStatement {}
+
+abstract class JumpStatement extends JavaStatement {}
+
+abstract class LabelJumpStatement extends JumpStatement {
+    Label name;
+}
+
+class LabeledStatement extends JavaStatement {
+    Label name;
+    Statement body;
+}
+
+class LoopInit extends JavaNonTerminalProgramElement {
+    List<LoopInitializer> inits;
+}
+
+class LoopScopeBlock extends JavaStatement {
+    Expression variant;
+    Statement body;
+}
+
+abstract class LoopStatement extends JavaStatement {
+    ILoopInit inits;
+    IForUpdates updates;
+    IGuard guard;
+    Statement body;
+    ImmutableList<TextualJMLConstruct> attachedJml;
+}
+
+class MergePointStatement extends JavaStatement {
+
+    IProgramVariable identifier;
+}
+
+class MethodBodyStatement extends JavaNonTerminalProgramElement {}
+
+class MethodFrame extends JavaStatement {}
+
+class Return extends ExpressionJumpStatement {}
+
+class SetStatement extends JavaStatement {}
+
+class Switch extends BranchStatement {
+    Expression expression;
+    List<Branch> branches;
+}
+
+class SynchronizedBlock extends JavaStatement {
+
+    Expression expression;
+
+    StatementBlock body;
+}
+
+class Then extends BranchImp {}
+
+class Throw extends ExpressionJumpStatement {}
+
+class TransactionStatement extends JavaStatement {}
+
+class Try extends BranchStatement {
+    StatementBlock tryBlock;
+    List<Catch> catches;
+    @Nullable StatementBlock finallyBlock;
+}
+
+class While extends LoopStatement {}
+
+abstract class ProgramConstruct {}
+
+class ProgramElementName extends Name {}
+
+abstract class ProgramPrefix {}
+
+abstract class IndProgramElementName extends ProgramElementName {}
+
+class PermIndProgramElementName extends IndProgramElementName {}
+
+class TempIndProgramElementName extends IndProgramElementName {}
+
+abstract class IProgramMethod {}
+abstract class IProgramVariable {}
+
+class LocationVariable extends ProgramVariable {}
+class ProgramConstant extends ProgramVariable {}
+class ProgramMethod extends ObserverFunction {}
+
+class ProgramSV extends JOperatorSV {}
+
+abstract class ProgramVariable extends JAbstractSortedOperator {}
+
+abstract class AbstractProgramElement {}
+
+class InitArrayCreation extends InitArray {}
+
+abstract class ProgramTransformer extends JavaNonTerminalProgramElement {}
+class ReattachLoopInvariant extends ProgramTransformer {}
+class SpecialConstructorCall extends ProgramTransformer {}
+class StaticInitialisation extends ProgramTransformer {}
+class SwitchToIf extends ProgramTransformer {}
+class TypeOf extends ProgramTransformer {}
+class Unpack extends ProgramTransformer {}
+class UnwindLoop extends ProgramTransformer {}
+class MultipleVarDecl extends ProgramTransformer {}
+class PostWork extends ProgramTransformer {}
+class IsStatic extends ProgramTransformer {}
+class MethodCall extends ProgramTransformer {
+    MethodReference methRef;
+    ReferencePrefix newContext;
+    ProgramVariable pvar;
+    List<Expression> arguments;
+    KeYJavaType staticPrefixType;
+}
+class ArrayLength extends ProgramTransformer {}
+class ArrayPostDecl extends ProgramTransformer {}
+class ConstructorCall extends ProgramTransformer {}
+class CreateObject extends ProgramTransformer {}
+class DoBreak extends ProgramTransformer {}
+class EnhancedForElimination extends ProgramTransformer {}
+class EvaluateArgs extends ProgramTransformer {}
+class ExpandMethodBody extends ProgramTransformer {}
+class ForInitUnfoldTransformer extends ProgramTransformer {}
+class ForToWhile extends ProgramTransformer {}
+abstract class InitArray extends ProgramTransformer {}
diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java
new file mode 100644
index 0000000000..218205132d
--- /dev/null
+++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/Generator.java
@@ -0,0 +1,126 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.ncore.java;
+
+import java.io.File;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.concurrent.Callable;
+import java.util.stream.Stream;
+
+import org.key_project.ncore.java.NodeSteps.NodeStep;
+import org.key_project.ncore.java.PostSteps.PostStep;
+import org.key_project.ncore.java.PreSteps.PreStep;
+
+import com.github.javaparser.ParserConfiguration;
+import com.github.javaparser.StaticJavaParser;
+import com.github.javaparser.ast.CompilationUnit;
+import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration;
+import com.github.javaparser.utils.SourceRoot;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (4/11/26)
+ */
+public class Generator implements Callable<Integer> {
+    public static final Path ROOT = Paths.get("key.ncore.java/src/generated/java");
+    public static final Generator INSTANCE = new Generator();
+
+    CompilationUnit metaModel;
+
+    List<NodeStep> nodeSteps = new ArrayList<>(64);
+    List<PreStep> preSteps = new ArrayList<>(64);
+    List<PostStep> postSteps = new ArrayList<>(64);
+
+    public static void main(String[] args) throws Exception {
+        INSTANCE.call();
+    }
+
+    public Generator() {
+        preSteps.add(new PreSteps.PreComputation());
+
+        addStep(NodeSteps::setPackage);
+        addStep(NodeSteps::enforceHierarchy);
+        addStep(NodeSteps::processFields);
+        addStep(NodeSteps::addAllFieldsConstructor);
+        addStep(NodeSteps::addAllWoOptFieldsConstructor);
+        addStep(NodeSteps::addCopyConstructor);
+        addStep(NodeSteps::addEquals);
+        addStep(NodeSteps::ToString);
+        addStep(NodeSteps::addHashCode);
+        addStep(NodeSteps::addWiths);
+        addStep(NodeSteps::addBuilder);
+        addStep(NodeSteps::addOverrideConstructor);
+        addStep(NodeSteps::addOverrideConstructor2);
+        addStep(NodeSteps::addGetProperties);
+        addStep(NodeSteps::processFieldsAccessor);
+
+        postSteps.add(PostSteps::createVisitor);
+        postSteps.add(PostSteps::createArgVisitor);
+        postSteps.add(PostSteps::createVoidVisitor);
+        postSteps.add(PostSteps::createTraversalVisitor);
+        postSteps.add(PostSteps::createTraversalCopyOnDemandVisitor);
+        postSteps.add(PostSteps::createDeepCopyVisitor);
+    }
+
+    private void addStep(NodeStep nodeStep) {
+        nodeSteps.add(nodeStep);
+    }
+
+    @SuppressWarnings("unchecked")
+    <T> T getStep(Class<T> step) {
+        return (T) Stream.concat(preSteps.stream(), postSteps.stream())
+                .filter(step::isInstance)
+                .findFirst()
+                .orElse(null);
+    }
+
+    @Override
+    public Integer call() throws Exception {
+        var config = new ParserConfiguration();
+        config.setStoreTokens(false);
+        config.setLexicalPreservationEnabled(false);
+        config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_25);
+
+        StaticJavaParser.setConfiguration(config);
+        metaModel = StaticJavaParser
+                .parse(new File("key.ncore.java/src/adt/java-ast.java").getAbsoluteFile());
+        Files.createDirectories(ROOT);
+        SourceRoot sourceRoot = new SourceRoot(ROOT);
+
+        final var types = metaModel.getTypes();
+        for (var nodeStep : preSteps) {
+            nodeStep.applyOn(types);
+        }
+
+        List<CompilationUnit> nodeUnits = new ArrayList<>(types.size());
+        for (var type : types) {
+            var cu = new CompilationUnit();
+            cu.addType(type);
+            metaModel.getImports().forEach(it -> cu.addImport(it.clone()));
+            metaModel.addImport("java.lang.Objects");
+            metaModel.addImport("java.util.*");
+
+            for (var nodeStep : nodeSteps) {
+                nodeStep.applyOn((ClassOrInterfaceDeclaration) type);
+            }
+
+            nodeUnits.add(cu);
+            sourceRoot.add(cu);
+        }
+
+        for (var nodeStep : postSteps) {
+            nodeStep.applyOn(nodeUnits, sourceRoot);
+        }
+
+        sourceRoot.saveAll();
+        return 0;
+    }
+
+
+}
diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java
new file mode 100644
index 0000000000..a65a83a6fa
--- /dev/null
+++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/NodeSteps.java
@@ -0,0 +1,484 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.ncore.java;
+
+import java.util.stream.Collectors;
+
+import com.github.javaparser.StaticJavaParser;
+import com.github.javaparser.ast.CompilationUnit;
+import com.github.javaparser.ast.NodeList;
+import com.github.javaparser.ast.body.*;
+import com.github.javaparser.ast.expr.*;
+import com.github.javaparser.ast.nodeTypes.NodeWithName;
+import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName;
+import com.github.javaparser.ast.stmt.BlockStmt;
+import com.github.javaparser.ast.stmt.ReturnStmt;
+import com.github.javaparser.ast.type.ClassOrInterfaceType;
+import com.github.javaparser.ast.type.PrimitiveType;
+import com.github.javaparser.ast.type.Type;
+import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
+import static com.github.javaparser.StaticJavaParser.*;
+import static com.github.javaparser.ast.Modifier.DefaultKeyword.*;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (4/19/26)
+ */
+@SuppressWarnings("OptionalGetWithoutIsPresent")
+public class NodeSteps {
+    static void addWiths(ClassOrInterfaceDeclaration target) {
+        target.getFields().stream()
+                .flatMap(it -> it.getVariables().stream()).forEach(it -> {
+                    var args =
+                        target.getFields().stream()
+                                .flatMap(f -> f.getVariables().stream())
+                                .map(v -> {
+                                    if (v == it) {
+                                        return (Expression) v.getNameAsExpression();
+                                    } else {
+                                        return new MethodCallExpr(null, v.getNameAsString());
+                                    }
+                                }).toList();
+
+                    var m = target.addMethod("with" + upperStart(it.getNameAsString()), PUBLIC);
+                    m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString()));
+                    m.setType(new ClassOrInterfaceType(null, target.getNameAsString()));
+                    m.getBody().get().addStatement(new ReturnStmt(
+                        new ObjectCreationExpr(null,
+                            new ClassOrInterfaceType(null, target.getNameAsString()),
+                            new NodeList<>(args))));
+                });
+    }
+
+    private static String upperStart(String nameAsString) {
+        var c = nameAsString.substring(0, 1).toUpperCase();
+        return c + nameAsString.substring(1);
+    }
+
+    static void addEquals(ClassOrInterfaceDeclaration target) {
+        if (target.isAbstract() || target.isInterface()) {
+            return;
+        }
+        MethodDeclaration equals = target.addMethod("equals", PUBLIC);
+        equals.addModifier(FINAL);
+        equals.addAnnotation(Override.class);
+        equals.setType(Boolean.TYPE);
+        final var o = getNullableObject();
+        equals.getParameters().add(o);
+        BlockStmt body = equals.getBody().get();
+        body.addStatement(parseStatement("if(this == o) return true;"));
+        body.addStatement(parseStatement(
+            "if(!(o instanceof %s that)) return false;".formatted(target.getNameAsString())));
+        Expression equalFields = target.getFields().stream()
+                .filter(it -> it.getAnnotationByName("EqEx").isEmpty())
+                .flatMap(it -> it.getVariables().stream())
+                .map(it -> callObjects("equals", it.getNameAsExpression(),
+                    new FieldAccessExpr(new NameExpr("that"), it.getNameAsString())))
+                .reduce((a, b) -> new BinaryExpr(a, b, BinaryExpr.Operator.AND))
+                .orElse(new BooleanLiteralExpr(true));
+        body.addStatement(new ReturnStmt(equalFields));
+    }
+
+    static void addHashCode(ClassOrInterfaceDeclaration target) {
+        if (target.isAbstract() || target.isInterface()) {
+            return;
+        }
+
+        MethodDeclaration hashCode = target.addMethod("hashCode", PUBLIC);
+        hashCode.addModifier(FINAL);
+        hashCode.addAnnotation(Override.class);
+        hashCode.setType(Integer.TYPE);
+        Expression[] args = target.getFields()
+                .stream()
+                .filter(it -> it.getAnnotationByName("EqEx").isEmpty())
+                .flatMap(it -> it.getVariables().stream())
+                .map(NodeWithSimpleName::getNameAsExpression)
+                .map(it -> (Expression) it)
+                .toArray(Expression[]::new);
+
+        if (args.length == 0)
+            assert false : "No defined fields";
+        else
+            hashCode.getBody().get().addStatement(new ReturnStmt(
+                callObjects("hash", args)));
+    }
+
+    static void ToString(ClassOrInterfaceDeclaration clazz) {
+        if (clazz.isAbstract() || clazz.isInterface()) {
+            return;
+        }
+
+        MethodDeclaration toString = clazz.addMethod("toString", PUBLIC, FINAL);
+        toString.addAnnotation(Override.class);
+        toString.setType(String.class);
+        var parameters =
+            clazz.getFields().stream().flatMap(it -> it.getVariables().stream()).toList();
+        var sb = (clazz.getNameAsString() + "[")
+            + parameters.stream().map(NodeWithSimpleName::getNameAsString).map(it -> it + "=%s")
+                    .collect(Collectors.joining(", "))
+            + "]";
+
+        var args = parameters.stream().map(NodeWithSimpleName::getNameAsExpression)
+                .map(it -> (Expression) it).toList();
+        toString.getBody().get().addStatement(new ReturnStmt(
+            new MethodCallExpr(new StringLiteralExpr(sb), "formatted", new NodeList<>(args))));
+    }
+
+    private static Expression callObjects(String method, Expression... args) {
+        return new MethodCallExpr(new NameExpr("Objects"), method, new NodeList<>(args));
+    }
+
+    private static @NonNull Parameter getNullableObject() {
+        Type tObject = StaticJavaParser.parseType("java.lang.Object");
+        return new Parameter(new NodeList<>(), tObject, new SimpleName("o"));
+    }
+
+    static void addAllFieldsConstructor(ClassOrInterfaceDeclaration target) {
+        if (target.isInterface()) {
+            return;
+        }
+        ConstructorDeclaration constr = new ConstructorDeclaration();
+        var body = constr.getBody().get();
+        var params = constr.getParameters();
+        constr.setName(target.getNameAsString());
+        constr.setModifiers(PUBLIC);
+
+        for (var field : target.getFields()) {
+            var isOptional = field.getAnnotations().stream()
+                    .anyMatch(it -> it.getNameAsString().equals("Nullable"));
+            for (var variable : field.getVariables()) {
+                final var p = new Parameter(variable.getType().clone(), variable.getNameAsString());
+                field.getAnnotations().stream().map(AnnotationExpr::clone)
+                        .forEach(p::addAnnotation);
+                params.add(p);
+                if (isOptional) {
+                    body.addStatement(
+                        "this.%s = %s;".formatted(
+                            variable.getNameAsString(), variable.getNameAsString()));
+                } else {
+                    body.addStatement(
+                        "this.%s = Objects.requireNonNull(%s);".formatted(
+                            variable.getNameAsString(), variable.getNameAsString()));
+                }
+            }
+        }
+
+
+        target.addMember(constr);
+    }
+
+    static void addAllWoOptFieldsConstructor(ClassOrInterfaceDeclaration target) {
+        if (target.isInterface()) {
+            return;
+        }
+        ConstructorDeclaration constr = new ConstructorDeclaration();
+        var body = constr.getBody().get();
+        var params = constr.getParameters();
+        constr.setName(target.getNameAsString());
+        constr.setModifiers(PUBLIC);
+
+        for (var field : target.getFields()) {
+            var isOptional = field.getAnnotations().stream()
+                    .anyMatch(it -> it.getNameAsString().equals("Nullable"));
+
+
+            for (var variable : field.getVariables()) {
+                if (isOptional) {
+                    body.addStatement(
+                        "this.%s = null;".formatted(variable.getNameAsString()));
+                } else {
+                    final var p =
+                        new Parameter(variable.getType().clone(), variable.getNameAsString());
+                    field.getAnnotations().stream().map(AnnotationExpr::clone)
+                            .forEach(p::addAnnotation);
+                    params.add(p);
+                    body.addStatement(
+                        "this.%s = Objects.requireNonNull(%s);".formatted(
+                            variable.getNameAsString(), variable.getNameAsString()));
+                }
+            }
+        }
+
+
+        target.addMember(constr);
+    }
+
+
+    static void addOverrideConstructor(ClassOrInterfaceDeclaration target) {
+        if (target.isInterface()) {
+            return;
+        }
+
+        ConstructorDeclaration constr = target.addConstructor(PUBLIC);
+        var body = constr.getBody().get();
+        var params = constr.getParameters();
+        constr.setName(target.getNameAsString());
+        params.add(
+            new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other"));
+
+        params.add(new Parameter(parseType("Properties"), "map"));
+
+        var args = target.getFields().stream().flatMap(it -> it.getVariables().stream())
+                .map(NodeWithSimpleName::getNameAsString)
+                .map(it -> (Expression) parseExpression(
+                    "map.get(PROPERTY_%s, other.%s)".formatted(it.toUpperCase(), it)))
+                .toList();
+        body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args)));
+    }
+
+    static void addOverrideConstructor2(ClassOrInterfaceDeclaration target) {
+        if (target.isInterface()) {
+            return;
+        }
+
+        ConstructorDeclaration constr = target.addConstructor(PUBLIC);
+        var body = constr.getBody().get();
+        var params = constr.getParameters();
+        constr.setName(target.getNameAsString());
+        params.add(new Parameter(parseType("Properties"), "map"));
+
+        var args = target.getFields().stream().flatMap(it -> it.getVariables().stream())
+                .map(NodeWithSimpleName::getNameAsString)
+                .map(it -> (Expression) parseExpression(
+                    "map.get(PROPERTY_%s)".formatted(it.toUpperCase())))
+                .toList();
+        body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args)));
+    }
+
+    static void addGetProperties(ClassOrInterfaceDeclaration target) {
+        if (target.isInterface()) {
+            return;
+        }
+
+        var method = target.addMethod("properties", PUBLIC);
+        method.setType("Properties");
+        var body = method.getBody().get();
+
+
+        body.addStatement("Properties p = new DefaultProperties();");
+        target.getFields().stream()
+                .flatMap(it -> it.getVariables().stream())
+                .forEach(variable -> body.addStatement("p.set(PROPERTY_%s, %s());".formatted(
+                    variable.getNameAsString().toUpperCase(), variable.getNameAsString())));
+        body.addStatement("return p;");
+    }
+
+    static void addCopyConstructor(ClassOrInterfaceDeclaration target) {
+        if (target.isInterface()) {
+            return;
+        }
+
+        ConstructorDeclaration constr = target.addConstructor(PUBLIC);
+        var body = constr.getBody().get();
+        var params = constr.getParameters();
+        constr.setName(target.getNameAsString());
+        params.add(
+            new Parameter(new ClassOrInterfaceType(null, target.getNameAsString()), "other"));
+
+        /*
+         * for (var field : target.getFields()) {
+         * for (var variable : field.getVariables()) {
+         * //params.add(new Parameter(variable.getType().clone(), variable.getNameAsString()));
+         * body.addStatement(
+         * new ExpressionStmt(new AssignExpr(
+         * new FieldAccessExpr(new ThisExpr(), variable.getNameAsString()),
+         * new FieldAccessExpr(new NameExpr("other"), variable.getNameAsString()),
+         * AssignExpr.Operator.ASSIGN
+         * ))
+         * );
+         * }
+         * }
+         */
+
+        var args = target.getFields().stream().flatMap(it -> it.getVariables().stream())
+                .map(NodeWithSimpleName::getNameAsString)
+                .map(it -> (Expression) new FieldAccessExpr(new NameExpr("other"), it))
+                .toList();
+        body.addStatement(new MethodCallExpr(null, "this", new NodeList<>(args)));
+
+    }
+
+    static void setPackage(ClassOrInterfaceDeclaration target) {
+        var annotation = target.getAnnotationByName("Package")
+                .map(NodeWithName::getNameAsString)
+                .orElse("org.key_project.java.ast");
+
+        CompilationUnit cu = target.findCompilationUnit().get();
+        cu.setPackageDeclaration(annotation);
+
+        cu.setStorage(Generator.ROOT.resolve(annotation.replace(".", "/"))
+                .resolve(target.getNameAsString() + ".java"));
+
+        target.addAnnotation(NullMarked.class);
+        target.addModifier(PUBLIC);
+
+        boolean isAbstract = target.isAbstract() || target.isInterface();
+        if (isAbstract) {
+            target.setInterface(true);
+            target.addModifier(SEALED);
+            target.removeModifier(ABSTRACT);
+            var permittedTypes =
+                Generator.INSTANCE.getStep(PreSteps.PreComputation.class).permittedTypes;
+            for (var s : permittedTypes.get(target.getNameAsString())) {
+                target.getPermittedTypes().add(new ClassOrInterfaceType(null, s));
+            }
+        } else {
+            target.addModifier(FINAL);
+            target.setImplementedTypes(target.getExtendedTypes());
+            target.setExtendedTypes(new NodeList<>());
+        }
+    }
+
+    static void processFieldsAccessor(ClassOrInterfaceDeclaration target) {
+        if (target.isInterface())
+            return;
+
+        target.findCompilationUnit().get().addImport("org.key_project.java.ast.Property");
+
+        for (var field : target.getFields()) {
+            for (var variable : field.getVariables()) {
+                final var dataKey = new ClassOrInterfaceType(null, new SimpleName("Property"),
+                    new NodeList<>(toBoxType(variable.getType().clone())));
+                var f = target.addField(
+                    dataKey, "PROPERTY_" + variable.getNameAsString().toUpperCase(), PUBLIC, STATIC,
+                    FINAL);
+                f.getVariables().getFirst().setInitializer(
+                    "new Property<>(\"%s\")".formatted(variable.getNameAsString()));
+            }
+        }
+    }
+
+    private static Type toBoxType(Type clone) {
+        if (clone instanceof PrimitiveType pt) {
+            return pt.toBoxedType();
+        }
+        return clone;
+    }
+
+    static void processFields(ClassOrInterfaceDeclaration target) {
+        boolean isAbstract = target.isAbstract() || target.isInterface();
+
+        for (var field : target.getFields()) {
+            if (isAbstract) {
+                field.remove();
+            } else {
+                field.setModifiers(PRIVATE, FINAL);
+            }
+
+            for (var variable : field.getVariables()) {
+                if (isList(variable)) {
+                    var old = variable.getType().asClassOrInterfaceType();
+                    old.setName("RoList");
+                }
+
+
+                var getter = target.addMethod(variable.getNameAsString());
+                getter.setType(variable.getType().clone());
+
+                var nullable = field.getAnnotationByName("Nullable");
+                if (nullable.isPresent()) {
+                    getter.addAndGetAnnotation(Nullable.class);
+                }
+
+                if (isAbstract) {
+                    // getter.addModifier(Modifier.DefaultKeyword.ABSTRACT);
+                    getter.setBody(null);
+                } else {
+                    getter.getBody().get()
+                            .addStatement(new ReturnStmt(variable.getNameAsExpression()));
+                    getter.addModifier(PUBLIC, FINAL);
+                }
+                field.getAnnotationByName("Override")
+                        .ifPresent(it -> {
+                            it.remove();
+                            getter.addAnnotation(it);
+                        });
+            }
+        }
+    }
+
+    static void addBuilder(ClassOrInterfaceDeclaration target) {
+        if (target.isInterface())
+            return;
+
+        var builder = new ClassOrInterfaceDeclaration();
+        builder.setName("Builder");
+        builder.addModifier(PUBLIC, FINAL, STATIC);
+
+        for (var field : target.getFields()) {
+            for (var variable : field.variables()) {
+                var f = builder.addField(variable.getType().clone(),
+                    variable.getNameAsString(), PUBLIC);
+                f.addAnnotation(Nullable.class);
+            }
+        }
+
+        var build = builder.addMethod("build", PUBLIC);
+        build.setType(new ClassOrInterfaceType(null, target.getNameAsString()));
+
+        var args = builder.getFields().stream().flatMap(it -> it.variables().stream())
+                .map(it -> (Expression) it.getNameAsExpression())
+                .toList();
+        build.getBody().get().addStatement(new ReturnStmt(
+            new ObjectCreationExpr(null,
+                new ClassOrInterfaceType(null, target.getNameAsString()),
+                new NodeList<>(args))));
+
+        builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> {
+            var m = builder.addMethod(it.getNameAsString(), PUBLIC);
+            m.addParameter(new Parameter(it.getType().clone(), it.getNameAsString()));
+            m.setType(new ClassOrInterfaceType(null, "Builder"));
+            m.getBody().get().addStatement(
+                "this.%s=%s;".formatted(it.getNameAsString(), it.getNameAsString()));
+            m.getBody().get().addStatement("return this;");
+        });
+
+
+        builder.getFields().stream().flatMap(it -> it.variables().stream())
+                .filter(NodeSteps::isList)
+                .forEach(it -> {
+                    var m = builder.addMethod(it.getNameAsString(), PUBLIC);
+                    var t =
+                        it.getType().asClassOrInterfaceType().getTypeArguments().get().getFirst();
+                    m.addParameter(new Parameter(t.clone(), it.getNameAsString()));
+                    m.setType(new ClassOrInterfaceType(null, "Builder"));
+                    m.getBody().get().addStatement("if(this.%s==null) this.%s = new ArrayList<>();"
+                            .formatted(it.getNameAsString(), it.getNameAsString()));
+                    m.getBody().get().addStatement(
+                        "this.%s.add(%s);".formatted(it.getNameAsString(), it.getNameAsString()));
+                    m.getBody().get().addStatement("return this;");
+                });
+
+        target.addMember(builder);
+
+        var tb = target.addMethod("builder", PUBLIC);
+        tb.setType(new ClassOrInterfaceType(null, "Builder"));
+        final var b = tb.getBody().get();
+        b.addStatement("Builder b =  new Builder();");
+        builder.getFields().stream().flatMap(it -> it.variables().stream()).forEach(it -> b
+                .addStatement("b.%s = %s;".formatted(it.getNameAsString(), it.getNameAsString())));
+        b.addStatement("return b;");
+    }
+
+    private static boolean isList(VariableDeclarator type) {
+        if (type.getType().isClassOrInterfaceType()) {
+            return type.getType().asClassOrInterfaceType().getNameAsString().equals("List");
+        }
+        return false;
+    }
+
+    public static void enforceHierarchy(ClassOrInterfaceDeclaration decl) {
+        if (decl.getExtendedTypes().isEmpty()) {
+            decl.addExtendedType("JavaSourceElement");
+        }
+    }
+
+    interface NodeStep {
+        void applyOn(ClassOrInterfaceDeclaration target);
+    }
+}
diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java
new file mode 100644
index 0000000000..2bcd7de6f9
--- /dev/null
+++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PostSteps.java
@@ -0,0 +1,341 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.ncore.java;
+
+import java.util.List;
+import java.util.stream.Collectors;
+
+import com.github.javaparser.StaticJavaParser;
+import com.github.javaparser.ast.CompilationUnit;
+import com.github.javaparser.ast.Modifier;
+import com.github.javaparser.ast.NodeList;
+import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration;
+import com.github.javaparser.ast.body.FieldDeclaration;
+import com.github.javaparser.ast.body.VariableDeclarator;
+import com.github.javaparser.ast.expr.SimpleName;
+import com.github.javaparser.ast.nodeTypes.modifiers.NodeWithPrivateModifier;
+import com.github.javaparser.ast.stmt.BlockStmt;
+import com.github.javaparser.ast.type.ClassOrInterfaceType;
+import com.github.javaparser.ast.type.Type;
+import com.github.javaparser.ast.type.TypeParameter;
+import com.github.javaparser.utils.SourceRoot;
+
+import static com.github.javaparser.ast.Modifier.DefaultKeyword.*;
+import static org.key_project.ncore.java.Generator.ROOT;
+
+public class PostSteps {
+    public static void createVisitor(List<CompilationUnit> nodeUnits, SourceRoot sourceRoot) {
+        var generic = new TypeParameter("R");
+
+        var cu = new CompilationUnit();
+        var type = createTypeAndSetDefaults(cu, "Visitor", PUBLIC);
+        type.setInterface(true);
+        type.addTypeParameter(generic.clone());
+
+        for (CompilationUnit clazz : nodeUnits) {
+            try {
+                var t = clazz.getPrimaryType().get();
+                if (!(t instanceof ClassOrInterfaceDeclaration c))
+                    continue;
+                if (c.isInterface())
+                    continue;
+
+                var m = type.addMethod("visit");
+                m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n");
+                m.setType(generic.clone());
+                m.setBody(null);
+
+                var accept = t.addMethod("accept", PUBLIC);
+                accept.setType(generic.clone());
+                accept.getTypeParameters().add(generic.clone());
+                accept.addParameter(
+                    new ClassOrInterfaceType(null,
+                        new SimpleName(type.getFullyQualifiedName().get()),
+                        new NodeList<>(generic.clone())),
+                    "visitor");
+                accept.getBody().get()
+                        .addStatement("return visitor.visit(this);");
+            } catch (Exception e) {
+                System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath());
+            }
+        }
+        sourceRoot.add(cu);
+
+        var s = StaticJavaParser.parseBlock("{return defaultVisit(n);}");
+        var visitorWithDefaults = cu.clone();
+        visitorWithDefaults.setStorage(
+            ROOT.resolve("org/key_project/java/ast/visitor/VisitorWithDefaults.java"));
+        final var vwdef = visitorWithDefaults.getType(0);
+        vwdef.setName("VisitorWithDefaults");
+        for (var method : vwdef.getMethods()) {
+            method.addModifier(DEFAULT);
+            method.setBody(s.clone());
+        }
+        visitorWithDefaults.addImport("org.key_project.java.ast.*");
+        var m = vwdef.addMethod("defaultVisit");
+        m.addParameter("JavaSourceElement", "n");
+        m.setType(generic.clone());
+        m.setBody(null);
+        sourceRoot.add(visitorWithDefaults);
+    }
+
+    public static void createVoidVisitor(List<CompilationUnit> nodeUnits, SourceRoot sourceRoot) {
+        var cu = new CompilationUnit();
+        var type = createTypeAndSetDefaults(cu, "VoidVisitor", PUBLIC);
+        type.setInterface(true);
+
+        for (CompilationUnit clazz : nodeUnits) {
+            try {
+                var t = clazz.getPrimaryType().get();
+                if (!(t instanceof ClassOrInterfaceDeclaration c))
+                    continue;
+                if (c.isInterface())
+                    continue;
+
+                var m = type.addMethod("visit");
+                m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n");
+                m.setBody(null);
+
+
+                var accept = t.addMethod("accept", PUBLIC);
+                accept.addParameter(
+                    new ClassOrInterfaceType(null, type.getFullyQualifiedName().get()),
+                    "visitor");
+                accept.getBody().get().addStatement("visitor.visit(this);");
+
+
+            } catch (Exception e) {
+                System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath());
+            }
+        }
+        sourceRoot.add(cu);
+    }
+
+    public static void createTraversalVisitor(List<CompilationUnit> nodeUnits,
+            SourceRoot sourceRoot) {
+        var cu = new CompilationUnit();
+        var type = createTypeAndSetDefaults(cu, "CopyVisitor", PUBLIC);
+        type.getImplementedTypes().add(
+            (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor<JavaSourceElement>"));
+        addAcceptMethods(type);
+
+        for (CompilationUnit clazz : nodeUnits) {
+            try {
+                var t = clazz.getPrimaryType().get();
+
+                if (!(t instanceof ClassOrInterfaceDeclaration c))
+                    continue;
+                if (c.isInterface())
+                    continue;
+
+                var m = type.addMethod("visit", PUBLIC);
+                m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n");
+                m.addAnnotation(Override.class);
+                BlockStmt body = m.getBody().get();
+                body.addStatement("var b = n.builder();");
+                t.getFields()
+                        .stream().filter(NodeWithPrivateModifier::isPrivate)
+                        .forEach(f -> body.addStatement(
+                            "b.%s = (%s) accept(n.%s());"
+                                    .formatted(f.getVariable(0).getNameAsExpression(),
+                                        f.getVariable(0).getTypeAsString(),
+                                        f.getVariable(0).getNameAsExpression())));
+                body.addStatement("return b.build();");
+                m.setType(new ClassOrInterfaceType(null, t.getFullyQualifiedName().get()));
+            } catch (Exception e) {
+                System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath());
+            }
+        }
+        sourceRoot.add(cu);
+    }
+
+    public static void createTraversalCopyOnDemandVisitor(List<CompilationUnit> nodeUnits,
+            SourceRoot sourceRoot) {
+        var cu = new CompilationUnit();
+        var type = createTypeAndSetDefaults(cu, "CopyOnWriteVisitor", PUBLIC);
+
+        type.getImplementedTypes().add(
+            (ClassOrInterfaceType) StaticJavaParser.parseType("Visitor<JavaSourceElement>"));
+        addAcceptMethods(type);
+
+
+        for (CompilationUnit clazz : nodeUnits) {
+            try {
+                var t = clazz.getPrimaryType().get();
+
+                if (!(t instanceof ClassOrInterfaceDeclaration c))
+                    continue;
+                if (c.isInterface())
+                    continue;
+
+                var m = type.addMethod("visit", PUBLIC);
+                m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n");
+                m.addAnnotation(Override.class);
+                BlockStmt body = m.getBody().get();
+                body.addStatement("var b = n.builder();");
+                t.getFields()
+                        .stream()
+                        .filter(NodeWithPrivateModifier::isPrivate)
+                        .filter(PostSteps::isAstNode)
+                        .forEach(f -> body.addStatement(
+                            "b.%s = (%s) accept(n.%s());"
+                                    .formatted(f.getVariable(0).getNameAsExpression(),
+                                        f.getVariable(0).getTypeAsString(),
+                                        f.getVariable(0).getNameAsExpression())));
+                final var formatted = "boolean clean = %s;".formatted(
+                    t.getFields().isEmpty() ? "false"
+                            : t.getFields()
+                                    .stream().filter(NodeWithPrivateModifier::isPrivate)
+                                    .map(it -> {
+                                        final var n = it.getVariable(0).getNameAsString();
+                                        return "(n.%s() == b.%s)".formatted(n, n);
+                                    })
+                                    .collect(Collectors.joining("&&")));
+                body.addStatement(formatted);
+                body.addStatement("return clean?n:b.build();");
+                m.setType(new ClassOrInterfaceType(null, t.getFullyQualifiedName().get()));
+            } catch (Exception e) {
+                System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath());
+            }
+        }
+        sourceRoot.add(cu);
+    }
+
+    private static boolean isAstNode(FieldDeclaration field) {
+        return isAstNode(field.getVariables().getFirst());
+    }
+
+    private static boolean isAstNode(VariableDeclarator v) {
+        return isAstNode(v.getType());
+    }
+
+    private static boolean isAstNode(Type type) {
+        if (type.isClassOrInterfaceType()) {
+            var c = type.asClassOrInterfaceType();
+            if (c.getNameAsString().equals("RoList")) {
+                return isAstNode(c.getTypeArguments().get().getFirst());
+            }
+
+            final var name = c.getNameAsString();
+            if (name.equals("String")) {
+                return false;
+            }
+            try {
+                c.toUnboxedType();
+                return false;
+            } catch (UnsupportedOperationException e) {
+                return !(name.contains("Kind") || name.equals("PositionInfo")
+                        || name.equals("JMLModifiers"));
+            }
+        }
+        return false;
+    }
+
+    ///
+    /// ```java
+    /// <T extends Visitable> T accept(T n) {
+    /// return n != null ? n.accept(this) : null;
+    /// }
+    /// <T extends Visitable> RoList<T> accept(RoList<T> n) {
+    /// return n != null ? n.stream().map(it -> (T) it.accept(this)).toList() : null;
+    /// }
+    /// ```
+    private static void addAcceptMethods(ClassOrInterfaceDeclaration type) {
+        var t = StaticJavaParser.parseTypeParameter("T extends Visitable");
+        var typeT = StaticJavaParser.parseType("T");
+
+        {
+            var accept = type.addMethod("accept", PROTECTED);
+            accept.addTypeParameter(t);
+            accept.addParameter(typeT, "n");
+            accept.setType(typeT.clone());
+            accept.getBody().get().addStatement("return n!=null?n.accept(this):null;");
+        }
+
+        {
+            var acceptList = type.addMethod("accept", PROTECTED);
+            acceptList.addTypeParameter(t.clone());
+            acceptList.addParameter(StaticJavaParser.parseType("RoList<T>"), "n");
+            acceptList.setType("RoList<T>");
+            acceptList.getBody().get().addStatement(
+                "return n != null ? n.stream().map(it -> (T) it.accept(this)).collect(RoList.collector()) : null;");
+        }
+
+        {
+            var acceptList = type.addMethod("accept", PROTECTED);
+            acceptList.addTypeParameter("T");
+            acceptList.addParameter("T", "n");
+            acceptList.setType("T");
+            acceptList.getBody().get().addStatement("return n;");
+        }
+    }
+
+    private static ClassOrInterfaceDeclaration createTypeAndSetDefaults(CompilationUnit cu,
+            String typeName, Modifier.DefaultKeyword... mods) {
+        String name = "org.key_project.java.ast.visitor";
+        cu.setPackageDeclaration(name);
+        cu.addImport("org.key_project.java.ast.visitor.*");
+        cu.addImport("org.key_project.java.ast.*");
+        cu.addImport("de.uka.ilkd.key.java.ast.PositionInfo");
+        cu.addImport("org.key_project.util.collection.*");
+        cu.setStorage(ROOT.resolve("org/key_project/java/ast/visitor/%s.java".formatted(typeName)));
+        return cu.addClass(typeName, mods);
+    }
+
+    public static void createArgVisitor(List<CompilationUnit> nodeUnits, SourceRoot sourceRoot) {
+        var cu = new CompilationUnit();
+        var type = createTypeAndSetDefaults(cu, "ArgVisitor", PUBLIC);
+
+        var generic = new TypeParameter("R");
+        var argType = new TypeParameter("A");
+
+        type.setInterface(true);
+        type.addTypeParameter(generic.clone());
+        type.addTypeParameter(argType.clone());
+
+        for (CompilationUnit clazz : nodeUnits) {
+            try {
+                var t = clazz.getPrimaryType().get();
+                if (!(t instanceof ClassOrInterfaceDeclaration c))
+                    continue;
+                if (c.isInterface())
+                    continue;
+
+                cu.addImport(t.getFullyQualifiedName().get());
+
+                var m = type.addMethod("visit");
+                m.addParameter(new ClassOrInterfaceType(null, t.getNameAsString()), "n");
+                m.addParameter(argType.clone(), "arg");
+                m.setType(generic.clone());
+                m.setBody(null);
+
+                var accept = t.addMethod("accept", PUBLIC);
+                accept.setType(generic.clone());
+                accept.getTypeParameters().add(generic.clone());
+                accept.getTypeParameters().add(argType.clone());
+                accept.addParameter(
+                    new ClassOrInterfaceType(null,
+                        new SimpleName(type.getFullyQualifiedName().get()),
+                        new NodeList<>(generic.clone(), argType.clone())),
+                    "visitor");
+                accept.addParameter(argType.clone(), "arg");
+                accept.getBody().get()
+                        .addStatement("return visitor.visit(this,arg);");
+            } catch (Exception e) {
+                System.err.println(e.getMessage() + " :: " + clazz.getStorage().get().getPath());
+            }
+        }
+        sourceRoot.add(cu);
+    }
+
+
+    public static void createDeepCopyVisitor(List<CompilationUnit> nodeUnits,
+            SourceRoot sourceRoot) {
+
+    }
+
+    public interface PostStep {
+        void applyOn(List<CompilationUnit> nodeUnits, SourceRoot sourceRoot);
+    }
+}
diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java
new file mode 100644
index 0000000000..97daf7898e
--- /dev/null
+++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/PreSteps.java
@@ -0,0 +1,87 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.ncore.java;
+
+import java.util.ArrayList;
+import java.util.TreeMap;
+
+import com.github.javaparser.ast.NodeList;
+import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration;
+import com.github.javaparser.ast.body.FieldDeclaration;
+import com.github.javaparser.ast.body.TypeDeclaration;
+import com.github.javaparser.ast.nodeTypes.NodeWithSimpleName;
+import com.google.common.collect.Multimap;
+import com.google.common.collect.MultimapBuilder;
+
+import static com.github.javaparser.ast.Modifier.DefaultKeyword.ABSTRACT;
+
+public class PreSteps {
+    final static class PreComputation implements PreStep {
+        Multimap<String, String> inheritanceMap =
+            MultimapBuilder.treeKeys().treeSetValues().build();
+        Multimap<String, String> permittedTypes =
+            MultimapBuilder.treeKeys().treeSetValues().build();
+
+        @Override
+        public void applyOn(NodeList<TypeDeclaration<?>> types) {
+            TreeMap<String, ClassOrInterfaceDeclaration> fields = new TreeMap<>();
+
+            for (TypeDeclaration<?> decl : types) {
+                fields.put(decl.getNameAsString(), (ClassOrInterfaceDeclaration) decl);
+
+                var zuper = ((ClassOrInterfaceDeclaration) decl).getExtendedTypes().getOFirst()
+                        .map(NodeWithSimpleName::getNameAsString);
+                zuper.ifPresent(s -> inheritanceMap.put(decl.getNameAsString(), s));
+            }
+
+            // compute transitive closure
+            boolean changed = true;
+            while (changed) {
+                changed = false;
+                for (var clazz : inheritanceMap.keySet()) {
+                    final var strings = new ArrayList<>(inheritanceMap.get(clazz));
+                    for (var zuper : strings) {
+                        changed =
+                            changed || inheritanceMap.putAll(clazz, inheritanceMap.get(zuper));
+                    }
+                }
+            }
+
+            for (var decl : fields.sequencedValues()) {
+                if (decl.hasModifier(ABSTRACT)) {
+                    continue;
+                }
+
+                var newFields = new TreeMap<String, FieldDeclaration>();
+                for (var c : inheritanceMap.get(decl.getNameAsString())) {
+                    final var classOrInterfaceDeclaration = fields.get(c);
+                    if (classOrInterfaceDeclaration != null) {
+                        for (FieldDeclaration it : classOrInterfaceDeclaration.getFields()) {
+                            var name = it.getVariable(0).getNameAsString();
+                            newFields.computeIfAbsent(name, (k) -> {
+                                final var clone = it.clone();
+                                clone.addAnnotation(Override.class.getName());
+                                clone.setRange(null);
+                                return clone;
+                            });
+                        }
+                    }
+                }
+                decl.getMembers().addAll(newFields.values());
+            }
+
+            fillPermittedTypes();
+        }
+
+        private void fillPermittedTypes() {
+            for (var entry : inheritanceMap.entries()) {
+                permittedTypes.put(entry.getValue(), entry.getKey());
+            }
+        }
+    }
+
+    interface PreStep {
+        void applyOn(NodeList<TypeDeclaration<?>> types);
+    }
+}
diff --git a/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java b/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java
new file mode 100644
index 0000000000..2a467876f9
--- /dev/null
+++ b/key.ncore.java/src/generator/java/org/key_project/ncore/java/ReadAllHierarchy.java
@@ -0,0 +1,799 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.ncore.java;
+
+import java.io.File;
+import java.io.FileNotFoundException;
+import java.io.PrintWriter;
+import java.lang.reflect.AccessFlag;
+import java.util.*;
+
+import de.uka.ilkd.key.java.ast.*;
+import de.uka.ilkd.key.java.ast.ccatch.*;
+import de.uka.ilkd.key.java.ast.declaration.*;
+import de.uka.ilkd.key.java.ast.declaration.modifier.*;
+import de.uka.ilkd.key.java.ast.expression.*;
+import de.uka.ilkd.key.java.ast.expression.literal.*;
+import de.uka.ilkd.key.java.ast.expression.operator.*;
+import de.uka.ilkd.key.java.ast.expression.operator.adt.*;
+import de.uka.ilkd.key.java.ast.reference.*;
+import de.uka.ilkd.key.java.ast.statement.*;
+import de.uka.ilkd.key.logic.ProgramConstruct;
+import de.uka.ilkd.key.logic.ProgramElementName;
+import de.uka.ilkd.key.logic.ProgramPrefix;
+import de.uka.ilkd.key.logic.VariableNamer;
+import de.uka.ilkd.key.logic.op.*;
+import de.uka.ilkd.key.rule.AbstractProgramElement;
+import de.uka.ilkd.key.rule.metaconstruct.*;
+
+import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration;
+import com.github.javaparser.ast.type.ClassOrInterfaceType;
+
+import static de.uka.ilkd.key.java.ast.declaration.modifier.Modifiers.*;
+
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (4/11/26)
+ */
+public class ReadAllHierarchy {
+    static Set<Class<?>> allClasses = new HashSet<>(List.of(
+        GreaterThan.class,
+        ExecutionContext.class,
+        ArrayLength.class,
+        SuperReference.class,
+        ProgramTransformer.class,
+        Instanceof.class,
+        ArrayInitializer.class,
+        ProgramSV.class,
+        Exec.class,
+        ThisReference.class,
+        MethodCall.class,
+        FieldDeclaration.class,
+        ForInitUnfoldTransformer.class,
+        SchemaTypeReference.class,
+        EnhancedForElimination.class,
+        IProgramVariable.class,
+        ClassDeclaration.class,
+        ContextStatementBlock.class,
+        MethodReference.class,
+        SpecialConstructorCall.class,
+        FloatLiteral.class,
+        TypeDeclaration.class,
+        PackageReference.class,
+        SuperConstructorReference.class,
+        SeqSub.class,
+        Positive.class,
+        SchematicFieldReference.class,
+        TypeCast.class,
+        ForToWhile.class,
+        LogicalOr.class,
+        LabelJumpStatement.class,
+        ReattachLoopInvariant.class,
+        Switch.class,
+        InterfaceDeclaration.class,
+        JML_NULLABLE_BY_DEFAULT.class,
+        PostDecrement.class,
+        Break.class,
+        TypeDeclaration.class,
+        CcatchContinueWildcardParameterDeclaration.class,
+        InitArrayCreation.class,
+        TypeRef.class,
+        UnsignedShiftRightAssignment.class,
+        EnumClassDeclaration.class,
+        CatchAllStatement.class,
+        LoopInit.class,
+        TypeReferenceImp.class,
+        MethodOrConstructorReference.class,
+        ForToWhile.class,
+        FieldReference.class,
+        PostIncrement.class,
+        ForToWhile.class,
+        MultipleVarDecl.class,
+        EnumClassDeclaration.class,
+        TypeDeclaration.class,
+        Break.class,
+        Conditional.class,
+        JavaDeclaration.class,
+        CompilationUnit.class,
+        PostWork.class,
+        JML_HELPER.class,
+        ReattachLoopInvariant.class,
+        ClassDeclaration.class,
+        ConstructorDeclaration.class,
+        LessOrEquals.class,
+        Modulo.class,
+        ThisReference.class,
+        UnwindLoop.class,
+        ArrayReference.class,
+        InterfaceDeclaration.class,
+        UnwindLoop.class,
+        EnhancedForElimination.class,
+        MethodCall.class,
+        PostWork.class,
+        LocalVariableDeclaration.class,
+        ReferencePrefix.class,
+        ExactInstanceof.class,
+        EvaluateArgs.class,
+        FieldReference.class,
+        EnumClassDeclaration.class,
+        ExpandMethodBody.class,
+        Switch.class,
+        Unpack.class,
+        ContextStatementBlock.class,
+        SpecialConstructorReference.class,
+        Exec.class,
+        ConstructorCall.class,
+        VariableNamer.IndProgramElementName.class,
+        IsStatic.class,
+        ProgramSV.class,
+        ArrayLength.class,
+        BranchStatement.class,
+        PostIncrement.class,
+        ProgramSV.class,
+        ForInitUnfoldTransformer.class,
+        PackageReference.class,
+        Operator.class,
+        Label.class,
+        TypeDeclaration.class,
+        JML_SPEC_PACKAGE.class,
+        SwitchToIf.class,
+        ExpandMethodBody.class,
+        ExpandMethodBody.class,
+        Instanceof.class,
+        Switch.class,
+        TypeReference.class,
+        CcatchContinueLabelParameterDeclaration.class,
+        ForInitUnfoldTransformer.class,
+        Throws.class,
+        SuperArrayDeclaration.class,
+        BinaryOrAssignment.class,
+        ExpandMethodBody.class,
+        UnsignedShiftRightAssignment.class,
+        Equals.class,
+        ProgramConstruct.class,
+        ExactInstanceof.class,
+        NotEquals.class,
+        PostIncrement.class,
+        ShiftRight.class,
+        SuperArrayDeclaration.class,
+        SchemaTypeReference.class,
+        TypeReferenceImp.class,
+        ForToWhile.class,
+        ConstructorCall.class,
+        FieldDeclaration.class,
+        LogicalAnd.class,
+        EvaluateArgs.class,
+        ParenthesizedExpression.class,
+        ConstructorCall.class,
+        SeqLength.class,
+        SeqConcat.class,
+        EnumClassDeclaration.class,
+        SuperConstructorReference.class,
+        PackageSpecification.class,
+        ClassInitializer.class,
+        ProgramSV.class,
+        PRIVATE.class,
+        InitArray.class,
+        UnwindLoop.class,
+        ExecutionContext.class,
+        ProgramConstruct.class,
+        New.class,
+        ArrayPostDecl.class,
+        For.class,
+        MethodFrame.class,
+        ForUpdates.class,
+        SuperArrayDeclaration.class,
+        Unpack.class,
+        ArrayLengthReference.class,
+        LoopInitializer.class,
+        ClassDeclaration.class,
+        DoBreak.class,
+        BranchStatement.class,
+        InterfaceDeclaration.class,
+        JavaDeclaration.class,
+        SetStatement.class,
+        Finally.class,
+        Ccatch.class,
+        EnhancedForElimination.class,
+        PassiveExpression.class,
+        SeqGet.class,
+        ArrayReference.class,
+        AllFields.class,
+        MethodDeclaration.class,
+        SwitchToIf.class,
+        For.class,
+        ConstructorCall.class,
+        ExpressionJumpStatement.class,
+        Case.class,
+        LoopScopeBlock.class,
+        SetMinus.class,
+        IntLiteral.class,
+        ThisReference.class,
+        ProgramTransformer.class,
+        ShiftRightAssignment.class,
+        Import.class,
+        SpecialConstructorCall.class,
+        PreDecrement.class,
+        Ghost.class,
+        LabelJumpStatement.class,
+        PostDecrement.class,
+        TypeCast.class,
+        EvaluateArgs.class,
+        StaticInitialisation.class,
+        MethodCall.class,
+        Unpack.class,
+        ConstructorReference.class,
+        ForUpdates.class,
+        ProgramTransformer.class,
+        ProgramElement.class,
+        Then.class,
+        SynchronizedBlock.class,
+        ArrayDeclaration.class,
+        NON_SEALED.class,
+        ShiftRight.class,
+        TypeOperator.class,
+        Extends.class,
+        GreaterOrEquals.class,
+        ArrayReference.class,
+        DoBreak.class,
+        SuperReference.class,
+        Abstract.class,
+        Catch.class,
+        UnsignedShiftRightAssignment.class,
+        TypeReferenceImp.class,
+        TypeOf.class,
+        LocationVariable.class,
+        Expression.class,
+        Transient.class,
+        AnnotationUseSpecification.class,
+        ExpandMethodBody.class,
+        SpecialConstructorReference.class,
+        BinaryXOr.class,
+        BinaryAndAssignment.class,
+        ForToWhile.class,
+        Equals.class,
+        PostWork.class,
+        SwitchToIf.class,
+        JavaStatement.class,
+        ArrayDeclaration.class,
+        MethodReference.class,
+        ThisConstructorReference.class,
+        JML_NO_STATE.class,
+        ProgramSV.class,
+        MethodDeclaration.class,
+        DoubleLiteral.class,
+        EnhancedFor.class,
+        ProgramConstruct.class,
+        Default.class,
+        FreeLiteral.class,
+        Literal.class,
+        InheritanceSpecification.class,
+        JML_PACKAGE.class,
+        ThisConstructorReference.class,
+        FieldReference.class,
+        PUBLIC.class,
+        SpecialConstructorCall.class,
+        BinaryXOrAssignment.class,
+        CcatchReturnValParameterDeclaration.class,
+        ClassInitializer.class,
+        Assert.class,
+        PostWork.class,
+        Break.class,
+        InitArrayCreation.class,
+        TypeDeclaration.class,
+        Singleton.class,
+        ExpandMethodBody.class,
+        Private.class,
+        CcatchBreakWildcardParameterDeclaration.class,
+        VariableDeclaration.class,
+        CreateObject.class,
+        InitArray.class,
+        IExecutionContext.class,
+        SchematicFieldReference.class,
+        JmlAssert.class,
+        VariableNamer.IndProgramElementName.class,
+        SeqPut.class,
+        Assignment.class,
+        MethodCall.class,
+        Try.class,
+        SeqIndexOf.class,
+        BinaryOr.class,
+        ConstructorCall.class,
+        JML_NON_NULL.class,
+        JML_SPEC_BIGINT_MATH.class,
+        ProgramConstruct.class,
+        Do.class,
+        CcatchReturnValParameterDeclaration.class,
+        IsStatic.class,
+        MethodReference.class,
+        ExpandMethodBody.class,
+        PostWork.class,
+        ConstructorDeclaration.class,
+        BinaryAnd.class,
+        If.class,
+        FieldReference.class,
+        SuperConstructorReference.class,
+        VariableNamer.IndProgramElementName.class,
+        Exec.class,
+        FieldDeclaration.class,
+        CreateObject.class,
+        LessThan.class,
+        LoopStatement.class,
+        Import.class,
+        ProgramConstruct.class,
+        Case.class,
+        UnwindLoop.class,
+        Catch.class,
+        EmptyMapLiteral.class,
+        VariableReference.class,
+        MethodReference.class,
+        TypeOperator.class,
+        JML_SPEC_PUBLIC.class,
+        TypeCast.class,
+        CreateObject.class,
+        JavaNonTerminalProgramElement.class,
+        Intersect.class,
+        TypeReferenceImp.class,
+        ArrayPostDecl.class,
+        PlusAssignment.class,
+        Times.class,
+        DoBreak.class,
+        ABSTRACT.class,
+        ForInitUnfoldTransformer.class,
+        ShiftLeftAssignment.class,
+        Protected.class,
+        TypeScope.class,
+        ForInitUnfoldTransformer.class,
+        IsStatic.class,
+        ClassDeclaration.class,
+        LogicalNot.class,
+        EmptySetLiteral.class,
+        ProgramSV.class,
+        Switch.class,
+        VariableDeclaration.class,
+        ForToWhile.class,
+        MultipleVarDecl.class,
+        SuperArrayDeclaration.class,
+        StaticInitialisation.class,
+        ConstructorDeclaration.class,
+        TypeOf.class,
+        InitArray.class,
+        MethodBodyStatement.class,
+        BinaryXOrAssignment.class,
+        SpecialConstructorCall.class,
+        CcatchBreakLabelParameterDeclaration.class,
+        ClassInitializer.class,
+        Guard.class,
+        Statement.class,
+        InterfaceDeclaration.class,
+        ConstructorCall.class,
+        Unpack.class,
+        MethodDeclaration.class,
+        ArrayPostDecl.class,
+        TypeOf.class,
+        EvaluateArgs.class,
+        SwitchToIf.class,
+        MultipleVarDecl.class,
+        Plus.class,
+        JumpStatement.class,
+        Times.class,
+        BinaryNot.class,
+        ConstructorDeclaration.class,
+        ClassDeclaration.class,
+        SeqIndexOf.class,
+        FieldSpecification.class,
+        MethodBodyStatement.class,
+        ProgramSV.class,
+        SeqConcat.class,
+        ModuloAssignment.class,
+        RealLiteral.class,
+        BinaryOperator.class,
+        BinaryXOr.class,
+        Then.class,
+        SpecialConstructorCall.class,
+        For.class,
+        TimesAssignment.class,
+        Unpack.class,
+        StringLiteral.class,
+        MethodDeclaration.class,
+        TypeDeclarationContainer.class,
+        Literal.class,
+        BooleanLiteral.class,
+        PreDecrement.class,
+        STRICTFP.class,
+        StatementBlock.class,
+        CcatchContinueLabelParameterDeclaration.class,
+        MultipleVarDecl.class,
+        LocalVariableDeclaration.class,
+        Reference.class,
+        TypeRef.class,
+        MultipleVarDecl.class,
+        ReattachLoopInvariant.class,
+        MethodDeclaration.class,
+        MultipleVarDecl.class,
+        EnhancedFor.class,
+        JML_INSTANCE.class,
+        Conditional.class,
+        UnwindLoop.class,
+        SpecialConstructorReference.class,
+        EnhancedForElimination.class,
+        While.class,
+        DoBreak.class,
+        UnsignedShiftRight.class,
+        MethodFrame.class,
+        ArrayLengthReference.class,
+        SpecialConstructorReference.class,
+        IsStatic.class,
+        Else.class,
+        JML_OT_REP.class,
+        ProgramTransformer.class,
+        MethodCall.class,
+        NameReference.class,
+        ForUpdates.class,
+        ConstructorCall.class,
+        ConstructorDeclaration.class,
+        MethodReference.class,
+        Assert.class,
+        SwitchToIf.class,
+        ArrayPostDecl.class,
+        CopyAssignment.class,
+        FieldSpecification.class,
+        InitArrayCreation.class,
+        UnwindLoop.class,
+        Exec.class,
+        TypeOf.class,
+        SeqIndexOf.class,
+        TypeRef.class,
+        VOLATILE.class,
+        EvaluateArgs.class,
+        SEALED.class,
+        LogicalNot.class,
+        DoBreak.class,
+        CcatchContinueParameterDeclaration.class,
+        ProgramSV.class,
+        Modulo.class,
+        EnhancedForElimination.class,
+        ProgramConstruct.class,
+        ProgramMethod.class,
+        MethodName.class,
+        Default.class,
+        ProgramTransformer.class,
+        JML_CODE.class,
+        ModuloAssignment.class,
+        ShiftLeft.class,
+        Negative.class,
+        Case.class,
+        NewArray.class,
+        Ccatch.class,
+        Switch.class,
+        MethodCall.class,
+        ProgramConstant.class,
+        PackageReferenceContainer.class,
+        BinaryOrAssignment.class,
+        TypeReferenceInfix.class,
+        ComparativeOperator.class,
+        DoBreak.class,
+        PreDecrement.class,
+        UnsignedShiftRightAssignment.class,
+        InitArrayCreation.class,
+        JML_SPEC_PRIVATE.class,
+        StatementBlock.class,
+        ProgramConstruct.class,
+        FieldDeclaration.class,
+        FieldReference.class,
+        ExpandMethodBody.class,
+        PROTECTED.class,
+        Finally.class,
+        SuperArrayDeclaration.class,
+        Do.class,
+        AbstractIntegerLiteral.class,
+        MethodCall.class,
+        ExpandMethodBody.class,
+        Extends.class,
+        SchematicFieldReference.class,
+        StaticInitialisation.class,
+        TypeOf.class,
+        JML_CODE_JAVA_MATH.class,
+        LoopStatement.class,
+        SeqPut.class,
+        SpecialConstructorReference.class,
+        TypeCast.class,
+        JML_STRICTLY_PURE.class,
+        DLEmbeddedExpression.class,
+        ReattachLoopInvariant.class,
+        TypeRef.class,
+        IProgramMethod.class,
+        CcatchContinueParameterDeclaration.class,
+        PreIncrement.class,
+        TypeOf.class,
+        MergePointStatement.class,
+        CharLiteral.class,
+        ModuloAssignment.class,
+        ConstructorReference.class,
+        JML_UNPARSABLE_MODIFIERS.class,
+        MultipleVarDecl.class,
+        PostWork.class,
+        SchemaTypeReference.class,
+        ArrayPostDecl.class,
+        ScopeDefiningElement.class,
+        JavaStatement.class,
+        CharLiteral.class,
+        Divide.class,
+        TypeRef.class,
+        InheritanceSpecification.class,
+        ComparativeOperator.class,
+        SetMinus.class,
+        EmptyStatement.class,
+        SwitchToIf.class,
+        SchematicFieldReference.class,
+        DoBreak.class,
+        JML_NULLABLE.class,
+        SeqReverse.class,
+        Try.class,
+        LoopInit.class,
+        ExpressionContainer.class,
+        IsStatic.class,
+        ProgramConstruct.class,
+        New.class,
+        EmptySetLiteral.class,
+        ForInitUnfoldTransformer.class,
+        BinaryOperator.class,
+        LabeledStatement.class,
+        MinusAssignment.class,
+        Operator.class,
+        MethodDeclaration.class,
+        MethodReference.class,
+        Extends.class,
+        ForToWhile.class,
+        IsStatic.class,
+        GreaterOrEquals.class,
+        Native.class,
+        ShiftLeftAssignment.class,
+        LabeledStatement.class,
+        ArrayReference.class,
+        PackageReference.class,
+        Unpack.class,
+        Minus.class,
+        MemberDeclaration.class,
+        SpecialConstructorCall.class,
+        Divide.class,
+        MemberReference.class,
+        TypeReference.class,
+        InitArray.class,
+        SchematicFieldReference.class,
+        ExpandMethodBody.class,
+        Throws.class,
+        IForUpdates.class,
+        Volatile.class,
+        SuperReference.class,
+        StaticInitialisation.class,
+        ExpressionStatement.class,
+        TypeRef.class,
+        SchematicFieldReference.class,
+        InheritanceSpecification.class,
+        Catch.class,
+        LogicalOr.class,
+        ModuloAssignment.class,
+        Import.class,
+        Catch.class,
+        ProgramElementName.class,
+        InterfaceDeclaration.class,
+        Instanceof.class,
+        New.class,
+        Continue.class,
+        ProgramSV.class,
+        SchematicFieldReference.class,
+        Implements.class,
+        BinaryAnd.class,
+        ShiftLeftAssignment.class,
+        PreDecrement.class,
+        Ccatch.class,
+        Static.class,
+        Return.class,
+        TRANSIENT.class,
+        PackageSpecification.class,
+        TypeOperator.class,
+        TypeReferenceImp.class,
+        Branch.class,
+        Operator.class,
+        Exec.class,
+        ReattachLoopInvariant.class,
+        Divide.class,
+        AllFields.class,
+        SeqLength.class,
+        ForToWhile.class,
+        NamedProgramElement.class,
+        JML_NON_NULL_ELEMENTS.class,
+        MethodFrame.class,
+        VariableSpecification.class,
+        BranchImp.class,
+        CreateObject.class,
+        Try.class,
+        BinaryOperator.class,
+        ProgramConstant.class,
+        ProgramVariable.class,
+        Switch.class,
+        MinusAssignment.class,
+        PostIncrement.class,
+        SeqReverse.class,
+        SetUnion.class,
+        MethodFrame.class,
+        Guard.class,
+        JML_PURE.class,
+        CcatchReturnValParameterDeclaration.class,
+        PlusAssignment.class,
+        LessOrEquals.class,
+        InitArray.class,
+        Assert.class,
+        EnhancedForElimination.class,
+        EnhancedForElimination.class,
+        SchematicFieldReference.class,
+        LogicalAnd.class,
+        JML_SPEC_PROTECTED.class,
+        Equals.class,
+        ConstructorReference.class,
+        ConstructorDeclaration.class,
+        ShiftLeft.class,
+        SwitchToIf.class,
+        SuperConstructorReference.class,
+        Guard.class,
+        ArrayDeclaration.class,
+        ProgramVariable.class,
+        ProgramMethod.class,
+        IsStatic.class,
+        IsStatic.class,
+        MergePointStatement.class,
+        PostDecrement.class,
+        For.class,
+        StaticInitialisation.class,
+        ProgramTransformer.class,
+        MultipleVarDecl.class,
+        SchemaTypeReference.class,
+        EnumClassDeclaration.class,
+        TypeRef.class,
+        FieldDeclaration.class,
+        FINAL.class,
+        MetaClassReference.class,
+        SeqSingleton.class,
+        LocalVariableDeclaration.class,
+        IGuard.class,
+        ProgramVariableName.class,
+        ProgramConstruct.class,
+        SchemaTypeReference.class,
+        Else.class,
+        ProgramConstruct.class,
+        Continue.class,
+        TypeRef.class,
+        TypeRef.class,
+        ReattachLoopInvariant.class,
+        ConstructorCall.class,
+        EnumClassDeclaration.class,
+        Do.class,
+        MethodCall.class,
+        BinaryOrAssignment.class,
+        ArrayLengthReference.class,
+        Positive.class,
+        SchematicFieldReference.class,
+        PostWork.class,
+        EmptyStatement.class,
+        SpecialConstructorCall.class,
+        Break.class,
+        ForUpdates.class,
+        ArrayPostDecl.class,
+        EvaluateArgs.class,
+        InitArray.class,
+        MethodDeclaration.class,
+        TypeReferenceImp.class,
+        Unpack.class,
+        InitArray.class,
+        TimesAssignment.class,
+        MethodReference.class,
+        ReattachLoopInvariant.class,
+        ProgramConstruct.class,
+        IsStatic.class,
+        JavaDeclaration.class,
+        Catch.class,
+        DivideAssignment.class,
+        ProgramPrefix.class,
+        SuperReference.class,
+        LabelJumpStatement.class,
+        Throw.class,
+        TypeReference.class,
+        CatchAllStatement.class,
+        InitArray.class,
+        ClassInitializer.class,
+        TypeRef.class,
+        BranchImp.class,
+        TransactionStatement.class,
+        ParameterContainer.class,
+        VariableScope.class,
+        Final.class,
+        DEFAULT.class,
+        TRANSITIVE.class,
+        StatementContainer.class,
+        NATIVE.class,
+        TypeReferenceContainer.class,
+        TerminalProgramElement.class,
+        SYNCHRONIZED.class,
+        JML_OT_READ_ONLY.class,
+        NoState.class,
+        Modifier.class,
+        VisibilityModifier.class,
+        CcatchReturnParameterDeclaration.class,
+        VariableNamer.PermIndProgramElementName.class,
+        Subtype.class,
+        AllObjects.class,
+        Declaration.class,
+        JML_CODE_BIGINT_MATH.class,
+        JavaProgramElement.class,
+        LongLiteral.class,
+        ParameterDeclaration.class,
+        JML_SPEC_JAVA_MATH.class,
+        TwoState.class,
+        ILoopInit.class,
+        Model.class,
+        ReferenceSuffix.class,
+        JML_TWO_STATE.class,
+        CcatchNonstandardParameterDeclaration.class,
+        StrictFp.class,
+        EmptySeqLiteral.class,
+        AbstractProgramElement.class,
+        Synchronized.class,
+        JML_NON_NULL_BY_DEFAULT.class,
+        JML_CODE_SAFE_MATH.class,
+        Public.class,
+        JML_SPEC_SAFE_MATH.class,
+        VariableNamer.TempIndProgramElementName.class,
+        Modifiers.STATIC.class));
+
+    public static void main(String[] args) throws FileNotFoundException {
+        var all = new TreeSet<Class<?>>(Comparator.comparing(Class::getName));
+        all.addAll(allClasses);
+
+        System.out.println(all.size());
+        var cu = new com.github.javaparser.ast.CompilationUnit();
+
+        for (var clazz : all) {
+            var r = new ClassOrInterfaceDeclaration();
+            r.setName(clazz.getSimpleName());
+            if (clazz.getSuperclass() != null) {
+                r.getExtendedTypes()
+                        .add(new ClassOrInterfaceType(null, clazz.getSuperclass().getSimpleName()));
+            }
+
+            if (clazz.accessFlags().contains(AccessFlag.ABSTRACT)) {
+                r.addModifier(com.github.javaparser.ast.Modifier.DefaultKeyword.ABSTRACT);
+            }
+
+            for (var declaredField : clazz.getDeclaredFields()) {
+                if (declaredField.isSynthetic()
+                        || declaredField.accessFlags().contains(AccessFlag.STATIC)
+                        || declaredField.accessFlags().contains(AccessFlag.PRIVATE))
+                    continue;
+
+                String type;
+                if (declaredField.getType().getTypeParameters().length == 0)
+                    type = declaredField.getType().getSimpleName();
+                else {
+                    type = declaredField.getGenericType().toString();
+                    int j = type.lastIndexOf('<');
+                    int i = type.lastIndexOf('.', j);
+                    type = type.substring(i + 1);
+                }
+                System.out.println(type);
+                r.addField(type, declaredField.getName());
+            }
+
+
+            cu.addType(r);
+        }
+
+        try (var out =
+            new PrintWriter(new File("key.ncore.java/src/adt/java-ast.java").getAbsoluteFile())) {
+            out.write(cu.toString());
+        }
+    }
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java b/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java
new file mode 100644
index 0000000000..333ea81444
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/AssignmentKind.java
@@ -0,0 +1,25 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+public enum AssignmentKind {
+    Copy(""),
+    BinaryOr("|"),
+    Divide("/"),
+    ShiftLeft("<<"),
+    UnsignedShiftRight(">>>"),
+    Plus("+"),
+    ShiftRight(">>"),
+    Minus("-"),
+    Modulo("%"),
+    Times("*"),
+    BinaryAnd("&"),
+    BinaryXOr("^");
+
+    public final String symbol;
+
+    AssignmentKind(String symbol) {
+        this.symbol = symbol;
+    }
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java b/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java
new file mode 100644
index 0000000000..c35471eafb
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/BinaryOperatorKind.java
@@ -0,0 +1,40 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+public enum BinaryOperatorKind {
+    DIVIDE(2, "/"),
+    MODULO(2, "%"),
+    TIMES(2, "*"),
+    MINUS(3, "-"),
+    PLUS(3, "+"),
+    SUBTYPE(3, "<:"),
+
+    SHIFT_LEFT(4, "<<"),
+    SHIFT_RIGHT(4, ">>"),
+    UNSIGNED_SHIFT_RIGHT(4, ">>>"),
+
+    GREATER_OR_EQUALS(5, ">="),
+    LESS_OR_EQUALS(5, "<="),
+    GREATER_THAN(5, ">"),
+    LESS_THAN(5, "<"),
+    EQUALS(6, "=="),
+    NOT_EQUALS(6, "!="),
+
+
+    BINARY_AND(7, "&"),
+    BINARY_XOR(8, "^"),
+    BINARY_OR(9, "|"),
+    LOGICAL_AND(10, "&&"),
+    LOGICAL_OR(11, "||");
+
+
+    public final int precedence;
+    public final String symbol;
+
+    BinaryOperatorKind(int precedence, String symbol) {
+        this.precedence = precedence;
+        this.symbol = symbol;
+    }
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java b/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java
new file mode 100644
index 0000000000..12e5d82909
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/DefaultProperties.java
@@ -0,0 +1,37 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (4/12/26)
+ */
+@SuppressWarnings("unchecked")
+public class DefaultProperties implements Properties {
+    private final Map<Property<?>, Object> properties = new HashMap<>();
+
+    @Override
+    public <T> T get(Property<T> property, T defaultValue) {
+        return (T) properties.getOrDefault(property, defaultValue);
+    }
+
+    @Override
+    public <T> T get(Property<T> property) {
+        return (T) properties.get(property);
+    }
+
+    @Override
+    public <T> boolean contains(Property<T> property) {
+        return properties.containsKey(property);
+    }
+
+    @Override
+    public <T> void set(Property<T> property, T value) {
+        properties.put(property, value);
+    }
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java
new file mode 100644
index 0000000000..b2994df22b
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/EqEx.java
@@ -0,0 +1,16 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/// Exclude a field from equality and hashCode.
+@Retention(RetentionPolicy.SOURCE)
+@Target({ ElementType.PARAMETER, ElementType.FIELD })
+public @interface EqEx {
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java b/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java
new file mode 100644
index 0000000000..f2310f32b8
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/LogicFunction.java
@@ -0,0 +1,34 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+public enum LogicFunction {
+    Intersect(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\intersect")),
+    SetUnion(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\set_union")),
+    SetMinus(2, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\set_minus")),
+    AllObjects(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\all_objects")),
+    SeqPut(3, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_upd")),
+    SeqGet(1, 1, PrimitiveType.JAVA_INT, AsArrayAccess()),
+    SeqReverse(1, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_reverse")),
+    AllFields(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\all_fields")),
+    SeqIndexOf(2, 1, PrimitiveType.JAVA_INT, AsFunction("\\indexOf")),
+    SeqSingleton(1, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_singleton")),
+    SeqSub(3, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_sub")),
+    SeqConcat(2, 1, PrimitiveType.JAVA_SEQ, AsFunction("\\seq_concat")),
+    Singleton(1, 1, PrimitiveType.JAVA_LOCSET, AsFunction("\\singleton")),
+    SeqLength(1, 1, PrimitiveType.JAVA_INT, AsSuffix("length"));
+
+    public final int arity;
+    public final int precedence;
+    public final PrimitiveType returnType;
+    public final PrettyPrinter.PrintOp format;
+
+    LogicFunction(int arity, int precedence, PrimitiveType returnType,
+            PrettyPrinter.PrintOp format) {
+        this.arity = arity;
+        this.precedence = precedence;
+        this.returnType = returnType;
+        this.format = format;
+    }
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java
new file mode 100644
index 0000000000..3749f94748
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Package.java
@@ -0,0 +1,16 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/// Sets the suffix of the package with respect to `org.key_project.java.ast`
+@Retention(RetentionPolicy.SOURCE)
+@Target({ ElementType.TYPE })
+public @interface Package {
+    String value() default "";
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java
new file mode 100644
index 0000000000..b72d394f04
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Properties.java
@@ -0,0 +1,19 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (4/12/26)
+ */
+public interface Properties {
+    <T> T get(Property<T> property, T defaultValue);
+
+    <T> T get(Property<T> property);
+
+    <T> boolean contains(Property<T> property);
+
+    <T> void set(Property<T> property, T value);
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java
new file mode 100644
index 0000000000..a74364cd51
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Property.java
@@ -0,0 +1,28 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+import com.github.javaparser.ast.Node;
+
+/**
+ * A key to a piece of data associated with a {@link Node} at runtime.
+ * The key contains type information that can be used to check the
+ * type of any user data value for the key when the value is set. DataKey is abstract in order to
+ * force the creation of a subtype. That subtype is used to test for identity when looking for the
+ * user data because actual object identity would suffer from problems under serialization.
+ * So, the correct way to declare a DataKey is like this:
+ * <p>
+ * <pre>
+ * {@code
+ * public static final DataKey<Role> ROLE = new DataKey<Role>() { };
+ * }
+ * </pre>
+ * <p>
+ * This code was taken from the <a href="http://wicket.apache.org/">Wicket project</a>.
+ *
+ * @param <T> The type of the object which is stored
+ * @see Node#getData(com.github.javaparser.ast.DataKey)
+ */
+public record Property<T>(String name) {
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java
new file mode 100644
index 0000000000..cfec916d19
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Root.java
@@ -0,0 +1,16 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/// Marks the ROOT class of the hierarchy
+@Retention(RetentionPolicy.SOURCE)
+@Target({ ElementType.TYPE })
+public @interface Root {
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java b/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java
new file mode 100644
index 0000000000..71f9f869ce
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/UnaryOperatorKind.java
@@ -0,0 +1,31 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+public enum UnaryOperatorKind {
+    LOGICAL_NOT("!", 1),
+    NEGATIVE("-", 1),
+    POSITIVE("+", 1),
+    BINARY_NOT("~", 1),
+
+    PRE_INCREMENT("++", 0),
+    PRE_DECREMENT("--", 0),
+    POST_INCREMENT("++", 0, POSTFIX),
+    POST_DECREMENT("--", 0, POSTFIX);
+
+
+    public final String symbol;
+    public final int precedence;
+    public final int notation;
+
+    UnaryOperatorKind(String symbol, int precedence) {
+        this(symbol, precedence, PREFIX);
+    }
+
+    UnaryOperatorKind(String symbol, int precedence, int notation) {
+        this.symbol = symbol;
+        this.notation = notation;
+        this.precedence = precedence;
+    }
+}
diff --git a/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java b/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java
new file mode 100644
index 0000000000..6b4ee339d3
--- /dev/null
+++ b/key.ncore.java/src/main/java/org/key_project/java/ast/Visitable.java
@@ -0,0 +1,19 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.java.ast;
+
+import org.key_project.java.ast.visitor.*;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (4/19/26)
+ */
+public interface Visitable {
+    <R> R accept(Visitor<R> visitor);
+
+    <R, A> R accept(ArgVisitor<R, A> visitor, A arg);
+
+    void accept(VoidVisitor visitor);
+}
diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java
index 70936b1307..110271c6a2 100644
--- a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java
+++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java
@@ -14,7 +14,7 @@
 import org.jspecify.annotations.Nullable;
 
 public class ImmutableArray<S extends @Nullable Object>
-        implements java.lang.Iterable<S>, java.io.Serializable {
+        implements RoList<S>, java.io.Serializable {
 
     private static final long serialVersionUID = -9041545065066866250L;
 
@@ -106,7 +106,7 @@ public final boolean isEmpty() {
         return content.length == 0;
     }
 
-    public boolean contains(S op) {
+    public boolean contains(Object op) {
         for (S el : content) {
             if (Objects.equals(el, op)) {
                 return true;
@@ -174,6 +174,16 @@ public Iterator<S> iterator() {
         return new ArrayIterator<S>(this);
     }
 
+    @Override
+    public S getFirst() {
+        return this.content[0];
+    }
+
+    @Override
+    public S getLast() {
+        return this.content[this.content.length - 1];
+    }
+
     private static class ArrayIterator<T extends @Nullable Object> implements Iterator<T> {
 
         private int i = 0;
diff --git a/key.util/src/main/java/org/key_project/util/collection/RoList.java b/key.util/src/main/java/org/key_project/util/collection/RoList.java
new file mode 100644
index 0000000000..adc6f12905
--- /dev/null
+++ b/key.util/src/main/java/org/key_project/util/collection/RoList.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
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.util.collection;
+
+import java.util.*;
+import java.util.function.BiConsumer;
+import java.util.function.BinaryOperator;
+import java.util.function.Function;
+import java.util.function.Supplier;
+import java.util.stream.Collector;
+import java.util.stream.Stream;
+
+import org.jspecify.annotations.Nullable;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (4/19/26)
+ */
+public interface RoList<E extends @Nullable Object> extends Iterable<E> {
+    RoList<?> EMPTY = new RoList<>() {
+        @Override
+        public int size() {
+            return 0;
+        }
+
+        @Override
+        public Object get(int index) {
+            throw new IndexOutOfBoundsException();
+        }
+
+        @Override
+        public boolean isEmpty() {
+            return true;
+        }
+
+        @Override
+        public boolean contains(Object e) {
+            return false;
+        }
+
+        @Override
+        public Iterator<Object> iterator() {
+            return new Iterator<>() {
+                @Override
+                public boolean hasNext() {
+                    return false;
+                }
+
+                @Override
+                public Object next() {
+                    throw new NoSuchElementException();
+                }
+            };
+        }
+
+        @Override
+        public Object getFirst() {
+            throw new NoSuchElementException();
+        }
+
+        @Override
+        public Object getLast() {
+            throw new NoSuchElementException();
+        }
+
+        @Override
+        public Stream<Object> stream() {
+            return Stream.empty();
+        }
+    };
+
+    static <T> Collector<? super T, List<T>, RoList<T>> collector() {
+        return new Collector<>() {
+            @Override
+            public Supplier<List<T>> supplier() {
+                return ArrayList::new;
+            }
+
+            @Override
+            public BiConsumer<List<T>, T> accumulator() {
+                return List::add;
+            }
+
+            @Override
+            public BinaryOperator<List<T>> combiner() {
+                return (a, b) -> {
+                    a.addAll(b);
+                    return a;
+                };
+            }
+
+            @Override
+            public Function<List<T>, RoList<T>> finisher() {
+                return (a) -> RoList.fromList(a);
+            }
+
+            @Override
+            public Set<Characteristics> characteristics() {
+                return Set.of();
+            }
+        };
+    }
+
+    static <T> RoList<T> fromList(List<T> a) {
+        if (a.isEmpty()) {
+            return RoList.empty();
+        } else if (a.size() == 1) {
+            return RoList.singleton(a.getFirst());
+        } else {
+            return new ImmutableArray<>(a);
+        }
+    }
+
+    static <T> RoList<T> singleton(T item) {
+        return new SingletonRoList<>(item);
+    }
+
+    static <T> RoList<T> empty() {
+        return (RoList<T>) EMPTY;
+    }
+
+    int size();
+
+    E get(int index);
+
+    boolean isEmpty();
+
+    default boolean isNonEmpty() {
+        return !isEmpty();
+    }
+
+    boolean contains(Object e);
+
+    Iterator<E> iterator();
+
+    E getFirst();
+
+    E getLast();
+
+    Stream<E> stream();
+
+    default List<E> toList() {
+        return stream().toList();
+    }
+}
diff --git a/key.util/src/main/java/org/key_project/util/collection/SingletonRoList.java b/key.util/src/main/java/org/key_project/util/collection/SingletonRoList.java
new file mode 100644
index 0000000000..b42b35f0c3
--- /dev/null
+++ b/key.util/src/main/java/org/key_project/util/collection/SingletonRoList.java
@@ -0,0 +1,75 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package org.key_project.util.collection;
+
+import java.util.Iterator;
+import java.util.NoSuchElementException;
+import java.util.Objects;
+import java.util.stream.Stream;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (4/19/26)
+ */
+public record SingletonRoList<T>(T item) implements RoList<T> {
+    @Override
+    public int size() {
+        return 1;
+    }
+
+    @Override
+    public T get(int index) {
+        if (index == 0) {
+            return item();
+        }
+        throw new IndexOutOfBoundsException();
+    }
+
+    @Override
+    public boolean isEmpty() {
+        return false;
+    }
+
+    @Override
+    public boolean contains(Object e) {
+        return Objects.equals(e, item);
+    }
+
+    @Override
+    public Iterator<T> iterator() {
+        return new Iterator<>() {
+            private boolean called;
+
+            @Override
+            public boolean hasNext() {
+                return !called;
+            }
+
+            @Override
+            public T next() {
+                if (called) {
+                    throw new NoSuchElementException();
+                }
+                called = true;
+                return item;
+            }
+        };
+    }
+
+    @Override
+    public T getFirst() {
+        return item;
+    }
+
+    @Override
+    public T getLast() {
+        return item;
+    }
+
+    @Override
+    public Stream<T> stream() {
+        return Stream.of(item);
+    }
+}
diff --git a/settings.gradle b/settings.gradle
index 00226f6fa8..282af3d986 100644
--- a/settings.gradle
+++ b/settings.gradle
@@ -7,6 +7,7 @@ plugins {
 include "key.util"
 include "key.ncore"
 include 'key.ncore.calculus'
+include 'key.ncore.java'
 
 include "key.core"
 //include "key.core.rifl"