diff --git a/apps/web/src/routes/kripke/components/formula-input.svelte b/apps/web/src/routes/kripke/components/formula-input.svelte
index a4bd056..9960c6f 100644
--- a/apps/web/src/routes/kripke/components/formula-input.svelte
+++ b/apps/web/src/routes/kripke/components/formula-input.svelte
@@ -32,7 +32,7 @@ $effect(() => {
 </script>
 
 {#if history.length > 0}
-  <datalist id="formula">
+  <datalist id="formula-history">
     {#each history as fml}
       <option value={fml}></option>
     {/each}
@@ -41,6 +41,7 @@ $effect(() => {
 
 <input
   id="formula"
+  list="formula-history"
   class={["rounded border border-foreground ring-0 focus:outline-none focus:ring-0 p-2 w-full", error && "border-primary"]}
   type="text"
   placeholder="Enter modal formula"
diff --git a/apps/web/src/routes/kripke/components/game.svelte b/apps/web/src/routes/kripke/components/game.svelte
index 75311c2..a6fd4e2 100644
--- a/apps/web/src/routes/kripke/components/game.svelte
+++ b/apps/web/src/routes/kripke/components/game.svelte
@@ -10,11 +10,13 @@ import {
   isomorphic,
   latexSymbols,
   prettyPrint,
+  unicodeSymbols,
 } from "@cannorin/kripke";
 import LuCheck from "lucide-svelte/icons/check";
 import LuHeart from "lucide-svelte/icons/heart";
 import LuHeartCrack from "lucide-svelte/icons/heart-crack";
 import LuX from "lucide-svelte/icons/x";
+import { formulaHistory } from "../lib/store";
 import FormulaInput from "./formula-input.svelte";
 import FrameInput from "./frame-input.svelte";
 
@@ -91,6 +93,9 @@ let canCheck = $derived.by(() => {
 async function check() {
   if (!canCheck || !formula) return;
   const valid = await checkImpl(formula);
+  formulaHistory.update((h) =>
+    formula ? h.add(prettyPrint(formula, { symbols: unicodeSymbols })) : h,
+  );
   moves.push({ type: "check", formulaStr, valid });
   moves = [...moves];
   formula = undefined;