diff --git a/.github/workflows/typos.yml b/.github/workflows/typos.yml
new file mode 100644
index 000000000..c7828a2e2
--- /dev/null
+++ b/.github/workflows/typos.yml
@@ -0,0 +1,35 @@
+name: Typos
+
+permissions:
+  contents: read
+
+on:
+  pull_request:
+  push:
+
+env:
+  TYPOS_VER: v1.29.1
+  TYPOS_PLATFORM: x86_64-unknown-linux-musl
+  CLICOLOR: 1
+
+jobs:
+  typos:
+    defaults:
+      run:
+        shell: bash
+    runs-on: ubuntu-latest
+
+    steps:
+
+    - uses: actions/checkout@v4
+
+    - run: |
+        wget -q https://github.com/crate-ci/typos/releases/download/${{ env.TYPOS_VER }}/typos-${{ env.TYPOS_VER }}-${{ env.TYPOS_PLATFORM }}.tar.gz
+        tar -xf typos-${{ env.TYPOS_VER }}-${{ env.TYPOS_PLATFORM }}.tar.gz --one-top-level=typos-${{ env.TYPOS_VER }}
+        mkdir -p "$HOME/.local/bin"
+        mv typos-${{ env.TYPOS_VER }} "$HOME/.local/bin/typos-${{ env.TYPOS_VER }}"
+        chmod +x "$HOME/.local/bin/typos-${{ env.TYPOS_VER }}/typos"
+        echo "$HOME/.local/bin/typos-${{ env.TYPOS_VER }}" >> $GITHUB_PATH
+
+    - run: make markdown-typos
+    - run: make hs-typos
diff --git a/.typos.toml b/.typos.toml
new file mode 100644
index 000000000..a4b26e993
--- /dev/null
+++ b/.typos.toml
@@ -0,0 +1,16 @@
+[type.hs]
+extend-glob = []
+extend-ignore-identifiers-re = []
+extend-ignore-words-re = []
+extend-ignore-re = []
+
+[type.hs.extend-identifiers]
+sIy = "sIy"
+vIy = "vIy"
+tre = "tre"
+inh = "inh"
+TypeLits = "TypeLits"
+fof = "fof"
+
+[type.hs.extend-words]
+alse = "alse"
diff --git a/Makefile b/Makefile
new file mode 100644
index 000000000..ffd2395a7
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,36 @@
+all: help-banner help
+
+PHONY: help
+help: ## Show the commented targets.
+	@grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) | \
+	sort | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-30s\033[0m %s\n", $$1, $$2}'
+
+PHONY: help-banner
+help-banner: ## Show the help banner.
+	@echo "===================================================================="
+	@echo "§ all                  make with no arguments also shows this banner"
+	@echo "§ help                 make help will list targets with descriptions"
+	@echo "===================================================================="
+
+.PHONY: typos-install
+typos-install: ## Install typos-cli for typos target using cargo.
+	cargo install typos-cli
+
+GREP_EXCLUDE := grep -v -E 'dist-'
+FIND_NAMED := find . -type f -name
+
+.PHONY: markdown-typos
+markdown-typos: ## Find typos in Markdown .md files.
+	$(FIND_NAMED) '*.md' | $(GREP_EXCLUDE) | xargs typos
+
+.PHONY: markdown-fix-typos
+markdown-fix-typos: ## Fix typos in Markdown .md files.
+	$(FIND_NAMED) '*.md' | $(GREP_EXCLUDE) | xargs typos --write-changes
+
+.PHONY: hs-typos
+hs-typos: ## Find typos in Haskell .hs files.
+	$(FIND_NAMED) '*.hs' | $(GREP_EXCLUDE) | xargs typos
+
+.PHONY: hs-fix-typos
+hs-fix-typos: ## Fix typos in Haskell .hs files.
+	$(FIND_NAMED) '*.hs' | $(GREP_EXCLUDE) | xargs typos --write-changes
diff --git a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
index ce822e558..a06c4d618 100644
--- a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs
@@ -267,7 +267,7 @@ mkStep cSettings streams triggers exts =
     --
     -- We create temporary variables because:
     --
-    -- 1. We want to pass structs by reference intead of by value. To this end,
+    -- 1. We want to pass structs by reference instead of by value. To this end,
     --    we use C's & operator to obtain a reference to a temporary variable
     --    of a struct type and pass that to the handler function.
     --
diff --git a/copilot-c99/src/Copilot/Compile/C99/Compile.hs b/copilot-c99/src/Copilot/Compile/C99/Compile.hs
index 1467af403..d7f051e96 100644
--- a/copilot-c99/src/Copilot/Compile/C99/Compile.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/Compile.hs
@@ -283,7 +283,7 @@ typeTypes ty = case ty of
   _         -> [UType ty]
 
 -- | Collect all expression of a list of streams and triggers and wrap them
--- into an UEXpr.
+-- into an UExpr.
 gatherExprs :: [Stream] -> [Trigger] -> [UExpr]
 gatherExprs streams triggers =  map streamUExpr streams
                              ++ concatMap triggerUExpr triggers
diff --git a/copilot-c99/tests/Test/Copilot/Compile/C99.hs b/copilot-c99/tests/Test/Copilot/Compile/C99.hs
index 60276e870..78b5fc66d 100644
--- a/copilot-c99/tests/Test/Copilot/Compile/C99.hs
+++ b/copilot-c99/tests/Test/Copilot/Compile/C99.hs
@@ -240,9 +240,9 @@ arbitraryOpBoolBits =
     ]
 
 -- | Generator of functions that take Nums and produce booleans.
