diff --git a/Taskfile.yml b/Taskfile.yml
new file mode 100644
index 0000000..1e81bfc
--- /dev/null
+++ b/Taskfile.yml
@@ -0,0 +1,16 @@
+version: "3"
+
+tasks:
+  deps:
+    desc: "Install Python packages and Lean toolchain"
+    cmds:
+      - pip install --upgrade pip
+      - pip install -r requirements.txt
+      - curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y
+      - echo "source $HOME/.elan/env" >> ~/.bashrc
+
+  test:
+    desc: "Run PyTest suite"
+    deps: [deps]
+    cmds:
+      - bash -c '. "$HOME/.elan/env" && export PYTHONPATH="$PWD" && pytest -q tests/'
diff --git a/tests/test_sanity_loss.py b/tests/test_sanity_loss.py
new file mode 100644
index 0000000..1d3cb6a
--- /dev/null
+++ b/tests/test_sanity_loss.py
@@ -0,0 +1,37 @@
+# tests/test_sanity_loss.py
+import torch
+import torch.nn as nn
+
+def test_dummy_loss_decreases():
+    """
+    Sanity-check that a mini training step actually lowers loss.
+    Uses a 2-layer MLP on random data so it runs in <2 s on CPU.
+    """
+    torch.manual_seed(0)
+
+    model = nn.Sequential(
+        nn.Linear(4, 8),
+        nn.ReLU(),
+        nn.Linear(8, 1)
+    )
+
+    x = torch.randn(32, 4)
+    y = torch.randn(32, 1)
+
+    criterion = nn.MSELoss()
+    optimizer = torch.optim.SGD(model.parameters(), lr=0.1)
+
+    # loss before training
+    loss_start = criterion(model(x), y).item()
+
+    # one quick training step
+    optimizer.zero_grad()
+    criterion(model(x), y).backward()
+    optimizer.step()
+
+    # loss after training
+    loss_end = criterion(model(x), y).item()
+
+    assert loss_end < loss_start, (
+        f"loss did not decrease: start={loss_start:.4f}, end={loss_end:.4f}"
+    )
\ No newline at end of file
diff --git a/tests/test_sanity_tactic.py b/tests/test_sanity_tactic.py
new file mode 100644
index 0000000..346df4f
--- /dev/null
+++ b/tests/test_sanity_tactic.py
@@ -0,0 +1,6 @@
+from tests.util_stub import suggest_tactics
+
+def test_tactic_generator_nonempty():
+    """Generator should emit at least one tactic string."""
+    tactics = suggest_tactics("⊢ 1 = 1")
+    assert tactics and any(t.strip() for t in tactics), "generator returned nothing"
diff --git a/tests/util_stub.py b/tests/util_stub.py
new file mode 100644
index 0000000..586f666
--- /dev/null
+++ b/tests/util_stub.py
@@ -0,0 +1,3 @@
+def suggest_tactics(state, top_k=3):
+    """Return a dummy tactic list (acts like a stand-in for the real generator)."""
+    return ["rfl"]      # works for the goal ⊢ 1 = 1