diff --git a/EvaluationHarness/.gitignore b/EvaluationHarness/.gitignore
new file mode 100644
index 0000000000..bfb30ec8c7
--- /dev/null
+++ b/EvaluationHarness/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/EvaluationHarness/EvaluationHarness.lean b/EvaluationHarness/EvaluationHarness.lean
new file mode 100644
index 0000000000..abb0242cd4
--- /dev/null
+++ b/EvaluationHarness/EvaluationHarness.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `EvaluationHarness` library.
+-- Import modules here that should be built as part of the library.
+import EvaluationHarness.Basic
diff --git a/EvaluationHarness/EvaluationHarness/Basic.lean b/EvaluationHarness/EvaluationHarness/Basic.lean
new file mode 100644
index 0000000000..d65413ec5b
--- /dev/null
+++ b/EvaluationHarness/EvaluationHarness/Basic.lean
@@ -0,0 +1,196 @@
+import Lean
+
+import EvaluationHarness.Options
+
+/-!
+# Evaluation Harness
+
+This file defines the `#evaluation in ...` command wrapper, for easier evaluation.
+-/
+namespace EvaluationHarness
+
+open Lean Meta Elab Command
+
+/--
+`SimpleMessage` contains the subset of fields from `SerialMessage` that we
+wish to include in the logged output.
+-/
+protected structure SimpleMessage where
+  severity: MessageSeverity
+  data: String
+  caption: String
+  pos: Position
+deriving ToJson, FromJson
+
+protected structure Messages where
+  messages : List SerialMessage
+
+open EvaluationHarness (Messages SimpleMessage)
+
+/-! ## Message Collection -/
+
+/--
+Given a monadic action `cmd : CommandElabM Unit`, run the action, collect all
+messages (trace, info, warning and error messages) that the action logged, and
+return those. The collected messages are *not* left in the environment.
+-/
+protected def collectMessages (runCmd : CommandElabM α) : CommandElabM (α × Messages) := do
+  -- NOTE: the following is largely copied from the `#guard_msgs in` command,
+  --       with some slight adaptations
+
+  let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
+  -- do not forward snapshot as we don't want messages assigned to it to leak outside
+  let ret ← withReader ({ · with snap? := none }) runCmd
+  -- collect sync and async messages
+  let msgs := (← get).messages ++
+    (← get).snapshotTasks.foldl (· ++ ·.get.getAll.foldl (· ++ ·.diagnostics.msgLog) default) {}
+  -- clear async messages as we don't want them to leak outside, and
+  -- reset messages to initial state
+  modify ({ · with
+    snapshotTasks := #[]
+    messages := initMsgs
+  })
+  let messages ← msgs.toList
+    |>.filter (!·.isSilent)
+    |>.mapM (·.serialize)
+  return ⟨ret, { messages }⟩
+open EvaluationHarness (collectMessages)
+
+variable {m} [Monad m] [MonadOptions m] in
+def Messages.toSimple (self : Messages) : m (Option <| List SimpleMessage) := do
+  if (← getBoolOption `evaluation.includeMessages true) then
+    let includePosition ← getBoolOption `evaluation.includePosition true
+    some <$> self.messages.mapM fun m =>
+      return { m with
+        pos := if includePosition then m.pos else ⟨0, 0⟩
+      }
+  else
+    return none
+
+/-! ## EvaluationConfig -/
+
+structure EvaluationConfig where
+  strategy: Option String := none
+deriving Inhabited
+
+syntax evalConfigElem :=
+  ("strategy" " := " str)
+syntax evalConfig := "(" evalConfigElem,* ")"
+
+def parseEvaluationConfig (cfgElems : TSyntax ``evalConfig) : EvaluationConfig := Id.run <| do
+  let mut cfg := { }
+  let `(evalConfig| ( $cfgElems,* ) ) := cfgElems
+    | return cfg
+  for cfgElem in cfgElems.getElems do
+    cfg := match cfgElem with
+    | `(evalConfigElem| strategy := $s) =>
+        { cfg with strategy := some s.getString }
+    | _ =>
+        panic! "Unknown configuration option: {elem}"
+
+  return cfg
+
+
+/-! ## EvaluationInfo -/
+
+structure EvaluationInfo where
+  filename: String
+  /-- The line number on which `#evaluation in cmd` occurred. -/
+  line: Nat
+  /--
+  The collected messages generated by command `cmd`, or
+  `none` when the `evaluation.includeMessages` option is set to `false`.
+  -/
+  messages: Option (List SimpleMessage)
+  /--
+  Whether any errors were raised by `cmd`.
+
+  NOTE: this is reported regardless of the `includeMessages` option.
+  -/
+  hasErrors: Bool
+  /--
+  The time elapsed while elaborating `cmd`, or `none` when the
+  `evaluation.includeWalltime` option is set to `false` (which is the default).
+  -/
+  wallTime : Option Float
+  -- TODO: `data` field for more structured data reporting
+  /--
+  The name of the elaborated definition/theorem, or `none` if the command
+  was neither definition nor theorem.
+  -/
+  name : Option String
+  /--
+  An optional user-defined string that can be embedded in the output,
+  see `EvaluationConfig` for details.
+  -/
+  strategy : Option String
+deriving ToJson, FromJson
+
+open Lean.Parser.Command in
+/--
+If `cmd` is a `def` or `theorem`, return the name of the defininition/theorem.
+-/
+def getDefLikeName? (cmd : TSyntax `command) : Option String :=
+  let raw := cmd.raw
+  let kind := raw.getKind
+  if kind == ``declaration then
+    let name := raw[1]![1]![0]!.getId
+    some <| name.eraseMacroScopes.toString
+  else
+    none
+
+/--
+Run `cmd` and return the elapsed wall-time, or run the command but return `none`
+when the `evaluation.includeWalltime` option is set to `false` (which is the
+default).
+-/
+def measureWallTime (cmd : CommandElabM Unit) : CommandElabM (Option Float) := do
+  if (← getBoolOption `evaluation.includeWallTime false) then
+    let t1 ← IO.monoNanosNow
+    cmd
+    let t2 ← IO.monoNanosNow
+    return some (deltaInMs t2 t1)
+  else
+    cmd
+    return none
+where
+  deltaInMs (now past : Nat) : Float :=
+    (Float.ofNat <| now - past) / 1000000.0
+
+def evalEvaluation (cmd : TSyntax `command) (config : EvaluationConfig) : CommandElabM Unit := do
+  let (wallTime, msgs) ← collectMessages <| measureWallTime <| do
+    elabCommand cmd
+  let info : EvaluationInfo := {
+    filename := ← getFileName
+    line :=← getRefLine
+    messages := ← msgs.toSimple
+    hasErrors := msgs.messages.any (·.severity == .error)
+    wallTime
+    name := getDefLikeName? cmd
+    strategy := config.strategy
+  }
+  let info := s!"{toJson info}"
+  if (← getBoolOption `evaluation.outputAsLog) then
+    logInfo info
+  else
+    IO.println info
+where
+  getRefLine {m} [Monad m] [MonadOptions m] [MonadLog m] : m Nat := do
+    if (← getBoolOption `evaluation.includePosition true) then
+      return (← getRefPosition).line
+    else
+      return 0
+
+/--
+`#evalation in cmd` captures the messages generated by the command `cmd`, and
+serializes them into a single json object, together with some extra metadata
+such as the name of the current file.
+
+See `EvluationConfig` for details on extra configuration options.
+-/
+syntax "#evaluation" (evalConfig)? "in" command : command
+elab_rules : command
+| `(#evaluation in $cmd:command) => evalEvaluation cmd { }
+| `(#evaluation $cfg in $cmd:command) => do
+    let cfg := parseEvaluationConfig cfg
+    evalEvaluation cmd cfg
diff --git a/EvaluationHarness/EvaluationHarness/Options.lean b/EvaluationHarness/EvaluationHarness/Options.lean
new file mode 100644
index 0000000000..ef4fb3991b
--- /dev/null
+++ b/EvaluationHarness/EvaluationHarness/Options.lean
@@ -0,0 +1,34 @@
+import Lean
+
+/-!
+# Evaluation Harness Options
+This file defines various options which can be used to influence the behaviour
+of `#evaluation in cmd`.
+-/
+namespace EvaluationHarness
+open Lean
+
+initialize
+  registerOption `evaluation.includeWallTime {
+    defValue := false
+    descr := "Whether to include elapsed wall-time in the output of `#evaluation in cmd`"
+  }
+  registerOption `evaluation.includeMessages {
+    defValue := true
+    descr := "Whether to include a log of all messages in the output of `#evaluation in cmd`.\
+      When set to false, messages are still captured, but then they are discarded \
+      instead of incorporated into the output."
+  }
+
+  registerOption `evaluation.outputAsLog {
+    defValue := false
+    descr := "When set, output is emitted via `logInfo`, rather than `IO.println`"
+  }
+  registerOption `evaluation.includePosition {
+    defValue := true
+    descr := "Whether to include line/column information in the output. \
+      When set to false, all lines and columns are reported as 0. \
+      \n\n\
+      Can be particularly useful to disable in tests, to make the output less
+      brittle to changes in the overal file."
+  }
diff --git a/EvaluationHarness/EvaluationHarness/Tests/Basic.lean b/EvaluationHarness/EvaluationHarness/Tests/Basic.lean
new file mode 100644
index 0000000000..6bcd781cb6
--- /dev/null
+++ b/EvaluationHarness/EvaluationHarness/Tests/Basic.lean
@@ -0,0 +1,101 @@
+import EvaluationHarness.Basic
+
+namespace EvaluationHarness.Tests
+
+/-! ## getDefLikeName -/
+
+/-- info: some "foo" -/
+#guard_msgs in #eval do
+  let cmd ← `(command| theorem foo : False := sorry)
+  return getDefLikeName? cmd
+
+/-- info: some "foo.bar" -/
+#guard_msgs in #eval do
+  let cmd ← `(command| theorem foo.bar : False := sorry)
+  return getDefLikeName? cmd
+
+/-- info: some "baz" -/
+#guard_msgs in #eval do
+  let cmd ← `(command| def baz : False := sorry)
+  return getDefLikeName? cmd
+
+/-- info: some "privateBaz" -/
+#guard_msgs in #eval do
+  let cmd ← `(command| private def privateBaz : False := sorry)
+  return getDefLikeName? cmd
+
+/-- info: some "protBaz" -/
+#guard_msgs in #eval do
+  let cmd ← `(command| protected def protBaz : False := sorry)
+  return getDefLikeName? cmd
+
+/-! ## `#evaluation`-/
+set_option evaluation.outputAsLog true
+set_option evaluation.includePosition false
+
+/--
+info: {"wallTime": null,
+ "strategy": null,
+ "name": "foo",
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 0, "column": 0},
+   "data": "declaration uses 'sorry'",
+   "caption": ""}],
+ "line": 0,
+ "hasErrors": false,
+ "filename":
+ "/home/alex/Workspace/PhD/lean-mlir-alt/EvaluationHarness/EvaluationHarness/Tests/Basic.lean"}
+-/
+#guard_msgs in #evaluation in
+  def foo : False := sorry
+
+/--
+info: {"wallTime": null,
+ "strategy": "barStrat",
+ "name": "bar",
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 0, "column": 0},
+   "data": "declaration uses 'sorry'",
+   "caption": ""}],
+ "line": 0,
+ "hasErrors": false,
+ "filename":
+ "/home/alex/Workspace/PhD/lean-mlir-alt/EvaluationHarness/EvaluationHarness/Tests/Basic.lean"}
+-/
+#guard_msgs in #evaluation (strategy := "barStrat") in
+  def bar : False := sorry
+
+/--
+info: {"wallTime": null,
+ "strategy": null,
+ "name": "shouldError",
+ "messages":
+ [{"severity": "error",
+   "pos": {"line": 0, "column": 0},
+   "data": "Failed: `fail` tactic was invoked\n⊢ False",
+   "caption": ""}],
+ "line": 0,
+ "hasErrors": true,
+ "filename":
+ "/home/alex/Workspace/PhD/lean-mlir-alt/EvaluationHarness/EvaluationHarness/Tests/Basic.lean"}
+-/
+#guard_msgs in #evaluation in
+  def shouldError : False := by
+    fail
+
+set_option evaluation.includeMessages false in
+/--
+info: {"wallTime": null,
+ "strategy": null,
+ "name": "shouldErrorWithoutMsg",
+ "messages": null,
+ "line": 0,
+ "hasErrors": true,
+ "filename":
+ "/home/alex/Workspace/PhD/lean-mlir-alt/EvaluationHarness/EvaluationHarness/Tests/Basic.lean"}
+-/
+#guard_msgs in #evaluation in
+  def shouldErrorWithoutMsg : False := by
+    fail
diff --git a/EvaluationHarness/EvaluationHarness/Tests/ExampleFile.lean b/EvaluationHarness/EvaluationHarness/Tests/ExampleFile.lean
new file mode 100644
index 0000000000..5fe31a5396
--- /dev/null
+++ b/EvaluationHarness/EvaluationHarness/Tests/ExampleFile.lean
@@ -0,0 +1,19 @@
+import EvaluationHarness.Basic
+import Std.Tactic.BVDecide
+
+open BitVec
+
+#evaluation in
+theorem test_with_1_thm.extracted_1._1 : ∀ (x : BitVec 32),
+    ¬x ≥ ↑32 → 1#32 <<< x &&& 1#32 = zeroExtend 32 (ofBool (x == 0#32)) := by
+  bv_decide
+
+#evaluation in
+theorem test_with_3_thm.extracted_1._1 : ∀ (x : BitVec 32),
+    ¬x ≥ ↑32 → 3#32 <<< x &&& 1#32 = zeroExtend 32 (ofBool (x == 0#32)) := by
+  bv_decide
+
+#evaluation in
+theorem test_with_5_thm.extracted_1._1 : ∀ (x : BitVec 32),
+    ¬x ≥ ↑32 → 5#32 <<< x &&& 1#32 = zeroExtend 32 (ofBool (x == 0#32)) := by
+  fail
diff --git a/EvaluationHarness/Main.lean b/EvaluationHarness/Main.lean
new file mode 100644
index 0000000000..d4cd5f99e3
--- /dev/null
+++ b/EvaluationHarness/Main.lean
@@ -0,0 +1,4 @@
+import EvaluationHarness
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/EvaluationHarness/README.md b/EvaluationHarness/README.md
new file mode 100644
index 0000000000..9a614dbe70
--- /dev/null
+++ b/EvaluationHarness/README.md
@@ -0,0 +1 @@
+# evaluation-harness
\ No newline at end of file
diff --git a/EvaluationHarness/lakefile.toml b/EvaluationHarness/lakefile.toml
new file mode 100644
index 0000000000..8e761d908b
--- /dev/null
+++ b/EvaluationHarness/lakefile.toml
@@ -0,0 +1,6 @@
+name = "EvaluationHarness"
+version = "0.1.0"
+defaultTargets = ["EvaluationHarness"]
+
+[[lean_lib]]
+name = "EvaluationHarness"
diff --git a/EvaluationHarness/lean-toolchain b/EvaluationHarness/lean-toolchain
new file mode 120000
index 0000000000..6f68e61b37
--- /dev/null
+++ b/EvaluationHarness/lean-toolchain
@@ -0,0 +1 @@
+../lean-toolchain
\ No newline at end of file
diff --git a/SSA/Projects/InstCombine/tests/proofs/gand_proof.lean b/SSA/Projects/InstCombine/tests/proofs/gand_proof.lean
index 86d369e89c..9822a0a3f2 100644
--- a/SSA/Projects/InstCombine/tests/proofs/gand_proof.lean
+++ b/SSA/Projects/InstCombine/tests/proofs/gand_proof.lean
@@ -1,5 +1,67 @@
 
-import SSA.Projects.InstCombine.TacticAuto
+
+import SSA.Projects.InstCombine.Tactic.SimpLLVM
+import SSA.Projects.InstCombine.LLVM.Semantics
+
+import SSA.Core.Tactic.ExtractGoals
+
+open BitVec
+open LLVM
+
+set_option linter.unusedTactic false
+set_option linter.unreachableTactic false
+set_option maxHeartbeats 5000000
+set_option maxRecDepth 1000000
+set_option Elab.async false
+
+section gand_proof
+theorem test_with_1_thm (e : IntW 32) :
+  LLVM.and (shl (const? 32 1) e) (const? 32 1) ⊑ zext 32 (icmp IntPred.eq e (const? 32 0)) := by
+    simp_alive_undef
+    simp_alive_ops
+    simp_alive_case_bash
+    simp_alive_split
+    extract_goals
+    all_goals sorry
+
+
+theorem test_with_3_thm (e : IntW 32) :
+  LLVM.and (shl (const? 32 3) e) (const? 32 1) ⊑ zext 32 (icmp IntPred.eq e (const? 32 0)) := by
+    simp_alive_undef
+    simp_alive_ops
+    simp_alive_case_bash
+    simp_alive_split
+    extract_goals
+    all_goals sorry
+
+
+theorem test_with_5_thm (e : IntW 32) :
+  LLVM.and (shl (const? 32 5) e) (const? 32 1) ⊑ zext 32 (icmp IntPred.eq e (const? 32 0)) := by
+    simp_alive_undef
+    simp_alive_ops
+    simp_alive_case_bash
+    simp_alive_split
+    extract_goals
+    all_goals sorry
+
+
+theorem test_with_neg_5_thm (e : IntW 32) :
+  LLVM.and (shl (const? 32 (-5)) e) (const? 32 1) ⊑ zext 32 (icmp IntPred.eq e (const? 32 0)) := by
+    simp_alive_undef
+    simp_alive_ops
+    simp_alive_case_bash
+    simp_alive_split
+    extract_goals
+    all_goals sorry
+
+
+theorem test_with_even_thm (e : IntW 32) : LLVM.and (shl (const? 32 4) e) (const? 32 1) ⊑ const? 32 0 := by
+    simp_alive_undef
+    simp_alive_ops
+    simp_alive_case_bash
+    simp_alive_split
+    extract_goals
+    all_goals sorry
 import SSA.Projects.InstCombine.LLVM.Semantics
 open BitVec
 open LLVM
diff --git a/lake-manifest.json b/lake-manifest.json
index dd9f56bbe9..6b03b4978a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -31,6 +31,13 @@
    "inputRev": "nightly-testing-2025-08-11",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "EvaluationHarness",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "EvaluationHarness",
+   "configFile": "lakefile.toml"},
   {"type": "path",
    "scope": "",
    "name": "Blase",
diff --git a/lakefile.toml b/lakefile.toml
index 4f2bdf2131..bbd68e2789 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -14,6 +14,10 @@ name = "Blase"
 path = "Blase"
 rev = "main"
 
+[[require]]
+name = "EvaluationHarness"
+path = "EvaluationHarness"
+
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4-nightly-testing"