diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 0dbb6e4ac7801f732001d319c74e36c90646a12d..e12135c4c033edd283b2b226eb4f651c21ac5390 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -29,6 +29,7 @@ import de.prob2.jupyter.commands.ConstantsCommand;
 import de.prob2.jupyter.commands.DotCommand;
 import de.prob2.jupyter.commands.EvalCommand;
 import de.prob2.jupyter.commands.ExecCommand;
+import de.prob2.jupyter.commands.FindCommand;
 import de.prob2.jupyter.commands.GotoCommand;
 import de.prob2.jupyter.commands.GroovyCommand;
 import de.prob2.jupyter.commands.HelpCommand;
@@ -158,6 +159,7 @@ public final class ProBKernel extends BaseKernel {
 		this.commands.put(":constants", injector.getInstance(ConstantsCommand.class));
 		this.commands.put(":init", injector.getInstance(InitialiseCommand.class));
 		this.commands.put(":goto", injector.getInstance(GotoCommand.class));
+		this.commands.put(":find", injector.getInstance(FindCommand.class));
 		this.commands.put(":show", injector.getInstance(ShowCommand.class));
 		this.commands.put(":dot", injector.getInstance(DotCommand.class));
 		this.commands.put(":assert", injector.getInstance(AssertCommand.class));
diff --git a/src/main/java/de/prob2/jupyter/commands/FindCommand.java b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
new file mode 100644
index 0000000000000000000000000000000000000000..2abd00ad89d3156933d90119e011ab103ef16849
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/FindCommand.java
@@ -0,0 +1,53 @@
+package de.prob2.jupyter.commands;
+
+import com.google.inject.Inject;
+
+import de.prob.animator.domainobjects.FormulaExpand;
+import de.prob.animator.domainobjects.IEvalElement;
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.Trace;
+
+import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
+import io.github.spencerpark.jupyter.kernel.display.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class FindCommand implements Command {
+	private final @NotNull AnimationSelector animationSelector;
+	
+	@Inject
+	private FindCommand(final @NotNull AnimationSelector animationSelector) {
+		super();
+		
+		this.animationSelector = animationSelector;
+	}
+	
+	@Override
+	public @NotNull String getSyntax() {
+		return ":find PREDICATE";
+	}
+	
+	@Override
+	public @NotNull String getShortHelp() {
+		return "Try to find a state for which the given predicate is true (in addition to the machine's invariant).";
+	}
+	
+	@Override
+	public @NotNull String getHelpBody() {
+		return "If such a state is found, it is made the current state, otherwise an error is displayed.\n\nNote that this command does not necessarily find a valid *trace* to the found state. Instead, in some cases a single \"fake\" transition is added to the trace, which goes directly to the found state and does not use the machine's operations to reach it.";
+	}
+	
+	@Override
+	public @NotNull DisplayData run(final @NotNull String argString) {
+		final Trace trace = this.animationSelector.getCurrentTrace();
+		final IEvalElement pred = trace.getModel().parseFormula(argString, FormulaExpand.EXPAND);
+		final Trace newTrace = trace.getStateSpace().getTraceToState(pred);
+		this.animationSelector.changeCurrentAnimation(newTrace);
+		return new DisplayData("Found state: " + newTrace.getCurrentState().getId());
+	}
+	
+	@Override
+	public @NotNull ReplacementOptions complete(final @NotNull String argString, final int at) {
+		return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
+	}
+}