diff --git a/src/bin/sail.ml b/src/bin/sail.ml
index e559ff6cb..25ba61628 100644
--- a/src/bin/sail.ml
+++ b/src/bin/sail.ml
@@ -256,7 +256,7 @@ let rec options =
       ("-fmt", Arg.Set opt_format, " format input source code");
       ( "-fmt_backup",
         Arg.String (fun suffix -> opt_format_backup := Some suffix),
-        "<suffix> create backups of formated files as 'file.suffix'"
+        "<suffix> create backups of formatted files as 'file.suffix'"
       );
       ("-fmt_only", Arg.String (fun file -> opt_format_only := file :: !opt_format_only), "<file> format only this file");
       ( "-fmt_skip",
diff --git a/src/lib/constant_fold.ml b/src/lib/constant_fold.ml
index 6cfd62dae..11bfa51d0 100644
--- a/src/lib/constant_fold.ml
+++ b/src/lib/constant_fold.ml
@@ -125,7 +125,7 @@ let safe_primops =
    when f is in the list of identifiers to be mapped to unit. The
    advantage of doing it like this is if x, y, and z are
    computationally expensive then we remove them also. String
-   concatentation is very expensive at runtime so this is something we
+   concatenation is very expensive at runtime so this is something we
    really want when cutting out tracing features. Obviously it's
    important that they don't have any meaningful side effects, and
    that f does actually have type unit.
diff --git a/src/lib/interpreter.ml b/src/lib/interpreter.ml
index 203527a41..ddac641fd 100644
--- a/src/lib/interpreter.ml
+++ b/src/lib/interpreter.ml
@@ -684,7 +684,7 @@ and pattern_match env (P_aux (p_aux, (l, _))) value =
           end
         | _ ->
             failwith
-              ("Bad vector annotation for vector concatentation pattern " ^ string_of_typ (Type_check.typ_of_pat pat))
+              ("Bad vector annotation for vector concatenation pattern " ^ string_of_typ (Type_check.typ_of_pat pat))
       end
   | P_tuple [pat] -> pattern_match env pat value
   | P_tuple pats | P_list pats ->
diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml
index d3e05f4a4..c6817102e 100644
--- a/src/lib/type_check.ml
+++ b/src/lib/type_check.ml
@@ -3358,7 +3358,7 @@ and infer_lexp env (LE_aux (lexp_aux, (l, uannot)) as lexp) =
         | Typ_app (id, [A_aux (A_nexp len, _); A_aux (A_typ elem_typ, _)]) when Id.compare id (mk_id "vector") = 0 ->
             typ_equality l env elem_typ first_elem_typ;
             nsum acc len
-        | _ -> typ_error l "Vector concatentation l-expression must only contain vector types of the same order"
+        | _ -> typ_error l "Vector concatenation l-expression must only contain vector types of the same order"
       in
       let sum_bitvector_lengths acc (Typ_aux (v_typ_aux, _)) =
         match v_typ_aux with
@@ -3378,7 +3378,7 @@ and infer_lexp env (LE_aux (lexp_aux, (l, uannot)) as lexp) =
           annot_lexp (LE_vector_concat (inferred_v_lexp :: inferred_v_lexps)) (bitvector_typ (nexp_simp len))
       | _ ->
           typ_error l
-            ("Vector concatentation l-expression must only contain bitvector or vector types, found "
+            ("Vector concatenation l-expression must only contain bitvector or vector types, found "
            ^ string_of_typ v_typ
             )
     end
diff --git a/src/sail_doc_backend/wavedrom.ml b/src/sail_doc_backend/wavedrom.ml
index 06a00537d..725169c33 100644
--- a/src/sail_doc_backend/wavedrom.ml
+++ b/src/sail_doc_backend/wavedrom.ml
@@ -53,7 +53,7 @@ module Big_int = Nat_big_num
 
 exception Invalid_wavedrom
 
-(* Process the $[wavedrom] attribute for a vector concatentation pattern of length n *)
+(* Process the $[wavedrom] attribute for a vector concatenation pattern of length n *)
 let process_attr_arg = function
   | None -> []
   | Some arg ->