-arbitaryOpBoolOrdEqNum :: (Typed a, Eq a, Ord a, Num a)
+arbitraryOpBoolOrdEqNum :: (Typed a, Eq a, Ord a, Num a)
                        => Gen (Fun a Bool, [a] -> [Bool])
-arbitaryOpBoolOrdEqNum =
+arbitraryOpBoolOrdEqNum =
   frequency
     [ (1, funCompose2 <$> arbitraryOp2Eq  <*> arbitraryOpNum <*> arbitraryOpNum)
     , (1, funCompose2 <$> arbitraryOp2Ord <*> arbitraryOpNum <*> arbitraryOpNum)
@@ -379,7 +379,7 @@ arbitraryOpIntegralBool = frequency
 
     -- we need to use +1 because certain operations overflow the number
   , (2, mkTestCase1
-          arbitaryOpBoolOrdEqNum
+          arbitraryOpBoolOrdEqNum
           (chooseBoundedIntegral (minBound + 1, maxBound)))
   ]
 
diff --git a/copilot-interpreter/src/Copilot/Interpret/Eval.hs b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
index 462b5853e..6a142c7af 100644
--- a/copilot-interpreter/src/Copilot/Interpret/Eval.hs
+++ b/copilot-interpreter/src/Copilot/Interpret/Eval.hs
@@ -106,7 +106,7 @@ data ExecTrace = ExecTrace
 
 -- We could write this in a beautiful lazy style like above, but that creates a
 -- space leak in the interpreter that is hard to fix while maintaining laziness.
--- We take a more brute-force appraoch below.
+-- We take a more brute-force approach below.
 
 -- | Evaluate a specification for a number of steps.
 eval :: ShowType   -- ^ Show booleans as @0@\/@1@ (C) or @True@\/@False@
diff --git a/copilot-interpreter/src/Copilot/Interpret/Render.hs b/copilot-interpreter/src/Copilot/Interpret/Render.hs
index 3b6241a8c..82a10526d 100644
--- a/copilot-interpreter/src/Copilot/Interpret/Render.hs
+++ b/copilot-interpreter/src/Copilot/Interpret/Render.hs
@@ -16,7 +16,7 @@ import Text.PrettyPrint
 
 import Prelude hiding ((<>))
 
--- | Render an execution trace as a table, formatted to faciliate readability.
+-- | Render an execution trace as a table, formatted to facilitate readability.
 renderAsTable :: ExecTrace -> String
 renderAsTable
   ExecTrace
