diff --git a/README.md b/README.md
index cc3aacd..bdc771d 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ I'd like to build the following:
 
 - [X] parsing with parsec
   - need to harden tests a bit more but existing tests pass
-- [ ] alpha/beta reduction to beta normal
+- [X] alpha/beta reduction to beta normal
 - [ ] substitutions for known abstractions (numbers can be written and are displayed as numbers rather than lambda terms)
 - [ ] persisted variables
 - [ ] display all steps in alpha/beta reductions until beta normal form is reached
diff --git a/test/EvaluationSpec.hs b/test/EvaluationSpec.hs
index af0549e..117297f 100644
--- a/test/EvaluationSpec.hs
+++ b/test/EvaluationSpec.hs
@@ -1,7 +1,7 @@
 module EvaluationSpec (spec) where
 
 import Data.Set (Set, empty, fromList)
-import Evaluation (alphaEquiv, beta, bind, freeIn, freeVars, freshName, subst)
+import Evaluation (alphaEquiv, beta, bind, freeIn, freeVars, freshName, run, subst)
 import Parser (Expr (Abstraction, Application, Variable), parse)
 import Test.Hspec
 
@@ -261,9 +261,73 @@ spec = do
       -- The inner λx re-binds x, so the outer x should not be substituted into it
       beta (Application (Abstraction "x" (Abstraction "x" (Variable "x"))) (Variable "y"))
         `shouldBe` Just (Abstraction "x" (Variable "x"))
+
+  describe "run" $ do
+    -- Normal forms: run should be a no-op
+    it "returns a bare variable unchanged" $
+      run (Variable "x") `shouldBe` Variable "x"
+    it "returns a bare abstraction unchanged" $
+      run absI `shouldBe` absI
+    it "returns a normal application (no redex) unchanged" $
+      run (Application (Variable "x") (Variable "y")) `shouldBe` Application (Variable "x") (Variable "y")
+    it "returns a complex beta-normal term unchanged" $
+      case parse "λa. λb. λc. a (b c)" of
+        Right expr -> run expr `shouldBe` expr
+        Left err -> expectationFailure err
+
+    -- Single-step reductions
+    it "reduces identity applied to a variable: (λi. i) y → y" $
+      run (Application absI (Variable "y")) `shouldBe` Variable "y"
+    it "reduces constant function: (λx. z) y → z" $
+      run (Application (Abstraction "x" (Variable "z")) (Variable "y")) `shouldBe` Variable "z"
+
+    -- Multi-step reductions
+    it "reduces two nested identity applications to normal form: (λi. i)((λi. i) y) → y" $
+      run (Application absI (Application absI (Variable "y"))) `shouldBe` Variable "y"
+    it "reduces self-application of identity: (λx. x x)(λi. i) → (λi. i)" $
+      run (Application selfApp absI) `shouldBeAlphaEq` absI
+
+    -- Combinator reductions
+    it "fully reduces K combinator: K a b → a" $
+      run (Application (Application k (Variable "a")) (Variable "b")) `shouldBe` Variable "a"
+    it "reduces S K K to identity" $
+      run (Application (Application s k) k) `shouldBeAlphaEq` absI
+
+    -- Shadowing
+    it "does not substitute into a shadowed binder: (λx. λx. x) y → λx. x" $
+      run (Application (Abstraction "x" (Abstraction "x" (Variable "x"))) (Variable "y"))
+        `shouldBe` Abstraction "x" (Variable "x")
+
+    -- Capture-avoidance
+    it "avoids variable capture: (λx. λz. x) z does not reduce to identity" $
+      -- Naive substitution would yield λz. z (identity), capturing the free z.
+      -- Correct result renames the binder: λz'. z (a constant-z function).
+      run (Application (Abstraction "x" (Abstraction "z" (Variable "x"))) (Variable "z"))
+        `shouldBeAlphaEq'` Abstraction "z" (Variable "z")
+
+    -- Idempotency: run (run e) == run e
+    it "run is idempotent on a normal form" $
+      run (run (Variable "x")) `shouldBe` run (Variable "x")
+    it "run is idempotent on a reducible expression" $
+      run (run (Application absI (Variable "y"))) `shouldBe` run (Application absI (Variable "y"))
+
   where
+    -- | Assert that two expressions are alpha-equivalent.
+    shouldBeAlphaEq :: Expr -> Expr -> Expectation
+    shouldBeAlphaEq actual expected =
+      alphaEquiv actual expected
+        `shouldBe` True
+    -- | Assert that two expressions are NOT alpha-equivalent.
+    shouldBeAlphaEq' :: Expr -> Expr -> Expectation
+    shouldBeAlphaEq' actual expected =
+      alphaEquiv actual expected
+        `shouldBe` False
     absWithZMaker z = Abstraction "x" (Application z (Variable "x"))
     absWithZ = absWithZMaker (Variable "z")
     absI    = Abstraction "i" (Variable "i")
     selfApp = Abstraction "x" (Application (Variable "x") (Variable "x"))
     omega   = Abstraction "x" (Application (Variable "x") (Variable "x"))
+    k       = Abstraction "x" (Abstraction "y" (Variable "x"))
+    s       = Abstraction "x" (Abstraction "y" (Abstraction "z"
+                (Application (Application (Variable "x") (Variable "z"))
+                             (Application (Variable "y") (Variable "z")))))