diff --git a/build.gradle b/build.gradle
index 00bbb889424d0e7c17b560d7bc8a19973fe50239..f6e41249811fb69ba01942d318284970983ebc00 100644
--- a/build.gradle
+++ b/build.gradle
@@ -40,7 +40,7 @@ configurations.all {
 dependencies {
 	compile(group: "de.hhu.stups", name: "de.prob2.kernel", version: "3.2.12-SNAPSHOT", changing: true)
 	compile(group: "io.github.spencerpark", name: "jupyter-jvm-basekernel", version: "2.2.2")
-	compile(group: "org.jetbrains", name: "annotations", version: "13.0") // Old version, required for compatibility with Kotlin (which is used by Alloy2B, which is used by ProB 2).
+	compile(group: "org.jetbrains", name: "annotations", version: "17.0.0")
 	compile(group: "se.sawano.java", name: "alphanumeric-comparator", version: "1.4.1")
 }
 
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index dc3999a8c574701758b5110c2552978e1ca9d237..a7b3eb2e4bcf6499962a381ba4df3408c30f2c8b 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -74,7 +74,7 @@ public final class ProBKernel extends BaseKernel {
 	private static final @NotNull Pattern BSYMB_COMMAND_PATTERN = Pattern.compile("\\\\([a-z]+)");
 	private static final @NotNull Pattern LATEX_FORMULA_PATTERN = Pattern.compile("(\\$\\$?)([^\\$]+)\\1");
 	
-	private static final @NotNull Map<String, String> BSYMB_COMMAND_DEFINITIONS;
+	private static final @NotNull Map<@NotNull String, @NotNull String> BSYMB_COMMAND_DEFINITIONS;
 	static {
 		final Map<String, String> map = new HashMap<>();
 		map.put("bfalse", "\\newcommand{\\bfalse}{\\mathord\\bot}");
@@ -137,8 +137,8 @@ public final class ProBKernel extends BaseKernel {
 	
 	private final @NotNull AnimationSelector animationSelector;
 	
-	private final @NotNull Map<String, Command> commands;
-	private final @NotNull Map<String, String> variables;
+	private final @NotNull Map<@NotNull String, @NotNull Command> commands;
+	private final @NotNull Map<@NotNull String, @NotNull String> variables;
 	
 	@Inject
 	private ProBKernel(final @NotNull Injector injector, final @NotNull ClassicalBFactory classicalBFactory, final @NotNull AnimationSelector animationSelector) {
@@ -182,11 +182,11 @@ public final class ProBKernel extends BaseKernel {
 		this.animationSelector.changeCurrentAnimation(new Trace(classicalBFactory.create("(initial Jupyter machine)", "MACHINE repl END").load()));
 	}
 	
-	public @NotNull Map<String, Command> getCommands() {
+	public @NotNull Map<@NotNull String, @NotNull Command> getCommands() {
 		return Collections.unmodifiableMap(this.commands);
 	}
 	
-	public @NotNull Map<String, String> getVariables() {
+	public @NotNull Map<@NotNull String, @NotNull String> getVariables() {
 		return this.variables;
 	}
 	
@@ -196,7 +196,7 @@ public final class ProBKernel extends BaseKernel {
 	}
 	
 	@Override
-	public @NotNull List<LanguageInfo.Help> getHelpLinks() {
+	public @NotNull List<LanguageInfo.@NotNull Help> getHelpLinks() {
 		return Collections.singletonList(new LanguageInfo.Help("ProB User Manual", "https://www3.hhu.de/stups/prob/index.php/User_Manual"));
 	}
 	
@@ -367,7 +367,7 @@ public final class ProBKernel extends BaseKernel {
 		this.animationSelector.getCurrentTrace().getStateSpace().kill();
 	}
 	
-	private @NotNull List<String> formatErrorSource(final @NotNull List<String> sourceLines, final @NotNull ErrorItem.Location location) {
+	private @NotNull List<@NotNull String> formatErrorSource(final @NotNull List<@NotNull String> sourceLines, final @NotNull ErrorItem.Location location) {
 		if (sourceLines.isEmpty()) {
 			return Collections.singletonList(this.errorStyler.primary("// Source code not known"));
 		}
@@ -414,7 +414,7 @@ public final class ProBKernel extends BaseKernel {
 	}
 	
 	@Override
-	public @NotNull List<String> formatError(final Exception e) {
+	public @NotNull List<@NotNull String> formatError(final Exception e) {
 		try {
 			LOGGER.warn("Exception while executing command from user", e);
 			if (e instanceof UserErrorException) {
diff --git a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
index 9251873e8a29c1be5951b87f5fffdf21fdedf444..e1fba4bbe1f64ba7efc1eb06fb04d7e8a372e113 100644
--- a/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/CheckCommand.java
@@ -27,7 +27,7 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class CheckCommand implements Command {
-	private static final @NotNull Map<String, String> SECTION_NAME_MAP;
+	private static final @NotNull Map<@NotNull String, @NotNull String> SECTION_NAME_MAP;
 	static {
 		final Map<String, String> sectionNameMap = new HashMap<>();
 		sectionNameMap.put("properties", "PROPERTIES");
diff --git a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
index 7d82d90140cdfdc6add2c202499a93599630b011..929873d45b5e49a812d0bf6f1a728f69b99535c7 100644
--- a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java
@@ -89,7 +89,7 @@ public final class CommandUtils {
 		}
 	}
 	
-	public static @NotNull List<String> splitArgs(final @NotNull String args, final int limit) {
+	public static @NotNull List<@NotNull String> splitArgs(final @NotNull String args, final int limit) {
 		final List<String> split = new ArrayList<>(Arrays.asList(ARG_SPLIT_PATTERN.split(args, limit)));
 		if (!split.isEmpty() && split.get(split.size()-1).isEmpty()) {
 			split.remove(split.size()-1);
@@ -97,11 +97,11 @@ public final class CommandUtils {
 		return split;
 	}
 	
-	public static @NotNull List<String> splitArgs(final @NotNull String args) {
+	public static @NotNull List<@NotNull String> splitArgs(final @NotNull String args) {
 		return splitArgs(args, 0);
 	}
 	
-	public static @NotNull Map<String, String> parsePreferences(final @NotNull List<String> args) {
+	public static @NotNull Map<@NotNull String, @NotNull String> parsePreferences(final @NotNull List<@NotNull String> args) {
 		final Map<String, String> preferences = new HashMap<>();
 		for (final String arg : args) {
 			final String[] split = arg.split("=", 2);
@@ -233,7 +233,7 @@ public final class CommandUtils {
 		);
 	}
 	
-	public static @Nullable DisplayData inspectArgs(final @NotNull String argString, final int at, final @NotNull Inspector... inspectors) {
+	public static @Nullable DisplayData inspectArgs(final @NotNull String argString, final int at, final @NotNull Inspector @NotNull... inspectors) {
 		final Matcher argSplitMatcher = ARG_SPLIT_PATTERN.matcher(argString);
 		int argStart = 0;
 		int argEnd = argString.length();
@@ -252,7 +252,7 @@ public final class CommandUtils {
 		return inspectors[i].inspect(argString.substring(argStart, argEnd), at - argStart);
 	}
 	
-	public static @Nullable ReplacementOptions completeArgs(final @NotNull String argString, final int at, final @NotNull Completer... completers) {
+	public static @Nullable ReplacementOptions completeArgs(final @NotNull String argString, final int at, final @NotNull Completer @NotNull... completers) {
 		final Matcher argSplitMatcher = ARG_SPLIT_PATTERN.matcher(argString);
 		int argStart = 0;
 		int argEnd = argString.length();
diff --git a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
index c9b47eb8184d55311240d820e6fb290e2c63aed1..d21fbd16820f9fa1eaeea2b9f224d64a0fe422fe 100644
--- a/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/LoadFileCommand.java
@@ -37,7 +37,7 @@ import org.slf4j.LoggerFactory;
 public final class LoadFileCommand implements Command {
 	private static final @NotNull Logger LOGGER = LoggerFactory.getLogger(LoadFileCommand.class);
 	
-	private static final @NotNull Map<String, Class<? extends ModelFactory<?>>> EXTENSION_TO_FACTORY_MAP;
+	private static final @NotNull Map<@NotNull String, @NotNull Class<? extends ModelFactory<?>>> EXTENSION_TO_FACTORY_MAP;
 	static {
 		final Map<String, Class<? extends ModelFactory<?>>> extensionToFactoryMap = new HashMap<>();
 		extensionToFactoryMap.put("mch", ClassicalBFactory.class);
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
index 729e565862196379f913c70510988696388d6644..b12b289e3695daca70fd0c656b8ebaae9c2a1b4e 100644
--- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -22,7 +22,7 @@ import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public final class SolveCommand implements Command {
-	private static final @NotNull Map<String, CbcSolveCommand.Solvers> SOLVERS = Arrays.stream(CbcSolveCommand.Solvers.values())
+	private static final @NotNull Map<@NotNull String, CbcSolveCommand.@NotNull Solvers> SOLVERS = Arrays.stream(CbcSolveCommand.Solvers.values())
 		.collect(Collectors.toMap(s -> s.name().toLowerCase(), s -> s));
 	
 	private final @NotNull AnimationSelector animationSelector;