diff --git a/Code/driver/src/mux.rs b/Code/driver/src/mux.rs
index 9f52cdd6d..33314a2eb 100644
--- a/Code/driver/src/mux.rs
+++ b/Code/driver/src/mux.rs
@@ -200,7 +200,7 @@ where
     }
 
     /// After a step change, see if there is an input to be
-    /// sent implictly to the round state machine.
+    /// sent implicitly to the round state machine.
     pub fn multiplex_step_change(
         &self,
         pending_step: Step,
diff --git a/Code/test/tests/driver_extra.rs b/Code/test/tests/driver_extra.rs
index 5731cf0b1..edb7aaddc 100644
--- a/Code/test/tests/driver_extra.rs
+++ b/Code/test/tests/driver_extra.rs
@@ -30,7 +30,7 @@ use malachite_test::utils::*;
 // - L36 with previoustly received polkaValue and proposal, and entering prevote (due to received proposal)
 //      `driver_steps_polka_value_then_proposal()`
 //
-// - L34 with previously received polkaAny and entering prevote (due to received poposal)
+// - L34 with previously received polkaAny and entering prevote (due to received proposal)
 //      `driver_steps_polka_any_then_proposal_other()`
 
 struct TestStep {
@@ -788,7 +788,7 @@ fn driver_steps_polka_value_then_proposal() {
     run_steps(&mut driver, steps);
 }
 
-// Arrive at L34 with previously received polkaAny and entering prevote (due to received poposal)
+// Arrive at L34 with previously received polkaAny and entering prevote (due to received proposal)
 //
 // Ev:             NewRound(0)           <polkaAny(v)>          Proposal(v')         + replay <polkaAny>
 // State: NewRound ------------> Propose -------------> Propose -----------> Prevote -------------------------> Prevote
diff --git a/Docs/architecture/adr-001-architecture.md b/Docs/architecture/adr-001-architecture.md
index a2504feda..3911060cb 100644
--- a/Docs/architecture/adr-001-architecture.md
+++ b/Docs/architecture/adr-001-architecture.md
@@ -394,7 +394,7 @@ pub fn apply(self, data: &Info<Ctx>, input: Input<Ctx>) -> Transition<Ctx> {
 The events passed to the Round state machine are very close to the preconditions for the transition functions in the BFT paper, i.e., the `upon` clauses.
 In addition:
 - The `StartRound` events specify if the SM runs in the proposer mode or not. In the former case, the driver also passes a valid value to the round SM.
-- There are two `Poposal` events, for valid and invalid values respectively. Therefore, the `valid(v)` check is not performed in the round SM but by the Driver
+- There are two `Proposal` events, for valid and invalid values respectively. Therefore, the `valid(v)` check is not performed in the round SM but by the Driver
 
 ```rust
 pub enum Input<Ctx>
diff --git a/Specs/English/README.md b/Specs/English/README.md
index 55dc441ef..77b504e3b 100644
--- a/Specs/English/README.md
+++ b/Specs/English/README.md
@@ -197,7 +197,7 @@ interaction with other modules.
 ### Round state-machine
 
 The state machine represents the operation of consensus at a single `Height(h)` and `Round(r)`.
-The diagram below offers a visual representation of the state machine. It shows the input events, using green for simple inputs (e.g. timeouts, porposal)
+The diagram below offers a visual representation of the state machine. It shows the input events, using green for simple inputs (e.g. timeouts, proposal)
 and red for the complex events (e.g. `ProposalAndPolkaCurrent` is sent to the state machine when a valid proposal and a polka of prevotes have been received).
 The actions are shown in italics (blue) and the output messages are shown in blue.
 
diff --git a/Specs/Quint/TendermintDSL.qnt b/Specs/Quint/TendermintDSL.qnt
index 527fda574..412e84407 100644
--- a/Specs/Quint/TendermintDSL.qnt
+++ b/Specs/Quint/TendermintDSL.qnt
@@ -27,8 +27,8 @@ run ListDeliverSomeProposal (active) = {
     active.length().reps(i => deliverSomeProposal(active[i]))
 }
 
-run ProcessDeliverAllVotes(voteType, recepient, fromList, valset, h, r, value) =
-    fromList.length().reps(i => deliverVote(recepient, mkVote(voteType, fromList[i], h, r, value)))
+run ProcessDeliverAllVotes(voteType, recipient, fromList, valset, h, r, value) =
+    fromList.length().reps(i => deliverVote(recipient, mkVote(voteType, fromList[i], h, r, value)))
 
 run ListDeliverAllVotes(voteType, fromList, toList, valset, h, r, value) =
     toList.length().reps(i => ProcessDeliverAllVotes(voteType, toList[i], fromList, valset, h, r, value))
diff --git a/Specs/Quint/driver.qnt b/Specs/Quint/driver.qnt
index 5eb037c07..30d687734 100644
--- a/Specs/Quint/driver.qnt
+++ b/Specs/Quint/driver.qnt
@@ -446,7 +446,7 @@ module driver {
             // this might be cheating as we look into the "es"
             (state, PendingDInput(input_height_round._1))
             // I DID IT. TODO: In the "starkBFT Spec" Google doc, it is written that pending events
-            // should be executed before new messages, which would requir to push this
+            // should be executed before new messages, which would require to push this
             // branch up.
 
         else if (state.incomingProposals != Set())
diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt
index f7495280a..179c886d2 100644
--- a/Specs/Quint/voteBookkeeper.qnt
+++ b/Specs/Quint/voteBookkeeper.qnt
@@ -341,7 +341,7 @@ module voteBookkeeper {
     var weightedVote: WeightedVote
     // The state of the Bookkeeper.
     var bookkeeper: Bookkeeper
-    // The output outputing from applying a weighted vote to the bookkeeper.
+    // The output outputting from applying a weighted vote to the bookkeeper.
     var lastEmitted: VoteKeeperOutput
 
     // ************************************************************************