@@ -112,7 +112,7 @@ pad :: Int -> Int -> a -> [a] -> [a]
 pad lx max b ls = ls ++ replicate (max - lx) b
 
 -- | Pad a list of strings on the right with spaces.
-pad' :: Int      -- ^ Mininum number of spaces to add
+pad' :: Int      -- ^ Minimum number of spaces to add
      -> Int      -- ^ Maximum number of spaces to add
      -> [[Doc]]  -- ^ List of documents to pad
      -> [[Doc]]
diff --git a/copilot-language/src/Copilot/Language/Analyze.hs b/copilot-language/src/Copilot/Language/Analyze.hs
index 04de14ed4..379c40b41 100644
--- a/copilot-language/src/Copilot/Language/Analyze.hs
+++ b/copilot-language/src/Copilot/Language/Analyze.hs
@@ -60,13 +60,13 @@ instance Show AnalyzeException where
   show (DifferentTypes name) = badUsage $
     "The external symbol \'" ++ name ++ "\' has been declared to have two different types!"
   show (Redeclared name) = badUsage $
-    "The external symbol \'" ++ name ++ "\' has been redeclared to be a different symbol (e.g., a variable and an array, or a variable and a funciton symbol, etc.)."
+    "The external symbol \'" ++ name ++ "\' has been redeclared to be a different symbol (e.g., a variable and an array, or a variable and a function symbol, etc.)."
   show (BadNumberOfArgs name) = badUsage $
     "The function symbol \'" ++ name ++ "\' has been redeclared to have different number of arguments."
   show (BadFunctionArgType name) = badUsage $
     "The function symbol \'" ++ name ++ "\' has been redeclared to an argument with different types."
 
--- | 'Exception' instance so we can throw and catch 'AnalyzeExcetion's.
+-- | 'Exception' instance so we can throw and catch 'AnalyzeException's.
 instance Exception AnalyzeException
 
 -- | Max level of recursion supported. Any level above this constant
diff --git a/copilot-language/src/Copilot/Language/Operators/Integral.hs b/copilot-language/src/Copilot/Language/Operators/Integral.hs
index e4d052490..e95437c50 100644
--- a/copilot-language/src/Copilot/Language/Operators/Integral.hs
+++ b/copilot-language/src/Copilot/Language/Operators/Integral.hs
@@ -46,4 +46,4 @@ x `mod` y = Op2 (Core.Mod typeOf) x y
 (Const x) ^ (Const y)  = Const (x P.^ y)
 (Const 2) ^ y          = (Const 1) .<<. y
 x ^ (Const y)          = foldl' ((P.*)) (Const 1) (replicate (P.fromIntegral y) x)
-_ ^ _                  = Err.badUsage "in ^: in x ^ y, either x must be the constant 2, or y must be a constant.  (Do not confuse ^ with bitwise XOR (.^.) or with ** for exponentation of floats/doubles.)"
+_ ^ _                  = Err.badUsage "in ^: in x ^ y, either x must be the constant 2, or y must be a constant.  (Do not confuse ^ with bitwise XOR (.^.) or with ** for exponentiation of floats/doubles.)"
diff --git a/copilot-libraries/src/Copilot/Library/Statistics.hs b/copilot-libraries/src/Copilot/Library/Statistics.hs
index d6e0330b9..775cc6f32 100644
--- a/copilot-libraries/src/Copilot/Library/Statistics.hs
+++ b/copilot-libraries/src/Copilot/Library/Statistics.hs
@@ -32,7 +32,7 @@ min n s = nfoldl1 n smallest s
       smallest = \ x y -> mux ( x <= y ) x y
 
 -- | Mean value.  @n@ must not overflow
--- for word size @a@ for streams over which computation is peformed.
+-- for word size @a@ for streams over which computation is performed.
 mean :: ( Typed a, Eq a, Fractional a ) => Int -> Stream a -> Stream a
 mean n s = ( sum n s ) / ( fromIntegral n )
 
