diff --git a/Cslib.lean b/Cslib.lean
index eea1f4491..43c374ae7 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -36,7 +36,9 @@ public import Cslib.Computability.Languages.MyhillNerode
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Machines.Turing.SingleTape.Defs
 public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
new file mode 100644
index 000000000..5cac8d41b
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Defs.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Bolton Bailey
+-/
+
+module
+
+public import Cslib.Foundations.Data.BiTape
+
+/-! # Basic definitions for Turing Machines (TMs) -/
+
+@[expose] public section
+
+namespace Cslib.Computability.Turing.SingleTape
+
+/-- The transition labels used by a single-tape Turing Machine. -/
+inductive TrLabel (Symbol : Type*)
+  /-- Read `x` from the tape. -/
+  | read (x : Symbol)
+  /-- Write `x` on the tape. -/
+  | write (x : Symbol)
+  /-- Move the head of the tape. -/
+  | move (d : Turing.Dir)
+  /-- Do nothing. -/
+  | skip
+
+/-- Applies a transition label to a tape, returning `none` if it is not possible.
+The input is taken as an `Option` to make the function composable. -/
+def TrLabel.applyToTape [DecidableEq Symbol]
+    (otape : Option (Turing.BiTape Symbol)) (μ : TrLabel Symbol) :
+    Option (Turing.BiTape Symbol) :=
+  match μ, otape with
+  | read x, some tape => if x = tape.head then some tape else none
+  | write x, some tape => some (tape.write x)
+  | move d, some tape => some (tape.move d)
+  | skip, some tape => some tape
+  | _, _ => none
+
+@[scoped grind →]
+theorem TrLabel.applyToTape_isSome [DecidableEq Symbol] {μ : TrLabel Symbol}
+    {ot : Option (Turing.BiTape Symbol)} (h : (μ.applyToTape ot).isSome) : ot.isSome := by
+  have ⟨t', ht'⟩ := Option.isSome_iff_exists.mp h
+  simp only [applyToTape] at ht'
+  grind [applyToTape]
+
+@[scoped grind →]
+theorem TrLabel.applyToTape_foldl_isSome [DecidableEq Symbol] {μs : List (TrLabel Symbol)}
+    {ot : Option (Turing.BiTape Symbol)} (h : (μs.foldl applyToTape ot).isSome) : ot.isSome := by
+  induction μs generalizing ot <;> grind
+
+/-- Configuration of a single-tape Turing machine. -/
+@[ext]
+structure Cfg (State Symbol : Type*) where
+  /-- The state that the machine is in. -/
+  state : State
+  /-- Tape of the machine (memory). -/
+  tape : Turing.BiTape Symbol
+
+/-- Helper builder for a configuration with a given tape content. -/
+def Cfg.mk₁ (s : State) (xs : List Symbol) : Cfg State Symbol where
+  state := s
+  tape := Turing.BiTape.mk₁ xs
+
+/-- The space used by a configuration is the space used by its tape. -/
+def Cfg.spaceUsed (cfg : Cfg State Symbol) : ℕ := cfg.tape.spaceUsed
+
+end Cslib.Computability.Turing.SingleTape
diff --git a/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
new file mode 100644
index 000000000..0a21bd9ec
--- /dev/null
+++ b/Cslib/Computability/Machines/Turing/SingleTape/NonDeterministic.lean
@@ -0,0 +1,110 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Foundations.Relation.Defs
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Computability.Automata.Transducers.Transducer
+public import Cslib.Foundations.Data.BiTape
+public import Cslib.Computability.Machines.Turing.SingleTape.Defs
+
+/-! # Single-Tape Nondeterministic Turing Machines (NTMs)
+
+Nondeterministic Turing Machines (NTMs), defined as nondeterministic automata (`NA`) that act on a
+bidirectional tape (`BiTape`).
+-/
+
+@[expose] public section
+
+namespace Cslib.Computability.Turing.SingleTape
+
+open Automata
+
+/-- A (single-tape) Nondeterministic Turing Machine (NTM) is a nondeterministic automaton equipped
+with a set of accepting halting states. -/
+structure SingleTapeNTM (State Symbol : Type*)
+    extends NA State (TrLabel Symbol) where
+  /-- The set of accepting states. -/
+  accept : Set State
+  /-- Proof that all accepting states are halting states. -/
+  accept_halting (hmem : s ∈ accept) : ¬∃ μ s', Tr s μ s'
+
+variable {State Symbol : Type*}
+
+namespace SingleTapeNTM
+
+variable [DecidableEq Symbol]
+
+/-- An NTM yields a small-step operational semantics on configurations, which codifies an execution
+step. -/
+def Red (m : SingleTapeNTM State Symbol)
+    (c c' : Cfg State Symbol) : Prop :=
+  ∃ μ, m.Tr c.state μ c'.state ∧ μ.applyToTape c.tape = c'.tape
+
+@[scoped grind =]
+theorem red_tr {m : SingleTapeNTM State Symbol} :
+    m.Red c c' ↔ ∃ μ, m.Tr c.state μ c'.state ∧ μ.applyToTape c.tape = c'.tape := by rfl
+
+/-- Multistep execution of an NTM, defined as the reflexive and transitive closure of one-step
+execution.
+-/
+def MRed (m : SingleTapeNTM State Symbol) := Relation.ReflTransGen m.Red
+
+open scoped LTS LTS.MTr TrLabel
+
+/-- Characterisation of executions in terms of multistep transitions. -/
+@[scoped grind =]
+theorem mRed_mTr {m : SingleTapeNTM State Symbol} :
+    m.MRed c c' ↔ ∃ μs, m.MTr c.state μs c'.state ∧
+    μs.foldl TrLabel.applyToTape (some c.tape) = c'.tape := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    induction h using Relation.ReflTransGen.head_induction_on
+    case refl =>
+      exists []
+      grind
+    case head _ c cb hred hmred ih =>
+      rcases ih with ⟨μs, hmtr, ih⟩
+      have ⟨μ, _⟩ := red_tr.mp hred
+      exists μ :: μs
+      grind
+  case mpr =>
+    rcases h with ⟨μs, hmtr, h⟩
+    induction μs generalizing c
+    case nil =>
+      rw [show c = c' by grind [Cfg.ext]]
+      apply Relation.ReflTransGen.refl
+    case cons μ μs ih =>
+      cases hmtr
+      case stepL sb htr hmtr =>
+        have hat : ∀ (μ : TrLabel Symbol) t, (μ.applyToTape t).isSome → t.isSome := by grind
+        have ⟨tb, htb⟩ : ∃ tb, μ.applyToTape c.tape = some tb := by grind [Option.isSome_iff_exists]
+        let cb := {state := sb, tape := tb : Cfg State Symbol}
+        have hmred : m.MRed cb c' := by grind
+        apply Relation.ReflTransGen.head (b := cb) (by grind)
+        simp only [MRed] at hmred
+        grind
+
+/-- An NTM is an acceptor of finite lists of symbols. -/
+instance : Acceptor (SingleTapeNTM State Symbol) Symbol where
+    Accepts (m : SingleTapeNTM State Symbol) (xs : List Symbol) :=
+  ∃ s ∈ m.start, ∃ c', c'.state ∈ m.accept ∧ m.MRed (Cfg.mk₁ s xs) c'
+
+/-- An NTM is a transducer of finite lists of symbols. -/
+instance : Transducer (SingleTapeNTM State Symbol) Symbol Symbol where
+    Translates (m : SingleTapeNTM State Symbol) (xs ys : List Symbol) :=
+  ∃ s ∈ m.start, ∃ c',
+    c'.state ∈ m.accept ∧
+    m.MRed (Cfg.mk₁ s xs) c' ∧
+    /- The following condition on output deviates from textbooks, in order to have the same
+    criterion as for deterministic TMs. We might want to revisit this in the future.
+    -/
+    c'.tape = Turing.BiTape.mk₁ ys
+
+end SingleTapeNTM
+
+end Cslib.Computability.Turing.SingleTape