diff --git a/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean b/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean
index 96d885a87..0feba1945 100644
--- a/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean
+++ b/Cslib/Computability/Distributed/FLP/ZeroConsensus.lean
@@ -33,7 +33,7 @@ namespace Cslib.FLP.ZeroFaultAlg
 open Set Sum Option Multiset ωSequence
 
 /-- The payload of a message is of type `Bool ⊕ Bool`, where `inl b` denotes an input value `b`
-ane `inr b` denotes a value `b` sent by process 0 to all processes (including itself). -/
+and `inr b` denotes a value `b` sent by process 0 to all processes (including itself). -/
 abbrev M := Bool
 
 /-- The local state of a process is trivial. -/
diff --git a/Cslib/Computability/Languages/MyhillNerode.lean b/Cslib/Computability/Languages/MyhillNerode.lean
index f22fe8646..e42d3d325 100644
--- a/Cslib/Computability/Languages/MyhillNerode.lean
+++ b/Cslib/Computability/Languages/MyhillNerode.lean
@@ -23,7 +23,7 @@ The Myhill-Nerode theorem has three parts [WikipediaMyhillNerode2026]:
 
 (3) The minimal DFA is unique up to unique isomorphism. That is, for any
     minimal DFA accepting `l`, there exists exactly an isomorphism from it to the
-    canonical DFA whose states are the equivalence classses of `c_l`, whose
+    canonical DFA whose states are the equivalence classes of `c_l`, whose
     state transitions are of the form `⟦ x ⟧ → ⟦ x ++ [a] ⟧` (where `a : α`
     and `x : List α`), whose initial state is `⟦ [] ⟧`, and whose accepting states
     are `{ ⟦ x ⟧ | x ∈ l }`.
diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean
index f649ed5dd..888e64c46 100644
--- a/Cslib/Foundations/Relation/Defs.lean
+++ b/Cslib/Foundations/Relation/Defs.lean
@@ -85,7 +85,7 @@ abbrev Normalizable (r : α → α → Prop) (x : α) : Prop :=
 abbrev Normalizing (r : α → α → Prop) : Prop :=
   ∀ x, Normalizable r x
 
-/-- An element `x` is `SN` (for strongly-normalising) for a relation `r` if it is accesible under
+/-- An element `x` is `SN` (for strongly-normalising) for a relation `r` if it is accessible under
 the inverse of `r`. -/
 abbrev SN (r : α → α → Prop) := Acc (fun a b => r b a)
 
diff --git a/Cslib/Foundations/Semantics/LTS/Basic.lean b/Cslib/Foundations/Semantics/LTS/Basic.lean
index b1f864f89..ae62ed778 100644
--- a/Cslib/Foundations/Semantics/LTS/Basic.lean
+++ b/Cslib/Foundations/Semantics/LTS/Basic.lean
@@ -148,7 +148,7 @@ theorem MTr.single_invert (s1 : State) (μ : Label) (s2 : State) :
     cases hmtr
     exact htr
 
-/-- A 1-sized multistep transition is exactly a single transision with the given label. -/
+/-- A 1-sized multistep transition is exactly a single transition with the given label. -/
 @[simp] theorem MTr.singleton_iff (s1 : State) (μ : Label) (s2 : State) :
   lts.MTr s1 [μ] s2 ↔ lts.Tr s1 μ s2 := ⟨MTr.single_invert lts s1 μ s2, MTr.single lts⟩
 
diff --git a/Cslib/Foundations/Semantics/LTS/TraceEq.lean b/Cslib/Foundations/Semantics/LTS/TraceEq.lean
index 45782b67a..700ddf0c3 100644
--- a/Cslib/Foundations/Semantics/LTS/TraceEq.lean
+++ b/Cslib/Foundations/Semantics/LTS/TraceEq.lean
@@ -136,19 +136,19 @@ theorem HomTraceEq.eqv : Equivalence (· ~tr[lts] ·) where
 instance : Trans (TraceEq lts₁ lts₂) (TraceEq lts₂ lts₃) (TraceEq lts₁ lts₃) where
   trans := TraceEq.trans
 
-/-- For trace-equivalent states, any multistep transition of one can be mimiced by the other. -/
+/-- For trace-equivalent states, any multistep transition of one can be mimicked by the other. -/
 theorem TraceEq.exists_mTr_of_mTr {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label}
     (h : s₁ ~tr[lts₁,lts₂] s₂) (htr : lts₁.MTr s₁ μs s₁') : ∃ s₂', lts₂.MTr s₂ μs s₂' := by
   rw [←mem_traces_iff, ←h]
   exact ⟨s₁', htr⟩
 
-/-- For trace-equivalent states, any single-step transition of one can be mimiced by the other. -/
+/-- For trace-equivalent states, any single-step transition of one can be mimicked by the other. -/
 theorem TraceEq.exists_tr_of_tr {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label}
     (h : s₁ ~tr[lts₁,lts₂] s₂) (htr : lts₁.Tr s₁ μ s₁') : ∃ s₂', lts₂.Tr s₂ μ s₂' := by
   rw [←mem_traces_singleton_iff, ←h, mem_traces_singleton_iff]
   exact ⟨s₁', htr⟩
 
-/-- For deterministic lts's, trace equivalence is preseved by respective transitions with the same
+/-- For deterministic lts's, trace equivalence is preserved by respective transitions with the same
 label. -/
 theorem TraceEq.traceEq_of_tr_of_tr {lts₁ : LTS State₁ Label} {lts₂ : LTS State₂ Label}
     [hdet₁ : lts₁.Deterministic] [hdet₂ : lts₂.Deterministic] (h : s₁ ~tr[lts₁,lts₂] s₂)
diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 017c60ec9..048c650e8 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -145,7 +145,7 @@ This result proves that the definition is correct. -/
 theorem Satisfies.box_iff_forall {m : Model World Atom} :
     ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind [Proposition.box]
 
-/-- The theory of a world in a model is the set of all propositions that it satifies. -/
+/-- The theory of a world in a model is the set of all propositions that it satisfies. -/
 abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) :=
   {φ | ⇓Modal[m,w ⊨ φ]}