diff --git a/docs/src/adr/018adr-inlining.md b/docs/src/adr/018adr-inlining.md
index 35f59865ce..c1f7b2ff17 100644
--- a/docs/src/adr/018adr-inlining.md
+++ b/docs/src/adr/018adr-inlining.md
@@ -122,7 +122,7 @@ Knowing that we must perform (1) at some point, what remains is to decide whethe
 Additionally, if we do isolate inlining to a separate pass, we can choose whether or not to perform (2).
 
 1. Perform no inlining in preprocessing and inline only as needed in the rewriting rules.
-    - Pros: Spec intermediate output remains small, since inlining increases the size of the specificaiton
+    - Pros: Spec intermediate output remains small, since inlining increases the size of the specification
     - Cons: 
       - Fewer optimizations can be applied, as some are only applicable to the syntactic forms obtained after inlining (e.g. `ConstSimplifier` can simplify `IF TRUE THEN a ELSE b`, but not `IF p THEN a ELSE b`)
       - Rewriting rules for different encodings have to deal with operators in their generality.
diff --git a/docs/src/tutorials/trail-tips.md b/docs/src/tutorials/trail-tips.md
index 23754f059d..ac54270b4c 100644
--- a/docs/src/tutorials/trail-tips.md
+++ b/docs/src/tutorials/trail-tips.md
@@ -55,7 +55,7 @@ invariant](../apalache/principles/invariants.md#action-invariants):
 ```
 
 Our version of `NextFast` is quite concise and it uses the good parts of
-TLA+. However, new TLA+ users would probably write it differenty. Below you
+TLA+. However, new TLA+ users would probably write it differently. Below you
 can see the version that is more likely to be written by a specification
 writer who has good experience in software engineering: