diff --git a/common-lean/.gitignore b/common-lean/.gitignore
new file mode 100644
index 0000000..bfb30ec
--- /dev/null
+++ b/common-lean/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/common-lean/Common.lean b/common-lean/Common.lean
new file mode 100644
index 0000000..fb57002
--- /dev/null
+++ b/common-lean/Common.lean
@@ -0,0 +1,3 @@
+import Common.Lang
+import Common.Instances
+import Common.Demo
diff --git a/common-lean/Common/Demo.lean b/common-lean/Common/Demo.lean
new file mode 100644
index 0000000..d2e21f2
--- /dev/null
+++ b/common-lean/Common/Demo.lean
@@ -0,0 +1,56 @@
+import Common.Instances
+
+namespace Common.Demo
+
+open Common
+
+/-! # Cross-language abstraction demonstration.
+
+The same generic theorem `BigStepLang.unique_value` is here applied
+to TGC and TOC. The `SmallStepLang.step_deterministic` is applied
+to TSM. One abstract definition, multiple concrete payoffs. -/
+
+/-! ## Generic theorem statement (in `Common.Lang`):
+
+  `BigStepLang.unique_value : Eval s t v₁ s₁ → Eval s t v₂ s₂ → v₁ = v₂`
+
+Below are direct applications. -/
+
+/-! ### TGC (golang-lean) — the `Heap × Env`-stateful instance. -/
+
+example
+    (h : GolangLean.Core.Heap) (env : GolangLean.Core.Env)
+    (t : GolangLean.Core.Term)
+    (v₁ v₂ : GolangLean.Core.Value) (h₁ h₂ : GolangLean.Core.Heap)
+    (D₁ : GolangLean.Core.BigStep h env t v₁ h₁)
+    (D₂ : GolangLean.Core.BigStep h env t v₂ h₂) :
+    v₁ = v₂ := by
+  -- Package the existing TGC theorem as a Common.BigStepLang application:
+  exact BigStepLang.unique_value
+    (L := TGCLang) (s := (h, env)) (s₁ := (h₁, env)) (s₂ := (h₂, env))
+    ⟨D₁, rfl⟩ ⟨D₂, rfl⟩
+
+/-! ### TOC (octive-lean) — the env-mutating instance. -/
+
+example
+    (env : OctiveLean.Core.Env)
+    (t : OctiveLean.Core.Term)
+    (v₁ v₂ : OctiveLean.Core.Value) (env₁ env₂ : OctiveLean.Core.Env)
+    (D₁ : OctiveLean.Core.BigStep env t v₁ env₁)
+    (D₂ : OctiveLean.Core.BigStep env t v₂ env₂) :
+    v₁ = v₂ :=
+  BigStepLang.unique_value (L := TOCLang) D₁ D₂
+
+/-! ### TSM (tsm-lean) — the small-step instance. -/
+
+example
+    (s s₁ s₂ : TsmLean.Core.State)
+    (h₁ : TsmLean.Core.step s = some s₁) (h₂ : TsmLean.Core.step s = some s₂) :
+    s₁ = s₂ :=
+  SmallStepLang.step_deterministic (L := TSMLang) h₁ h₂
+
+/-! ## Observation: with three instances now exhibiting `BigStepLang`/
+`SmallStepLang`, any new theorem stated abstractly applies to all
+of them. The factoring is real. -/
+
+end Common.Demo
diff --git a/common-lean/Common/Instances.lean b/common-lean/Common/Instances.lean
new file mode 100644
index 0000000..5ad11f6
--- /dev/null
+++ b/common-lean/Common/Instances.lean
@@ -0,0 +1,46 @@
+import Common.Lang
+import GolangLean.Core.Determinism
+import OctiveLean.Core.Determinism
+import TsmLean.Core.Determinism
+
+namespace Common
+
+/-! # Instances — TGC, TOC, TSM as `Common` languages.
+
+Each kernel's existing types, semantics, and determinism theorem
+package as a typeclass instance. The shared abstractions in
+`Common.Lang` then apply uniformly. -/
+
+/-! ## TGC (golang-lean) — big-step over `Heap × Env`. -/
+
+instance TGCLang : BigStepLang where
+  Term  := GolangLean.Core.Term
+  Value := GolangLean.Core.Value
+  State := GolangLean.Core.Heap × GolangLean.Core.Env
+  Eval  := fun (he : GolangLean.Core.Heap × GolangLean.Core.Env)
+               (t  : GolangLean.Core.Term)
+               (v  : GolangLean.Core.Value)
+               (he' : GolangLean.Core.Heap × GolangLean.Core.Env) =>
+    GolangLean.Core.BigStep he.1 he.2 t v he'.1 ∧ he.2 = he'.2
+  deterministic := by
+    rintro ⟨h, env⟩ t v₁ v₂ ⟨h₁, env₁⟩ ⟨h₂, env₂⟩ ⟨D₁, henv₁⟩ ⟨D₂, henv₂⟩
+    have ⟨hv, hh⟩ := GolangLean.Core.BigStep.deterministic D₁ D₂
+    subst henv₁; subst henv₂; subst hh
+    exact ⟨hv, rfl⟩
+
+/-! ## TOC (octive-lean) — big-step over `Env`. -/
+
+instance TOCLang : BigStepLang where
+  Term  := OctiveLean.Core.Term
+  Value := OctiveLean.Core.Value
+  State := OctiveLean.Core.Env
+  Eval  := OctiveLean.Core.BigStep
+  deterministic := fun D₁ D₂ => OctiveLean.Core.BigStep.deterministic D₁ D₂
+
+/-! ## TSM (tsm-lean) — small-step over `State`. -/
+
+instance TSMLang : SmallStepLang where
+  State := TsmLean.Core.State
+  step  := TsmLean.Core.step
+
+end Common
diff --git a/common-lean/Common/Lang.lean b/common-lean/Common/Lang.lean
new file mode 100644
index 0000000..7856ec9
--- /dev/null
+++ b/common-lean/Common/Lang.lean
@@ -0,0 +1,97 @@
+/-!
+# Common.Lang — cross-language abstraction.
+
+A `BigStepLang` is a programming-language fragment with:
+  * a syntactic class of terms,
+  * a class of values,
+  * a state type carrying everything else (env, heap, etc.),
+  * a big-step relation `Eval : State → Term → Value → State → Prop`
+    saying "starting in state `s`, evaluating term `t` produces value
+    `v` and state `s'`",
+  * a determinism property (the relation is functional in `(v, s')`).
+
+This generalises TGC's `BigStep : Heap → Env → Term → Value → Heap`
+(with State := Heap × Env) and TOC's `BigStep : Env → Term → Value →
+Env` (with State := Env). TSM uses small-step semantics and fits a
+different class — see `SmallStepLang`.
+
+The point of the abstraction: theorems about *any* deterministic
+big-step language are stated and proved once, and apply to all
+instances. -/
+
+namespace Common
+
+class BigStepLang where
+  Term  : Type
+  Value : Type
+  State : Type
+  Eval  : State → Term → Value → State → Prop
+  deterministic : ∀ {s : State} {t : Term} {v₁ v₂ : Value} {s₁ s₂ : State},
+    Eval s t v₁ s₁ → Eval s t v₂ s₂ → v₁ = v₂ ∧ s₁ = s₂
+
+namespace BigStepLang
+
+variable [L : BigStepLang]
+
+/-- Result of an evaluation, when it exists, is unique. -/
+theorem unique_value
+    {s : L.State} {t : L.Term} {v₁ v₂ : L.Value} {s₁ s₂ : L.State}
+    (h₁ : L.Eval s t v₁ s₁) (h₂ : L.Eval s t v₂ s₂) :
+    v₁ = v₂ :=
+  (L.deterministic h₁ h₂).1
+
+theorem unique_state
+    {s : L.State} {t : L.Term} {v₁ v₂ : L.Value} {s₁ s₂ : L.State}
+    (h₁ : L.Eval s t v₁ s₁) (h₂ : L.Eval s t v₂ s₂) :
+    s₁ = s₂ :=
+  (L.deterministic h₁ h₂).2
+
+end BigStepLang
+
+/-! ## SmallStepLang — small-step semantics (e.g., TSM).
+
+A `SmallStepLang` is structurally simpler: a state type and a step
+function. Determinism is automatic since `step` is a function. -/
+
+class SmallStepLang where
+  State : Type
+  step  : State → Option State
+
+namespace SmallStepLang
+
+variable [L : SmallStepLang]
+
+/-- Reflexive-transitive closure of `step`. -/
+inductive MultiStep : L.State → L.State → Prop where
+  | refl (s : L.State) : MultiStep s s
+  | cons {s s' s'' : L.State}
+         (h₁ : L.step s = some s') (h₂ : MultiStep s' s'') :
+      MultiStep s s''
+
+/-- Single-step is functional. -/
+theorem step_deterministic {s s₁ s₂ : L.State}
+    (h₁ : L.step s = some s₁) (h₂ : L.step s = some s₂) :
+    s₁ = s₂ := by
+  rw [h₁] at h₂; exact Option.some.inj h₂
+
+end SmallStepLang
+
+/-! ## Compilation correctness — the substrate-projection theorem.
+
+If `Source` is a `BigStepLang`, `Target` is either kind, and `compile`
+maps source specs to target specs preserving evaluation, then the
+compilation pipeline inherits determinism.
+
+This is the categorical kernel of CompCert-style theorems. -/
+
+structure CompileCorrect
+    (Source : BigStepLang)
+    (Target : Type) (TargetEval : Target → Source.Value → Prop)
+    (compile : Source.Term → Target) where
+  /-- Compilation preserves evaluation: source `Eval` implies target
+      `TargetEval` produces the same value. -/
+  preservation :
+    ∀ {s : Source.State} {t : Source.Term} {v : Source.Value} {s' : Source.State},
+      Source.Eval s t v s' → TargetEval (compile t) v
+
+end Common
diff --git a/common-lean/lake-manifest.json b/common-lean/lake-manifest.json
new file mode 100644
index 0000000..119d0fa
--- /dev/null
+++ b/common-lean/lake-manifest.json
@@ -0,0 +1,37 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"type": "path",
+   "scope": "",
+   "name": "«tsm-lean»",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../tsm-lean",
+   "configFile": "lakefile.toml"},
+  {"type": "path",
+   "scope": "",
+   "name": "«octive-lean»",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../octive-lean",
+   "configFile": "lakefile.toml"},
+  {"type": "path",
+   "scope": "",
+   "name": "«golang-lean»",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../golang-lean",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.98",
+   "inherited": true,
+   "configFile": "lakefile.lean"}],
+ "name": "«common-lean»",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/common-lean/lakefile.toml b/common-lean/lakefile.toml
new file mode 100644
index 0000000..b0b972a
--- /dev/null
+++ b/common-lean/lakefile.toml
@@ -0,0 +1,18 @@
+name = "common-lean"
+version = "0.1.0"
+defaultTargets = ["Common"]
+
+[[require]]
+name = "golang-lean"
+path = "../golang-lean"
+
+[[require]]
+name = "octive-lean"
+path = "../octive-lean"
+
+[[require]]
+name = "tsm-lean"
+path = "../tsm-lean"
+
+[[lean_lib]]
+name = "Common"
diff --git a/common-lean/lean-toolchain b/common-lean/lean-toolchain
new file mode 100644
index 0000000..6c7e31f
--- /dev/null
+++ b/common-lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.30.0-rc2