diff --git a/copilot-theorem/README.md b/copilot-theorem/README.md
index e16d7f1ea..41f5faa91 100644
--- a/copilot-theorem/README.md
+++ b/copilot-theorem/README.md
@@ -216,7 +216,7 @@ process* [7] and so we have no way to keep them.
 #### Types
 
 In these three formats, GADTs are used to statically ensure a part of the
-type-corectness of the specification, in the same spirit it is done in the
+type-correctness of the specification, in the same spirit it is done in the
 other Copilot libraries. *copilot-theorem* handles only three types which are
 `Integer`, `Real` and `Bool` and which are handled by the SMTLib standard.
 *copilot-theorem* works with *pure* reals and integers. Thus, it is unsafe in the
@@ -389,9 +389,9 @@ the model-checking techniques we are using.
 #### Limitations related to Copilot implementation
 
 The reification process used to build the `Core.Spec` object looses many
-informations about the structure of the original Copilot program. In fact, a
+information about the structure of the original Copilot program. In fact, a
 stream is kept in the reified program only if it is recursively defined.
-Otherwise, all its occurences will be inlined. Moreover, let's look at the
+Otherwise, all its occurrences will be inlined. Moreover, let's look at the
 `intCounter` function defined in the example `Grey.hs`:
 
 ```haskell
@@ -413,7 +413,7 @@ There are many problems with this:
 * It makes the inputs given to the SMT solvers larger and repetitive.
 
 We can't rewrite the Copilot reification process in order to avoid these
-inconvenients as these informations are lost by GHC itself before it occurs.
+inconvenients as these information are lost by GHC itself before it occurs.
 The only solution we can see would be to use *Template Haskell* to generate
 automatically some structural annotations, which might not be worth the dirt
 introduced.
@@ -423,7 +423,7 @@ introduced.
 ##### Limitations of the IC3 algorithm
 
 The IC3 algorithm was shown to be a very powerful tool for hardware
-certification. However, the problems encountered when verifying softwares are
+certification. However, the problems encountered when verifying software are
 much more complex. For now, very few non-inductive properties can be proved by
 *Kind2* when basic integer arithmetic is involved.
 
@@ -433,7 +433,7 @@ the inductiveness* (CTI) for a property, these techniques are used to find a
 lemma discarding it which is general enough so that all CTIs can be discarded
 in a finite number of steps.
 
-The lemmas found by the current version fo *Kind2* are often too weak. Some
+The lemmas found by the current version of *Kind2* are often too weak. Some
 suggestions to enhance this are presented in [1]. We hope some progress will be
 made in this area in a near future.
 
@@ -487,7 +487,7 @@ forAllCst l f = conj $ map (f . constant) l
 ```
 
 However, this solution isn't completely satisfying because the size of the
-property generated is proportionnal to the cardinal of `allowed`.
+property generated is proportional to the cardinal of `allowed`.
 
 #### Some scalability issues
 
@@ -517,7 +517,7 @@ in the Kind2 SMT solver.
 Counterexamples are not displayed with the Kind2 prover because Kind2 doesn't
 support XML output of counterexamples. If the last feature is provided, it
 should be easy to implement counterexamples displaying in *copilot-theorem*. For
-this, we recommend to keep some informations about *observers* in
+this, we recommend to keep some information about *observers* in
 `TransSys.Spec` and to add one variable per observer in the Kind2 output file.
 
 #### Bad handling of non-linear operators and external functions
@@ -576,12 +576,12 @@ complexity added. It's especially true at the time I write this in the sense
 that:
 
 * Each predicate introduced is used only one time (which is true because
-  copilot doesn't handle functions or parametrized streams like Lustre does and
+  copilot doesn't handle functions or parameterized streams like Lustre does and
   everything is inlined during the reification process).
 * A similar form of structure could be obtained from a flattened Kind2 native
   input file with some basic static analysis by producing a dependency graph
   between variables.
