diff --git a/docs/src/cheat-sheets.md b/docs/src/cheat-sheets.md
index 11b1ab456e537..23b675b29ad7b 100644
--- a/docs/src/cheat-sheets.md
+++ b/docs/src/cheat-sheets.md
@@ -1,7 +1,7 @@
 # Command cheat sheets
 
 Development work in the Kani project depends on multiple tools. Regardless of
-your familiriaty with the project, the commands below may be useful for
+your familiarity with the project, the commands below may be useful for
 development purposes.
 
 ## Kani
diff --git a/docs/src/rust-feature-support/unstable.md b/docs/src/rust-feature-support/unstable.md
index 0372ddea31a63..6a317198b16b1 100644
--- a/docs/src/rust-feature-support/unstable.md
+++ b/docs/src/rust-feature-support/unstable.md
@@ -3,7 +3,7 @@
 In general, unstable Rust features are out of scope and any support
 for them available in Kani should be considered unstable as well.
 
-The following are exampels of unstable features that are not supported
+The following are examples of unstable features that are not supported
 in Kani:
  * Generators
  * C-variadics
diff --git a/docs/src/tutorial/arbitrary-variables/src/inventory.rs b/docs/src/tutorial/arbitrary-variables/src/inventory.rs
index bbd3f104fa1c2..bbccff150db75 100644
--- a/docs/src/tutorial/arbitrary-variables/src/inventory.rs
+++ b/docs/src/tutorial/arbitrary-variables/src/inventory.rs
@@ -54,7 +54,7 @@ mod verification {
         let quantity: NonZeroU32 = unsafe { kani::any_raw() };
 
         // The assert bellow would fail if we comment it out.
-        // assert!(id.get() != 0, "NonZeroU32 is internally a u32 but it should never be 0.");
+        // assert!(quantity.get() != 0, "NonZeroU32 is internally a u32 but it should never be 0.");
 
         // Update the inventory and check the result.
         inventory.update(id.clone(), quantity);
diff --git a/docs/src/undefined-behaviour.md b/docs/src/undefined-behaviour.md
index 147ddb717dde8..bc4b66653b202 100644
--- a/docs/src/undefined-behaviour.md
+++ b/docs/src/undefined-behaviour.md
@@ -20,14 +20,14 @@ Rust’s [definition of UB](https://doc.rust-lang.org/reference/behavior-conside
 
 
 Given the lack of a formal semantics for UB, and given Kani's focus on memory safety, there are classes of UB which Kani does not detect.
-A non-exhaustive list of these, based on the the non-exhaustive list from the [Rust documentation](https://doc.rust-lang.org/reference/behavior-considered-undefined.html), is:
+A non-exhaustive list of these, based on the non-exhaustive list from the [Rust documentation](https://doc.rust-lang.org/reference/behavior-considered-undefined.html), is:
 
 * Data races. 
     * Kani focuses on sequential code.
 * Breaking the pointer aliasing rules (http://llvm.org/docs/LangRef.html#pointer-aliasing-rules). 
-    * Kani can detect if misuse of pointers causes memory safety or assertion violations, but does not not track reference lifetimes.
+    * Kani can detect if misuse of pointers causes memory safety or assertion violations, but does not track reference lifetimes.
 * Mutating immutable data.
-    * Kani can detect if modification of immutable data causes memory safety or assertion violations, but does not not track reference lifetimes.
+    * Kani can detect if modification of immutable data causes memory safety or assertion violations, but does not track reference lifetimes.
 * Invoking undefined behavior via compiler intrinsics.
     * Kani makes a best effort attempt to check the preconditions of compiler intrinsics, but does not guarantee to do so in all cases.
 * Executing code compiled with platform features that the current platform does not support (see [target_feature](https://doc.rust-lang.org/reference/attributes/codegen.html#the-target_feature-attribute)).
@@ -44,6 +44,5 @@ Kani makes a best-effort attempt to detect some cases of UB:
     * Kani can detect invalid dereferences, but may not detect them in [place expression context](https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions).
 * Invoking undefined behavior via compiler intrinsics.
     * See [current support for compiler intrinsics](./rust-feature-support/intrinsics.md).
-* Producing an invalid value, even in private fields and locals. 
+* Producing an invalid value, even in private fields and locals.
     * Kani provides a [mechanism](./tutorial-nondeterministic-variables.md#safe-nondeterministic-variables-for-custom-types) `is_valid()` which users can use to check validity of objects, but it does not currently apply to all types.
-