diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1
index 4810ac443b2..98ea94c5349 100644
--- a/doc/man/goto-instrument.1
+++ b/doc/man/goto-instrument.1
@@ -346,7 +346,7 @@ void \fBtest_get_message\fP() {
 
 The harness verifies that \fIget_message\fR assigns non-decreasing time stamps
 to the returned messages. However, simply treating \fIclock\fR as
-non-deterministic would not allow to prove this property. Thus, we can supply a
+non-deterministic would not suffice to prove this property. Thus, we can supply a
 model for reads from \fIclock\fR:
 
 .EX
diff --git a/scripts/cpplint.py b/scripts/cpplint.py
index 169826b0f9e..845267986d2 100755
--- a/scripts/cpplint.py
+++ b/scripts/cpplint.py
@@ -2266,7 +2266,7 @@ def FindDoStart(clean_lines, linenum):
 
   Work our way up through the lines starting at linenum to find a do
   that hasn't been matched. This might not succeed as might just be an
-  emtpy while statement.
+  empty while statement.
 
   Args:
     clean_lines: A CleansedLines instance containing the file.
diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c
index 576b983fee9..602ce3b89c4 100644
--- a/src/ansi-c/library/cprover_contracts.c
+++ b/src/ansi-c/library/cprover_contracts.c
@@ -780,7 +780,7 @@ __CPROVER_HIDE:;
   if(set->allocated.elems[__CPROVER_POINTER_OBJECT(ptr)] != 0)
     return 1;
 
-  // don't even drive symex into the rest of the function if the set is emtpy
+  // don't even drive symex into the rest of the function if the set is empty
   if(set->contract_assigns.max_elems == 0)
     return 0;
 
diff --git a/src/solvers/flattening/boolbv_concatenation.cpp b/src/solvers/flattening/boolbv_concatenation.cpp
index 6eb15703892..4fcb5e936d4 100644
--- a/src/solvers/flattening/boolbv_concatenation.cpp
+++ b/src/solvers/flattening/boolbv_concatenation.cpp
@@ -18,7 +18,7 @@ bvt boolbvt::convert_concatenation(const concatenation_exprt &expr)
   const exprt::operandst &operands=expr.operands();
 
   DATA_INVARIANT(
-    !operands.empty(), "concatentation shall have at least one operand");
+    !operands.empty(), "concatenation shall have at least one operand");
 
   std::size_t offset=width;
   bvt bv;
@@ -30,7 +30,7 @@ bvt boolbvt::convert_concatenation(const concatenation_exprt &expr)
 
     INVARIANT(
       op.size() <= offset,
-      "concatentation operand must fit into the result bitvector");
+      "concatenation operand must fit into the result bitvector");
 
     offset-=op.size();
 
@@ -41,7 +41,7 @@ bvt boolbvt::convert_concatenation(const concatenation_exprt &expr)
   INVARIANT(
     offset == 0,
     "all bits in the result bitvector must have been filled up by the "
-    "concatentation operands");
+    "concatenation operands");
 
   return bv;
 }
diff --git a/src/solvers/sat/external_sat.cpp b/src/solvers/sat/external_sat.cpp
index 266feb2ecc8..17482139a54 100644
--- a/src/solvers/sat/external_sat.cpp
+++ b/src/solvers/sat/external_sat.cpp
@@ -85,7 +85,7 @@ external_satt::resultt external_satt::parse_result(std::string solver_output)
       if(parts.size() < 2)
       {
         log.error() << "external SAT solver has provided an unexpected "
-                       "response in results.\nUnexpected reponse: "
+                       "response in results.\nUnexpected response: "
                     << line << messaget::eom;
         return resultt::P_ERROR;
       }