-* For now, the *Kind2* model-checker ignores these structure informations.
+* For now, the *Kind2* model-checker ignores these structure information.
 
 However, the current code offers some nice transformation tools (node merging,
 `Renaming` monad...) which could be useful if you intend to write a tool for
diff --git a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs
index 6851d46fa..5c3fb0ae7 100644
--- a/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs
+++ b/copilot-theorem/src/Copilot/Theorem/Kind2/PrettyPrint.hs
@@ -9,7 +9,7 @@ import Copilot.Theorem.Kind2.AST
 
 import Data.List (intercalate)
 
--- | A tree of expressions, in which the leafs are strings.
+-- | A tree of expressions, in which the leaves are strings.
 type SSExpr = SExpr String
 
 -- | Reserved keyword prime.
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Invariants.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Invariants.hs
index 3a41d615e..ebf566acd 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Invariants.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Invariants.hs
@@ -8,7 +8,7 @@ module Copilot.Theorem.TransSys.Invariants
   , prop
   ) where
 
--- | Type class for types with additional invariants or contraints.
+-- | Type class for types with additional invariants or constraints.
 class HasInvariants a where
 
   invariants :: a -> [(String, Bool)]
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
index d2a953387..92bf96334 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Spec.hs
@@ -74,11 +74,11 @@ data Node = Node
                                            --   its local name.
   , nodeConstrs       :: [Expr Bool] }
 
--- | Identifer of a variable in the local (within one node) namespace.
+-- | Identifier of a variable in the local (within one node) namespace.
 data Var      =  Var {varName :: String}
   deriving (Eq, Show, Ord)
 
--- | Identifer of a variable in the global namespace by specifying both a node
+-- | Identifier of a variable in the global namespace by specifying both a node
 -- name and a variable.
 data ExtVar   =  ExtVar {extVarNode :: NodeId, extVarLocalPart :: Var }
   deriving (Eq, Ord)
@@ -115,7 +115,7 @@ foldExpr f expr = f expr <> fargs
 foldUExpr :: (Monoid m) => (forall t . Expr t -> m) -> U Expr -> m
 foldUExpr f (U e) = foldExpr f e
 
--- | Apply an arbitrary transformation to the leafs of an expression.
+-- | Apply an arbitrary transformation to the leaves of an expression.
 transformExpr :: (forall a . Expr a -> Expr a) -> Expr t -> Expr t
 transformExpr f = tre
   where
@@ -126,7 +126,7 @@ transformExpr f = tre
     tre e                 = f e
 
 -- | The set of variables related to a node (union of the local variables and
--- the imported variables after deferencing them).
+-- the imported variables after dereferencing them).
 nodeVarsSet :: Node -> Set Var
 nodeVarsSet = liftA2 Set.union
   nodeLocalVarsSet
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
index 79edd2828..1a66704a6 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Transform.hs
@@ -266,10 +266,10 @@ complete spec =
                 -- To get readable names, we don't prefix variables
                 -- which come from merged nodes as they are already
                 -- decorated
-                let preferedName
+                let preferredName
                      | head ncNodeIdSep `elem` n' = v
                      | otherwise = n' `prefix` v
