diff --git a/Cslib.lean b/Cslib.lean
index 1d0469a56..7d2baa571 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -28,6 +28,7 @@ public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
 public import Cslib.Computability.Automata.Transducers.Transducer
+public import Cslib.Computability.Automata.TwoWayNA.Basic
 public import Cslib.Computability.Distributed.FLP.Algorithm
 public import Cslib.Computability.Distributed.FLP.CanReachVia
 public import Cslib.Computability.Distributed.FLP.Consensus
diff --git a/Cslib/Computability/Automata/TwoWayNA/Basic.lean b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
new file mode 100644
index 000000000..b7188b6a6
--- /dev/null
+++ b/Cslib/Computability/Automata/TwoWayNA/Basic.lean
@@ -0,0 +1,109 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Computability.Automata.Acceptors.Acceptor
+public import Mathlib.Data.List.Chain
+public import Mathlib.Data.Sign.Basic
+public import Cslib.Foundations.Data.List.IsChainFromTo
+
+/-! # Nondeterministic Two-Way Automaton
+
+A Nondeterministic Two-Way Automaton (`TwoWayNA`) reads a finite input word on a tape and may move
+its input head in either direction. A transition reads the symbol under the head and, besides
+changing the state, moves the head one cell to the left, keeps it in place, or moves it one cell to
+the right.
+
+The input head cannot leave the input word to the left (in the sense that execution gets stuck in
+this case) and once it leaves the word to the right, it stops. A run is accepting if and only if it
+ends in an accepting state with the head just past the end of the input.
+
+## Main definitions
+
+* `TwoWayNA`, the automaton itself
+* `TwoWayNACfg`, a configuration of a `TwoWayNA`: Its input plus a state and the head position.
+* `TwoWayNA.Step`, The single-step relation between configurations.
+
+## Implementation notes
+
+The definition of `TwoWayNA` is kept close to [Vardi][Vardi1989]'s, because the main point is to
+prove that it accepts the same languages as `NA.FinAcc` via his proof. This means we do not allow
+the head to move off the input to the left (in the sense that if the transition relation has an
+entry that would cause that, there is no successor configuration, the computation is stuck), but
+also do not provide an end marker. Once the head moves off to the right, the machine instantly
+stops, so it also cannot move back into the word.
+
+## References
+
+* [Moshe Y. Vardi, *A Note on the Reduction of Two-Way Automata to One-Way Automata*][Vardi1989]
+
+-/
+
+@[expose] public section
+
+namespace Cslib.Automata
+
+variable {State Symbol : Type*}
+
+/-- A nondeterministic two-way automaton: a transition relation that reads an input symbol and
+moves the input head, together with a set of initial and a set of accepting states. -/
+structure TwoWayNA (State Symbol : Type*) where
+  /-- The transition relation. `Tr q x m q'` means that, while reading the symbol `x`, the
+  automaton attempts to transition from state `q` to state `q'` and move its head according to
+  `m`. -/
+  Tr (q : State) (x : Symbol) (m : SignType) (q' : State) : Prop
+  /-- The set of initial states of the automaton. -/
+  start : Set State
+  /-- The set of accepting states of the automaton. -/
+  accept : Set State
+
+/-- The configuration of a two-way nondeterministic automaton. -/
+@[ext]
+structure TwoWayNACfg (State Symbol : Type*) where
+  /-- The original input to the automaton. -/
+  input : List Symbol
+  /-- The state of the automaton. -/
+  state : State
+  /-- The input head position of the automaton: it can be on any symbol of the input or on the
+  position one step to the right of the input. -/
+  pos : Fin (input.length + 1)
+
+/-- This defines the set of initial configurations on a specific input. -/
+def TwoWayNACfg.IsInitialForInput (a : TwoWayNA State Symbol) (c : TwoWayNACfg State Symbol)
+    (input : List Symbol) : Prop :=
+  c.state ∈ a.start ∧ c.pos = 0 ∧ c.input = input
+
+/-- If a configuration is a accepting. -/
+def TwoWayNACfg.IsAccepting (a : TwoWayNA State Symbol) (c : TwoWayNACfg State Symbol) : Prop :=
+  c.state ∈ a.accept ∧ c.pos = Fin.last _
+
+/-- Returns a nondeterministic finite acceptor on the configurations as states, accepting exactly
+the runs of the two-way automaton on `input` that end in an accepting configuration. -/
+def TwoWayNA.toCfgNAFinAcc {State Symbol : Type*} (a : TwoWayNA State Symbol)
+    (input : List Symbol) :
+    NA.FinAcc (TwoWayNACfg State Symbol) (Symbol × SignType) where
+  Tr
+    | c, (x, m), c' =>
+      c.input = c'.input ∧
+      -- This also enforces that `c`'s input head position has to be inside the word.
+      some x = c.input[c.pos]? ∧
+      a.Tr c.state x m c'.state ∧
+      -- By doing input head position arithmetic and comparison in the integers, we get the
+      -- desired restrictions since `0 ≤ c'.pos < n + 1` and `0 ≤ c.pos < n`:
+      -- The input head after the transition cannot be left of the word but it is fine to be
+      -- one position right of the word (in which case no further transition is possible).
+      (c'.pos : ℤ) = (c.pos : ℤ) + (m.cast : ℤ)
+  start := { c | c.IsInitialForInput a input }
+  accept := { c | c.IsAccepting a }
+
+@[simp, scoped grind =]
+instance : Acceptor (TwoWayNA State Symbol) Symbol where
+  Accepts (a : TwoWayNA State Symbol) (input : List Symbol) :=
+    ∃ μs, Acceptor.Accepts (a.toCfgNAFinAcc input) μs
+
+end Cslib.Automata
diff --git a/Cslib/Computability/Automata/TwoWayNA/BasicAlt.lean b/Cslib/Computability/Automata/TwoWayNA/BasicAlt.lean
new file mode 100644
index 000000000..d1a356b13
--- /dev/null
+++ b/Cslib/Computability/Automata/TwoWayNA/BasicAlt.lean
@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Computability.Automata.NA.Basic
+public import Cslib.Computability.Automata.Acceptors.Acceptor
+public import Mathlib.Data.List.Chain
+public import Mathlib.Data.Sign.Basic
+public import Cslib.Foundations.Data.List.IsChainFromTo
+
+/-! # Nondeterministic Two-Way Automaton
+-/
+
+@[expose] public section
+
+namespace Cslib.Automata
+
+variable {State Symbol : Type*}
+
+/-- The word to be accepted is put in the state component `input`. This is necessary
+because the `Acceptor` framework refers only to the automaton and nothing else.  So
+you can't make the word to be accepted a parameter of the automaton. -/
+@[ext]
+structure TwoWayState (State Symbol : Type*) where
+  state : State
+  input : List Symbol
+  inpPos : ℕ
+
+/-- Another alternative is to use `Unit` for this type.  But I thik exposing the contents of
+the state transitions can potentially faciliate proofs because an execution in the sense
+of `LTS.Execution` would then include all nondeterministic choices made by an execution. -/
+@[ext]
+structure TwoWaySymbol (Symbol : Type*) where
+  symbol : Symbol
+  dir : SignType
+
+abbrev TwoWayLTS (State Symbol : Type*) :=
+  LTS (TwoWayState State Symbol) (TwoWaySymbol Symbol)
+
+structure TwoWayNA (State Symbol : Type*) where
+  LTS : TwoWayLTS State Symbol
+  start : Set (TwoWayState State Symbol)
+  accept : Set (TwoWayState State Symbol)
+  /-- We require that the state component `input` never changes. -/
+  input_inv : ∀ s x t, LTS.Tr s x t → t.input = s.input
+
+namespace TwoWayNA
+
+/-- The word to be accepted is put in the state component `input` at the beginning.
+The read pointer `inpPos` is at 0 at the beginning and just beyond `input` at the end.
+You can choose to change that requirement. -/
+instance : Acceptor (TwoWayNA State Symbol) Symbol where
+  Accepts (a : TwoWayNA State Symbol) (xs : List Symbol) : Prop :=
+    ∃ s, s ∈ a.start ∧ s.input = xs ∧ s.inpPos = 0 ∧
+      ∃ ys t, a.LTS.MTr s ys t ∧ t ∈ a.accept ∧ t.inpPos = s.input.length
+
+end TwoWayNA
+
+def TwoWayTr (State Symbol : Type*) := State → Symbol → SignType → State → Prop
+
+def twoWayLTS.mk (tr : TwoWayTr State Symbol) : TwoWayLTS State Symbol where
+  Tr s' x' t' := ∃ _ : s'.inpPos < s'.input.length,
+    s'.input[s'.inpPos] = x'.symbol ∧ t'.input = s'.input ∧
+    tr s'.state x'.symbol x'.dir t'.state ∧
+    match x'.dir with
+    | SignType.zero => t'.inpPos = s'.inpPos
+    | SignType.pos => t'.inpPos = s'.inpPos.succ
+    | SignType.neg => t'.inpPos = s'.inpPos.pred
+
+def twoWayNA.mk (tr : TwoWayTr State Symbol) (start accept : Set State)
+    : TwoWayNA State Symbol where
+  LTS := twoWayLTS.mk tr
+  start := (fun s' ↦ s'.state) ⁻¹' start
+  accept := (fun s' ↦ s'.state) ⁻¹' accept
+  input_inv s' x' t' := by grind [twoWayLTS.mk]
+
+end Cslib.Automata
diff --git a/Cslib/Foundations/Semantics/LTS/Execution.lean b/Cslib/Foundations/Semantics/LTS/Execution.lean
index fd49f191e..cac09cbb9 100644
--- a/Cslib/Foundations/Semantics/LTS/Execution.lean
+++ b/Cslib/Foundations/Semantics/LTS/Execution.lean
@@ -7,6 +7,7 @@ Authors: Fabrizio Montesi, Ching-Tsun Chou
 module
 
 public import Cslib.Foundations.Semantics.LTS.Basic
+public import Cslib.Foundations.Data.List.IsChainFromTo
 
 /-!
 # Finite executions of LTS
@@ -84,10 +85,16 @@ theorem Execution.to_mTr (hexec : lts.Execution s1 μs s2 ss) :
         apply this
       · grind
 
+/-- The states visited by an execution form a chain from the initial to the final state
+in the underlying unlabelled relation. -/
+theorem Execution.isChainFromTo (hexec : lts.Execution s1 μs s2 ss) :
+    ss.IsChainFromTo lts.UnlabelledTr s1 s2 := by
+  grind [List.IsChainFromTo, Execution, List.isChain_iff_getElem, UnlabelledTr]
+
 /-- The states visited by an execution form a chain in the underlying unlabelled relation. -/
 theorem Execution.isChain (hexec : lts.Execution s1 μs s2 ss) :
-    ss.IsChain lts.UnlabelledTr := by
-  grind [Execution, List.isChain_iff_getElem, UnlabelledTr]
+    ss.IsChain lts.UnlabelledTr :=
+  (Execution.isChainFromTo hexec).isChain
 
 open scoped Execution
 /-- Correspondence of multistep transitions and executions. -/
diff --git a/references.bib b/references.bib
index d2a7dfb13..48aa4fd76 100644
--- a/references.bib
+++ b/references.bib
@@ -551,3 +551,13 @@ @book{Papadimitriou94
   publisher={Addison-Wesley},
   address={Reading, Massachusetts}
 }
+
+@article{Vardi1989,
+  author       = {Moshe Y. Vardi},
+  title        = {A Note on the Reduction of Two-Way Automata to One-Way Automata},
+  journal      = {Information Processing Letters},
+  volume       = {30},
+  number       = {5},
+  pages        = {261--264},
+  year         = {1989}
+}