diff --git a/config.json b/config.json
index 0e40e01..432fed7 100644
--- a/config.json
+++ b/config.json
@@ -809,6 +809,14 @@
         "practices": [],
         "prerequisites": [],
         "difficulty": 9
+      },
+      {
+        "slug": "assemble",
+        "name": "assemble",
+        "uuid": "17337704-ef28-490b-bbdd-f8e3f51e326b",
+        "practices": [],
+        "prerequisites": [],
+        "difficulty": 10
       }
     ]
   },
diff --git a/exercises/practice/assemble/.docs/instructions.md b/exercises/practice/assemble/.docs/instructions.md
new file mode 100644
index 0000000..1b7760e
--- /dev/null
+++ b/exercises/practice/assemble/.docs/instructions.md
@@ -0,0 +1,141 @@
+# Instructions
+
+In this exercise, you will define the syntax and execution model for a small assembly-like language inspired by the `x86-64` assembly language.
+
+The goal is to formalize how code is written, parsed, and executed within a constrained environment.
+
+## Execution Model
+
+Your assembly code will be written inside a special construct:
+
+```lean
+let program := assemble!(
+    -- assembly code here
+)
+```
+
+This construct must produce a **program**, which simulates a function that executes the assembly code and returns a value.
+This program is then invoked using the following syntax, where `a`, `b`, `c`, etc. are arguments:
+
+```lean
+let result := program(a, b, c, ...)
+```
+
+All arguments and the return value are _64-bit signed integers_.
+A maximum of _6 arguments_ is allowed.
+
+## Registers
+
+The return value and all arguments are passed in **registers**.
+Your language must support the following registers:
+
+| register | role         |
+|----------|--------------|
+| `rdi`    | 1st argument |
+| `rsi`    | 2nd argument |
+| `rdx`    | 3rd argument |
+| `rcx`    | 4th argument |
+| `r8`     | 5th argument |
+| `r9`     | 6th argument |
+| `rax`    | return value |
+
+Registers start with a default value of `0`, unless they are used to pass arguments to the function.
+
+For example, in the following program, all registers have a value of `0` with the exception of `rdi`, which is initialized with `10`, and `rsi`. which is initialized with `-20`:
+
+```lean
+program(10, -20)
+```
+
+The return value of the program is always stored in `rax`.
+
+Note that register names are _case-insensitive_.
+This means that `rax`, `RAX` and `rAx` all refer to the same register.
+
+## Assembly code
+
+Each line in the assembly code can be of two forms:
+
+- **Labels** mark specific places of the program to be used by some instructions.
+- **Instructions** represent operations executed by the program.
+
+Unless modified by some instruction, the execution flow of the program proceeds linearly.
+This means that a previous line is fully executed before the line after it is executed.
+
+### Labels
+
+Labels have the following syntax:
+
+```lean
+<label>:
+```
+
+They do not alter the values of any register or have any effect to the program other than marking specific places of the code so they can be used by instructions.
+
+Note that labels are _case-sensitive_.
+This means that `Start`, `start` and `sTart` are all different labels.
+
+### Two-operand instructions
+
+Most instructions have the following syntax:
+
+```lean
+<opcode> <destination>, <source>
+```
+
+The `opcode` indicates the operation being executed, using the values of the `destination` and `source` operands.
+The result of the operation is stored in the `destination` operand.
+
+For example, the instruction `add` sums the values in the `destination` and the `source` operands and stores this result in the `destination` operand.
+
+The `destination` operand is _always_ a register, whereas the `source` operand may be a register or a literal number.
+
+This is a list of instructions your program must support:
+
+| opcode | operation performed                   |
+|--------|---------------------------------------|
+| `mov`  | destination := source                 |
+| `add`  | destination := destination + source   |
+| `sub`  | destination := destination - source   |
+| `mul`  | destination := destination * source   |
+| `div`  | destination := destination / source   |
+| `xor`  | destination := destination ^^^ source |
+| `and`  | destination := destination &&& source |
+| `or`   | destination := destination ||| source |
+| `shl`  | destination := destination <<< source |
+| `shr`  | destination := destination >>> source |
+
+Other than those, your program must support the two-operand `cmp` instruction.
+
+This instruction does not modify any register, but instead compares the `destination` and the `source` operands and sets an internal state of the program to one of three states:
+
+- _greater than_, if `destination` > `source`
+- _equal_, if `destination` == `source`
+- _lesser than_, if `destination` < `source`
+
+How you keep track internally of this state is up to you.
+
+### One-operand instructions
+
+There are some instructions that alter the flow of the program, transferring execution to another point of the code.
+They are called _jumping_ instructions.
+
+They all take just one operand, which is a label that indicates the target of the jump, i.e., the point of the code where execution will continue:
+
+```lean
+<opcode> <label>
+```
+
+The `jmp` instruction _always_ makes the jump to the target label.
+
+Other jumping instructions make the jump only if the internal state of the program is set to a specific value.
+This means they are usually preceded by a `cmp` instruction.
+
+Those are the jumping instructions your program must support:
+
+| instruction | operation performed                                |
+|-------------|----------------------------------------------------|
+| `jmp`       | unconditional jump. The jump is always performed |
+| `je`        | jumps if the internal state is _equal_             |
+| `jl`        | jumps if the internal state is _less than_         |
+| `jg`        | jumps if the internal state is _greater than_      |
diff --git a/exercises/practice/assemble/.meta/Example.lean b/exercises/practice/assemble/.meta/Example.lean
new file mode 100644
index 0000000..a98e0fb
--- /dev/null
+++ b/exercises/practice/assemble/.meta/Example.lean
@@ -0,0 +1,157 @@
+import Std.Data.HashMap
+
+open Lean Syntax Macro Std
+
+structure CPU where
+  regs : Vector Int64 10
+  deriving Repr
+
+structure Program where
+  labels : HashMap String Nat
+  ops    : Array (List String)
+
+private def getStr (id : TSyntax `ident) : String :=
+  id.getId.toString.toLower
+
+private def regIdx (reg : String) : Fin 10 :=
+  match reg with
+  | "rdi" => 0
+  | "rsi" => 1
+  | "rdx" => 2
+  | "rcx" => 3
+  | "r8"  => 4
+  | "r9"  => 5
+  | "r10" => 6
+  | "r11" => 7
+  | "rax" => 8
+  | "rflags" => 9
+  | _     => panic! "invalid register"
+
+private def getVal (cpu : CPU) (reg : String) : Int64 :=
+  match reg.toInt? with
+  | some n => n.toInt64
+  | none => cpu.regs[regIdx reg]!
+
+private def unFlag : Int64 := 1
+private def eqFlag : Int64 := (1 : Int64) <<< 6
+private def gtFlag : Int64 := (1 : Int64) <<< 5
+private def ltFlag : Int64 := (1 : Int64) <<< 4
+
+private def compareRegs (dest src : Int64) : Int64 := Id.run do
+  let mut acc : Int64 := 0
+  acc := acc ||| ((dest == src).toInt64 <<< 6)         -- equal
+  acc := acc ||| ((decide (dest > src)).toInt64 <<< 5) -- greater
+  acc := acc ||| ((decide (dest < src)).toInt64 <<< 4) -- lesser
+  return acc
+
+private def dispatchCondJmp (cpu : CPU) (dest : String) (labels : Std.HashMap String Nat) (flag : Int64) (RIP : Nat) : Nat :=
+  if flag == unFlag || getVal cpu "rflags" &&& flag != 0 then
+    if h₀: dest ∈ labels then
+      labels[dest] + 1
+    else panic! "Invalid label"
+  else RIP + 1
+
+declare_syntax_cat x86_dest
+syntax ident : x86_dest
+
+declare_syntax_cat x86_src
+syntax ident : x86_src
+syntax num   : x86_src
+syntax "-" num  : x86_src
+
+declare_syntax_cat x86_inst
+syntax ident x86_dest "," x86_src  : x86_inst
+syntax ident x86_dest : x86_inst
+syntax ident ":" : x86_inst
+
+syntax "assemble!(" (x86_inst)* ")" : term
+syntax term "(" (term),* ")" : term
+
+private def Program.evaluate (args : Array Int64) (program : Program) : Int64 := Id.run do
+  let regs := (Array.finRange 6).foldl (init := Vector.replicate 10 0) fun acc i =>
+    acc.set i (args[i]?.getD 0)
+
+  let mut acc : CPU := { regs }
+  let mut i := 0
+
+  while h: i < program.ops.size do
+    match program.ops[i] with
+    | [op, dest, src] =>
+      i := i + 1
+      let srcVal := getVal acc src
+      let destVal := getVal acc dest
+      match op with
+      | "mov"  => acc := { acc with regs := acc.regs.set (regIdx dest) srcVal }
+      | "add"  => acc := { acc with regs := acc.regs.set (regIdx dest) (destVal + srcVal) }
+      | "sub"  => acc := { acc with regs := acc.regs.set (regIdx dest) (destVal - srcVal) }
+      | "xor"  => acc := { acc with regs := acc.regs.set (regIdx dest) (destVal ^^^ srcVal) }
+      | "and"  => acc := { acc with regs := acc.regs.set (regIdx dest) (destVal &&& srcVal) }
+      | "or"   => acc := { acc with regs := acc.regs.set (regIdx dest) (destVal ||| srcVal) }
+      | "shl"  => acc := { acc with regs := acc.regs.set (regIdx dest) (destVal <<< srcVal) }
+      | "shr"  => acc := { acc with regs := acc.regs.set (regIdx dest) (destVal >>> srcVal) }
+      | "mul"  => acc := { acc with regs := acc.regs.set (regIdx dest) (destVal * srcVal) }
+      | "div"  => acc := { acc with regs := acc.regs.set (regIdx dest) (destVal / srcVal) }
+      | "cmp"  => acc := { acc with regs := acc.regs.set (regIdx "rflags") (compareRegs destVal srcVal) }
+      | _ => continue
+    | [op, dest] =>
+      match op with
+      | "jmp" => i := dispatchCondJmp acc dest program.labels unFlag i
+      | "je"  => i := dispatchCondJmp acc dest program.labels eqFlag i
+      | "jl"  => i := dispatchCondJmp acc dest program.labels ltFlag i
+      | "jg"  => i := dispatchCondJmp acc dest program.labels gtFlag i
+      | _     => i := i + 1
+    | _ => i := i + 1
+
+  return acc.regs.get $ regIdx "rax"
+
+macro_rules
+  | `(assemble!( $[$insts]* )) => do
+    let mut labelNames : Array (TSyntax `term) := #[]
+    let mut labelIndices : Array (TSyntax `term) := #[]
+    let mut ops   : Array (TSyntax `term) := #[]
+
+    for i in [:insts.size] do
+      match insts[i]! with
+      | `(x86_inst| $opId:ident $dest:x86_dest , $src:x86_src) =>
+        match dest with
+        | `(x86_dest| $destId:ident) =>
+          match src with
+          | `(x86_src| $srcId:ident) =>
+            let opStr   := mkStrLit $ getStr opId
+            let destStr := mkStrLit $ getStr destId
+            let srcStr  := mkStrLit $ getStr srcId
+            ops := ops.push (← `([$opStr, $destStr, $srcStr]))
+          | `(x86_src| $srcN:num) =>
+            let opStr   := mkStrLit $ getStr opId
+            let destStr := mkStrLit $ getStr destId
+            let srcStr := mkStrLit $ s!"{srcN.getNat}"
+            ops := ops.push (← `([$opStr, $destStr, $srcStr]))
+          | `(x86_src| -$srcN:num) =>
+            let opStr   := mkStrLit $ getStr opId
+            let destStr := mkStrLit $ getStr destId
+            let srcStr := mkStrLit $ s!"-{srcN.getNat}"
+            ops := ops.push (← `([$opStr, $destStr, $srcStr]))
+          | _ => throwUnsupported
+        | _ => throwUnsupported
+      | `(x86_inst| $opId:ident $dest:x86_dest) =>
+         match dest with
+        | `(x86_dest| $destId:ident) =>
+          let opStr   := mkStrLit $ getStr opId
+          let destStr := mkStrLit destId.getId.toString
+          ops := ops.push (← `([$opStr, $destStr]))
+        | _ => throwUnsupported
+      | `(x86_inst| $labelId:ident :) =>
+        labelNames := labelNames.push (mkStrLit labelId.getId.toString)
+        labelIndices := labelIndices.push (mkNumLit s!"{i}")
+        ops := ops.push (← `([]))
+      | _ => throwUnsupported
+
+    `(({
+        ops := #[$[$ops],*],
+        labels := HashMap.ofList [ $[ ($labelNames, $labelIndices) ],* ]
+      } : Program)
+    )
+  | `($program( $[$args],* )) => do
+    let args' ← args.mapM fun a => `(($a : Int64))
+    let result ← `(Program.evaluate #[$[$args'],*] $program)
+    `(($result))
diff --git a/exercises/practice/assemble/.meta/config.json b/exercises/practice/assemble/.meta/config.json
new file mode 100644
index 0000000..63d7022
--- /dev/null
+++ b/exercises/practice/assemble/.meta/config.json
@@ -0,0 +1,18 @@
+{
+  "authors": [
+    "oxe-i"
+  ],
+  "files": {
+    "solution": [
+      "Assemble.lean"
+    ],
+    "test": [
+      "AssembleTest.lean"
+    ],
+    "example": [
+      ".meta/Example.lean"
+    ]
+  },
+  "icon": "binary",
+  "blurb": "Define the syntax of a minimal x86-64–inspired assembly language"
+}
diff --git a/exercises/practice/assemble/.meta/extra.json b/exercises/practice/assemble/.meta/extra.json
new file mode 100644
index 0000000..e7fadeb
--- /dev/null
+++ b/exercises/practice/assemble/.meta/extra.json
@@ -0,0 +1,235 @@
+[
+  {
+    "description": "Copy a value",
+    "property": "assemble",
+    "input": {
+       "args": [10],
+       "code": [
+        "mov rax, rdi"
+       ]
+    },
+    "expected": {
+      "rax": 10
+    }
+  },
+  {
+    "description": "Sum and subtraction",
+    "property": "assemble",
+    "input": {
+       "args": [10, 20],
+       "code": [
+        "mov rax, rdi",
+        "add rax, rdi",
+        "sub rax, rsi"
+       ]
+    },
+    "expected": {
+      "rax": 0
+    }
+  },
+  {
+    "description": "Multiplication and division",
+    "property": "assemble",
+    "input": {
+      "args": [100, 5, 6],
+      "code": [
+        "mov rax, rdi",
+        "mul rax, rdx",
+        "div rax, rsi"
+      ]
+    },
+    "expected": {
+      "rax": 120
+    }
+  },
+  {
+    "description": "Bitwise operations",
+    "property": "assemble",
+    "input": {
+       "args": [49, 16, 1, 255],
+       "code": [
+        "or rax, rcx",
+        "and rax, rdi",
+        "xor rax, rsi",
+        "shr rax, rdx"
+       ]
+    },
+    "expected": {
+      "rax": 16
+    }
+  },
+  {
+    "description": "Skip instructions",
+    "property": "assemble",
+    "input": {
+       "args": [50000000000, -3000000000],
+       "code": [
+        "mov rax, rdi",
+        "jmp end_program",
+        "add rax, rsi",
+        "end_program:"
+       ]
+    },
+    "expected": {
+      "rax": 50000000000
+    }
+  },
+  {
+    "description": "Condition met",
+    "property": "assemble",
+    "input": {
+       "args": [40010, -40020],
+       "code": [
+        "mov rax, rdi",
+        "cmp rax, rsi",
+        "jg end_program",
+        "add rax, rsi",
+        "end_program:"
+       ]
+    },
+    "expected": {
+      "rax": 40010
+    }
+  },
+  {
+    "description": "Condition not met",
+    "property": "assemble",
+    "input": {
+       "args": [400, -600],
+       "code": [
+        "mov rax, rdi",
+        "cmp rax, rsi",
+        "jl end_program",
+        "add rax, rsi",
+        "end_program:"
+       ]
+    },
+    "expected": {
+      "rax": -200
+    }
+  },
+  {
+    "description": "Registers are case-insensitive",
+    "property": "assemble",
+    "input": {
+       "args": [4010, -3010],
+       "code": [
+        "mov RAX, rdi",
+        "SUB rax, Rsi"
+       ]
+    },
+    "expected": {
+      "rax": 7020
+    }
+  },
+  {
+    "description": "Labels are case-sensitive",
+    "property": "assemble",
+    "input": {
+       "args": [4010, -3010, 10],
+       "code": [
+        "mov rax, rdi",
+        "cmp rax, rsi",
+        "jg End_program",
+        "sub rax, rsi",
+        "End_program:",
+        "div rax, rdx",
+        "end_program:"
+       ]
+    },
+    "expected": {
+      "rax": 401
+    }
+  },
+  {
+    "description": "All registers are used",
+    "property": "assemble",
+    "input": {
+       "args": [4, -75590, -10, 890, 435, -235],
+       "code": [
+        "mov rax, r8",
+        "add rax, r9",
+        "mul rax, rdx",
+        "sub rax, rcx",
+        "and rax, rdi",
+        "or rax, rsi"
+       ]
+    },
+    "expected": {
+      "rax": -75586
+    }
+  },
+  {
+    "description": "Calculate the sum of the first 10 natural numbers",
+    "property": "assemble",
+    "input": {
+       "args": [10],
+       "code": [
+        "sum_first_N:",
+        "cmp rdi, 0",
+        "je base_case",
+        "add rax, rdi",
+        "sub rdi, 1",
+        "jmp sum_first_N",
+        "base_case:"
+       ]
+    },
+    "expected": {
+      "rax": 55
+    }
+  },
+  {
+    "description": "Count how many bits are set in 2000000000",
+    "property": "assemble",
+    "input": {
+       "args": [2000000000],
+       "code": [
+        "pop_count:",
+        "cmp rdi, 0",
+        "je base_case",
+        "add rax, 1",
+        "mov rdx, rdi",
+        "sub rdx, 1",
+        "and rdi, rdx",
+        "jmp pop_count",
+        "base_case:"
+       ]
+    },
+    "expected": {
+      "rax": 13
+    }
+  },
+  {
+    "description": "Count steps in the Collatz Conjecture starting with 1000000, -1 indicates error",
+    "property": "assemble",
+    "input": {
+       "args": [1000000],
+       "code": [
+        "steps:",
+        "cmp rdi, 1",
+        "jl error",
+        "je base_case",
+        "loop:",
+        "add rax, 1",
+        "mov rdx, rdi",
+        "and rdx, 1",
+        "cmp rdx, 0",
+        "je even",
+        "mul rdi, 3",
+        "add rdi, 1",
+        "jmp loop",
+        "even:",
+        "shr rdi, 1",
+        "cmp rdi, 1",
+        "je base_case",
+        "jmp loop",
+        "error:",
+        "mov rax, -1",
+        "base_case:"
+       ]
+    },
+    "expected": {
+      "rax": 152
+    }
+  }
+]
diff --git a/exercises/practice/assemble/Assemble.lean b/exercises/practice/assemble/Assemble.lean
new file mode 100644
index 0000000..3258877
--- /dev/null
+++ b/exercises/practice/assemble/Assemble.lean
@@ -0,0 +1,3 @@
+/-
+  Define syntax here for an assembly-like embedded language, according to the instructions.
+-/
diff --git a/exercises/practice/assemble/AssembleTest.lean b/exercises/practice/assemble/AssembleTest.lean
new file mode 100644
index 0000000..62f5df7
--- /dev/null
+++ b/exercises/practice/assemble/AssembleTest.lean
@@ -0,0 +1,139 @@
+import LeanTest
+import Assemble
+
+open LeanTest
+
+def assembleTests : TestSuite :=
+  (TestSuite.empty "Assemble")
+  |>.addTest "Copy a value" (do
+      let program := assemble!(
+          mov rax, rdi
+      )
+      return assertEqual (10) (program(10)))
+  |>.addTest "Sum and subtraction" (do
+      let program := assemble!(
+          mov rax, rdi
+          add rax, rdi
+          sub rax, rsi
+      )
+      return assertEqual (0) (program(10, 20)))
+  |>.addTest "Multiplication and division" (do
+      let program := assemble!(
+          mov rax, rdi
+          mul rax, rdx
+          div rax, rsi
+      )
+      return assertEqual (120) (program(100, 5, 6)))
+  |>.addTest "Bitwise operations" (do
+      let program := assemble!(
+          or rax, rcx
+          and rax, rdi
+          xor rax, rsi
+          shr rax, rdx
+      )
+      return assertEqual (16) (program(49, 16, 1, 255)))
+  |>.addTest "Skip instructions" (do
+      let program := assemble!(
+          mov rax, rdi
+          jmp end_program
+          add rax, rsi
+        end_program:
+      )
+      return assertEqual (50000000000) (program(50000000000, -3000000000)))
+  |>.addTest "Condition met" (do
+      let program := assemble!(
+          mov rax, rdi
+          cmp rax, rsi
+          jg end_program
+          add rax, rsi
+        end_program:
+      )
+      return assertEqual (40010) (program(40010, -40020)))
+  |>.addTest "Condition not met" (do
+      let program := assemble!(
+          mov rax, rdi
+          cmp rax, rsi
+          jl end_program
+          add rax, rsi
+        end_program:
+      )
+      return assertEqual (-200) (program(400, -600)))
+  |>.addTest "Registers are case-insensitive" (do
+      let program := assemble!(
+          mov RAX, rdi
+          SUB rax, Rsi
+      )
+      return assertEqual (7020) (program(4010, -3010)))
+  |>.addTest "Labels are case-sensitive" (do
+      let program := assemble!(
+          mov rax, rdi
+          cmp rax, rsi
+          jg End_program
+          sub rax, rsi
+        End_program:
+          div rax, rdx
+        end_program:
+      )
+      return assertEqual (401) (program(4010, -3010, 10)))
+  |>.addTest "All registers are used" (do
+      let program := assemble!(
+          mov rax, r8
+          add rax, r9
+          mul rax, rdx
+          sub rax, rcx
+          and rax, rdi
+          or rax, rsi
+      )
+      return assertEqual (-75586) (program(4, -75590, -10, 890, 435, -235)))
+  |>.addTest "Calculate the sum of the first 10 natural numbers" (do
+      let program := assemble!(
+        sum_first_N:
+          cmp rdi, 0
+          je base_case
+          add rax, rdi
+          sub rdi, 1
+          jmp sum_first_N
+        base_case:
+      )
+      return assertEqual (55) (program(10)))
+  |>.addTest "Count how many bits are set in 2000000000" (do
+      let program := assemble!(
+        pop_count:
+          cmp rdi, 0
+          je base_case
+          add rax, 1
+          mov rdx, rdi
+          sub rdx, 1
+          and rdi, rdx
+          jmp pop_count
+        base_case:
+      )
+      return assertEqual (13) (program(2000000000)))
+  |>.addTest "Count steps in the Collatz Conjecture starting with 1000000, -1 indicates error" (do
+      let program := assemble!(
+        steps:
+          cmp rdi, 1
+          jl error
+          je base_case
+        loop:
+          add rax, 1
+          mov rdx, rdi
+          and rdx, 1
+          cmp rdx, 0
+          je even
+          mul rdi, 3
+          add rdi, 1
+          jmp loop
+        even:
+          shr rdi, 1
+          cmp rdi, 1
+          je base_case
+          jmp loop
+        error:
+          mov rax, -1
+        base_case:
+      )
+      return assertEqual (152) (program(1000000)))
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [assembleTests]
diff --git a/exercises/practice/assemble/lakefile.toml b/exercises/practice/assemble/lakefile.toml
new file mode 100644
index 0000000..620a4e5
--- /dev/null
+++ b/exercises/practice/assemble/lakefile.toml
@@ -0,0 +1,15 @@
+name = "assemble"
+version = "0.1.0"
+defaultTargets = ["AssembleTest"]
+testDriver = "AssembleTest"
+
+[[lean_lib]]
+name = "LeanTest"
+srcDir = "vendor/LeanTest"
+
+[[lean_lib]]
+name = "Assemble"
+
+[[lean_exe]]
+name = "AssembleTest"
+root = "AssembleTest"
diff --git a/exercises/practice/assemble/lean-toolchain b/exercises/practice/assemble/lean-toolchain
new file mode 100644
index 0000000..14791d7
--- /dev/null
+++ b/exercises/practice/assemble/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.29.0
diff --git a/exercises/practice/assemble/vendor/LeanTest/LeanTest.lean b/exercises/practice/assemble/vendor/LeanTest/LeanTest.lean
new file mode 100644
index 0000000..012ba20
--- /dev/null
+++ b/exercises/practice/assemble/vendor/LeanTest/LeanTest.lean
@@ -0,0 +1,4 @@
+-- This module serves as the root of the `LeanTest` library.
+-- Import modules here that should be built as part of the library.
+import LeanTest.Assertions
+import LeanTest.Test
diff --git a/exercises/practice/assemble/vendor/LeanTest/LeanTest/Assertions.lean b/exercises/practice/assemble/vendor/LeanTest/LeanTest/Assertions.lean
new file mode 100644
index 0000000..60e4ad8
--- /dev/null
+++ b/exercises/practice/assemble/vendor/LeanTest/LeanTest/Assertions.lean
@@ -0,0 +1,166 @@
+/-
+Assertion functions for unit testing.
+-/
+
+namespace LeanTest
+
+/-- Result of a test assertion -/
+inductive AssertionResult where
+  | success : AssertionResult
+  | failure (message : String) : AssertionResult
+  deriving Repr, BEq
+
+namespace AssertionResult
+
+def isSuccess : AssertionResult → Bool
+  | success => true
+  | failure _ => false
+
+def getMessage : AssertionResult → String
+  | success => "Assertion passed"
+  | failure msg => msg
+
+end AssertionResult
+
+/-- Assert that a boolean condition is true -/
+def assert (condition : Bool) (message : String := "Assertion failed") : AssertionResult :=
+  if condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that two values are equal -/
+def assertEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected == actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected: {repr expected}\nActual: {repr actual}"
+    else
+      s!"{message}\nExpected: {repr expected}\nActual: {repr actual}"
+    .failure msg
+
+/-- Assert that two values are not equal -/
+def assertNotEqual [BEq α] [Repr α] (expected : α) (actual : α) (message : String := "") : AssertionResult :=
+  if expected != actual then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected values to be different, but both were: {repr expected}"
+    else
+      s!"{message}\nExpected values to be different, but both were: {repr expected}"
+    .failure msg
+
+/-- Refute that a boolean condition is true (assert it's false) -/
+def refute (condition : Bool) (message : String := "Refute failed - condition was true") : AssertionResult :=
+  if !condition then
+    .success
+  else
+    .failure message
+
+/-- Assert that a value is true -/
+def assertTrue (value : Bool) (message : String := "Expected true but got false") : AssertionResult :=
+  assert value message
+
+/-- Assert that a value is false -/
+def assertFalse (value : Bool) (message : String := "Expected false but got true") : AssertionResult :=
+  refute value message
+
+/-- Assert that an Option is some -/
+def assertSome [Repr α] (opt : Option α) (message : String := "Expected Some but got None") : AssertionResult :=
+  match opt with
+  | some _ => .success
+  | none => .failure message
+
+/-- Assert that an Option is none -/
+def assertNone [Repr α] (opt : Option α) (message : String := "") : AssertionResult :=
+  match opt with
+  | none => .success
+  | some val =>
+    let msg := if message.isEmpty then
+      s!"Expected None but got Some: {repr val}"
+    else
+      s!"{message}\nExpected None but got Some: {repr val}"
+    .failure msg
+
+/-- Assert that a list is empty -/
+def assertEmpty [Repr α] (list : List α) (message : String := "") : AssertionResult :=
+  match list with
+  | [] => .success
+  | _ =>
+    let msg := if message.isEmpty then
+      s!"Expected empty list but got: {repr list}"
+    else
+      s!"{message}\nExpected empty list but got: {repr list}"
+    .failure msg
+
+/-- Assert that a list contains an element -/
+def assertContains [BEq α] [Repr α] (list : List α) (element : α) (message : String := "") : AssertionResult :=
+  if list.contains element then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected list to contain {repr element}\nList: {repr list}"
+    else
+      s!"{message}\nExpected list to contain {repr element}\nList: {repr list}"
+    .failure msg
+
+/-- Assert that a value is within a range (inclusive) -/
+def assertInRange [LE α] [DecidableRel (· ≤ · : α → α → Prop)] [Repr α]
+    (value : α) (min : α) (max : α) (message : String := "") : AssertionResult :=
+  if min ≤ value ∧ value ≤ max then
+    .success
+  else
+    let msg := if message.isEmpty then
+      s!"Expected {repr value} to be in range [{repr min}, {repr max}]"
+    else
+      s!"{message}\nExpected {repr value} to be in range [{repr min}, {repr max}]"
+    .failure msg
+
+/-- Assert that an Except value is an error -/
+def assertError [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .error _ => .success
+  | .ok val =>
+    let msg := if message.isEmpty then
+      s!"Expected error but got Ok: {repr val}"
+    else
+      s!"{message}\nExpected error but got Ok: {repr val}"
+    .failure msg
+
+/-- Assert that an Except value is ok -/
+def assertOk [Repr ε] [Repr α] (result : Except ε α) (message : String := "") : AssertionResult :=
+  match result with
+  | .ok _ => .success
+  | .error err =>
+    let msg := if message.isEmpty then
+      s!"Expected Ok but got error: {repr err}"
+    else
+      s!"{message}\nExpected Ok but got error: {repr err}"
+    .failure msg
+
+/-- Assert that an IO action throws an error -/
+def assertThrows (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    let msg := if message.isEmpty then
+      "Expected IO action to throw an error, but it succeeded"
+    else
+      s!"{message}\nExpected IO action to throw an error, but it succeeded"
+    return .failure msg
+  catch _ =>
+    return .success
+
+/-- Assert that an IO action succeeds (doesn't throw) -/
+def assertSucceeds (action : IO α) (message : String := "") : IO AssertionResult := do
+  try
+    let _ ← action
+    return .success
+  catch e =>
+    let msg := if message.isEmpty then
+      s!"Expected IO action to succeed, but it threw: {e}"
+    else
+      s!"{message}\nExpected IO action to succeed, but it threw: {e}"
+    return .failure msg
+
+end LeanTest
diff --git a/exercises/practice/assemble/vendor/LeanTest/LeanTest/Test.lean b/exercises/practice/assemble/vendor/LeanTest/LeanTest/Test.lean
new file mode 100644
index 0000000..5ddbae5
--- /dev/null
+++ b/exercises/practice/assemble/vendor/LeanTest/LeanTest/Test.lean
@@ -0,0 +1,130 @@
+/-
+Test case and test suite management.
+-/
+
+import LeanTest.Assertions
+
+namespace LeanTest
+
+/-- A single test case -/
+structure TestCase where
+  description : String
+  test : IO AssertionResult
+  deriving Inhabited
+
+/-- Result of running a test -/
+structure TestResult where
+  description : String
+  result : AssertionResult
+  deriving Repr
+
+/-- A collection of tests (test suite) -/
+structure TestSuite where
+  name : String
+  tests : List TestCase
+  deriving Inhabited
+
+namespace TestSuite
+
+/-- Create an empty test suite -/
+def empty (name : String) : TestSuite :=
+  { name := name, tests := [] }
+
+/-- Add a test to the suite -/
+def addTest (suite : TestSuite) (description : String) (test : IO AssertionResult) : TestSuite :=
+  { suite with tests := suite.tests ++ [{ description := description, test := test }] }
+
+end TestSuite
+
+/-- Test statistics -/
+structure TestStats where
+  total : Nat
+  passed : Nat
+  failed : Nat
+  deriving Repr
+
+namespace TestStats
+
+def empty : TestStats :=
+  { total := 0, passed := 0, failed := 0 }
+
+def addResult (stats : TestStats) (result : AssertionResult) : TestStats :=
+  { total := stats.total + 1
+  , passed := if result.isSuccess then stats.passed + 1 else stats.passed
+  , failed := if result.isSuccess then stats.failed else stats.failed + 1
+  }
+
+end TestStats
+
+/-- ANSI color codes for terminal output -/
+def greenColor : String := "\x1b[32m"
+def redColor : String := "\x1b[31m"
+def yellowColor : String := "\x1b[33m"
+def resetColor : String := "\x1b[0m"
+def boldColor : String := "\x1b[1m"
+
+/-- Run a single test and print the result -/
+def runTest (testCase : TestCase) : IO TestResult := do
+  let result ← testCase.test
+  match result with
+  | .success =>
+    IO.println s!"  {greenColor}✓{resetColor} {testCase.description}"
+  | .failure msg =>
+    IO.println s!"  {redColor}✗{resetColor} {testCase.description}"
+    IO.println s!"    {redColor}{msg}{resetColor}"
+  return { description := testCase.description, result := result }
+
+/-- Run all tests in a test suite -/
+def runTestSuite (suite : TestSuite) : IO TestStats := do
+  IO.println s!"\n{boldColor}{suite.name}{resetColor}"
+  let mut stats := TestStats.empty
+
+  for testCase in suite.tests do
+    let result ← runTest testCase
+    stats := stats.addResult result.result
+
+  return stats
+
+/-- Print test summary -/
+def printSummary (stats : TestStats) : IO Unit := do
+  IO.println ""
+  IO.println s!"{boldColor}Test Summary:{resetColor}"
+  IO.println s!"  Total:  {stats.total}"
+  IO.println s!"  {greenColor}Passed: {stats.passed}{resetColor}"
+
+  if stats.failed > 0 then
+    IO.println s!"  {redColor}Failed: {stats.failed}{resetColor}"
+    IO.println s!"\n{redColor}FAILED{resetColor}"
+  else
+    IO.println s!"\n{greenColor}ALL TESTS PASSED{resetColor}"
+
+/-- Run multiple test suites -/
+def runTestSuites (suites : List TestSuite) : IO Unit := do
+  let mut totalStats := TestStats.empty
+
+  for suite in suites do
+    let stats ← runTestSuite suite
+    totalStats := {
+      total := totalStats.total + stats.total,
+      passed := totalStats.passed + stats.passed,
+      failed := totalStats.failed + stats.failed
+    }
+
+  printSummary totalStats
+
+/-- Run multiple test suites and return exit code (0 = all passed, 1 = some failed) -/
+def runTestSuitesWithExitCode (suites : List TestSuite) : IO UInt32 := do
+  let mut totalStats := TestStats.empty
+
+  for suite in suites do
+    let stats ← runTestSuite suite
+    totalStats := {
+      total := totalStats.total + stats.total,
+      passed := totalStats.passed + stats.passed,
+      failed := totalStats.failed + stats.failed
+    }
+
+  printSummary totalStats
+  return if totalStats.failed > 0 then 1 else 0
+
+end LeanTest
diff --git a/generators/Generator/Generator.lean b/generators/Generator/Generator.lean
index bfb905d..55b841e 100644
--- a/generators/Generator/Generator.lean
+++ b/generators/Generator/Generator.lean
@@ -1,3 +1,4 @@
+import Generator.AssembleGenerator
 import Generator.AlphameticsGenerator
 import Generator.PascalsTriangleGenerator
 import Generator.ResistorColorDuoGenerator
@@ -107,6 +108,7 @@ abbrev endBodyGenerator := String -> String
 
 def dispatch : Std.HashMap String (introGenerator × testCaseGenerator × endBodyGenerator) :=
   Std.HashMap.ofList [
+    ("Assemble", (AssembleGenerator.genIntro, AssembleGenerator.genTestCase, AssembleGenerator.genEnd)),
     ("Alphametics", (AlphameticsGenerator.genIntro, AlphameticsGenerator.genTestCase, AlphameticsGenerator.genEnd)),
     ("PascalsTriangle", (PascalsTriangleGenerator.genIntro, PascalsTriangleGenerator.genTestCase, PascalsTriangleGenerator.genEnd)),
     ("ResistorColorDuo", (ResistorColorDuoGenerator.genIntro, ResistorColorDuoGenerator.genTestCase, ResistorColorDuoGenerator.genEnd)),
diff --git a/generators/Generator/Generator/AssembleGenerator.lean b/generators/Generator/Generator/AssembleGenerator.lean
new file mode 100644
index 0000000..32fee1a
--- /dev/null
+++ b/generators/Generator/Generator/AssembleGenerator.lean
@@ -0,0 +1,55 @@
+import Lean.Data.Json
+import Std
+import Helper
+
+open Lean
+open Std
+open Helper
+
+namespace AssembleGenerator
+
+def genIntro (exercise : String) : String := s!"import LeanTest
+import {exercise}
+
+open LeanTest
+
+def {exercise.decapitalize}Tests : TestSuite :=
+  (TestSuite.empty \"{exercise}\")"
+
+def genTestCase (_exercise : String) (case : TreeMap.Raw String Json) : String :=
+  let input := case.get! "input"
+  let args := input.getObjValD "args"
+    |>.getArr?
+    |> getOk
+    |>.toList
+    |>.map (fun x => s!"{x}")
+    |> String.intercalate ", "
+  let code := input.getObjValD "code"
+    |>.getArr?
+    |> getOk
+    |>.toList
+    |>.map (fun x => toLiteral s!"{x}")
+    |>.map (fun ln =>
+      if ln.contains ":" then "        " ++ ln
+      else "          " ++ ln
+    )
+    |> String.intercalate "\n"
+  let expected := case.get! "expected" |>.getObjValD "rax"
+  let description := case.get! "description"
+              |> (·.compress)
+  let call := s!"(program({args}))"
+  s!"
+  |>.addTest {description} (do
+      let program := assemble!(
+{code}
+      )
+      return assertEqual ({expected}) {call})"
+
+def genEnd (exercise : String) : String :=
+  s!"
+
+def main : IO UInt32 := do
+  runTestSuitesWithExitCode [{exercise.decapitalize}Tests]
+"
+
+end AssembleGenerator