-                alias <- getFreshName [preferedName, n' `prefix` v]
+                alias <- getFreshName [preferredName, n' `prefix` v]
                 return $ Bimap.tryInsert alias ev acc
 
           foldM tryImport (nodeImportedVars n) toImportVars
diff --git a/copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs b/copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs
index e1408f044..eff4bcd83 100644
--- a/copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs
+++ b/copilot-theorem/src/Copilot/Theorem/TransSys/Type.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE GADTs                     #-}
 {-# LANGUAGE Safe                      #-}
 
--- | Types suported by the modular transition systems.
+-- | Types supported by the modular transition systems.
 module Copilot.Theorem.TransSys.Type
   ( Type (..)
   , U (..)
diff --git a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
index f6ced33b7..40ddc9b37 100644
--- a/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
+++ b/copilot-theorem/src/Copilot/Theorem/What4/Translate.hs
@@ -479,7 +479,7 @@ translateOp1 sym origExpr op xe = case (op, xe) of
       recip fiRepr e = do
         one <- fpLit fiRepr 1.0
         WFP.iFloatDiv @_ @fi sym fpRM one e
-  -- The argument should not cause the result to overflow or underlow
+  -- The argument should not cause the result to overflow or underflow
   (CE.Exp _, xe) -> liftIO $ fpSpecialOp WSF.Exp xe
   -- The argument should not be less than -0
   (CE.Sqrt _, xe) ->
diff --git a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs b/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs
index dbd98eb4a..7039e8a01 100644
--- a/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs
+++ b/copilot-theorem/tests/Test/Copilot/Theorem/What4.hs
@@ -69,7 +69,7 @@ testProveZ3False =
     spec :: Spec
     spec = propSpec propName $ Const typeOf False
 
--- | Test that Z3 is able to prove the following expresion valid:
+-- | Test that Z3 is able to prove the following expression valid:
 -- @
 --   for all (x :: Int8), constant x == constant x
 -- @
@@ -84,7 +84,7 @@ testProveZ3EqConst = forAll arbitrary $ \x ->
     spec x = propSpec propName $
       Op2 (Eq typeOf) (Const typeOf x) (Const typeOf x)
 
--- | Test that Z3 is able to prove the following expresion valid:
+-- | Test that Z3 is able to prove the following expression valid:
 -- @
 --   for all (s :: MyStruct),
 --   ((s ## testField =$ (+1)) # testField) == ((s # testField) + 1)
diff --git a/copilot/examples/Array.hs b/copilot/examples/Array.hs
index 7f43a21b1..3769ad860 100644
--- a/copilot/examples/Array.hs
+++ b/copilot/examples/Array.hs
@@ -3,7 +3,7 @@
 -- | This is a simple example for arrays. As a program, it does not make much
 -- sense, however it shows of the features of arrays nicely.
 
--- | Enable compiler extension for type-level data, necesary for the array
+-- | Enable compiler extension for type-level data, necessary for the array
 -- length.
 
 {-# LANGUAGE DataKinds        #-}
diff --git a/copilot/examples/Engine.hs b/copilot/examples/Engine.hs
index 1200170f9..d8e7bbea5 100644
--- a/copilot/examples/Engine.hs
+++ b/copilot/examples/Engine.hs
@@ -9,7 +9,7 @@ module Main where
 import Language.Copilot
 import qualified Prelude as P
 
--- If the majority of the engine temperature probes exeeds 250 degrees, then
+-- If the majority of the engine temperature probes exceeds 250 degrees, then
 -- the cooler is engaged and remains engaged until the majority of the engine
 -- temperature probes drop to 250 or below.  Otherwise, trigger an immediate
 -- shutdown of the engine.
diff --git a/copilot/examples/Voting.hs b/copilot/examples/Voting.hs
index d534fe2c7..aaf23e64f 100644
--- a/copilot/examples/Voting.hs
+++ b/copilot/examples/Voting.hs
@@ -10,7 +10,7 @@ import Language.Copilot
 
 vote :: Spec
 vote = do
-  -- majority selects element with the biggest occurance.
+  -- majority selects element with the biggest occurrence.
   trigger "maj"  true [arg maj]
 
   -- aMajority checks if the selected element has a majority.
diff --git a/copilot/examples/WCV.hs b/copilot/examples/WCV.hs
index 3ac016fb3..4636bacba 100644
--- a/copilot/examples/WCV.hs
+++ b/copilot/examples/WCV.hs
@@ -1,6 +1,6 @@
 -- | This example shows an implementation of the Well-Clear Violation
 -- algorithm, it follows the implementation described in 'Analysis of
--- Well-Clear Bounday Models for the Integration of UAS in the NAS',
+-- Well-Clear Boundary Models for the Integration of UAS in the NAS',
 -- https://ntrs.nasa.gov/citations/20140010078.
 
 {-# LANGUAGE DataKinds        #-}