diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
index 61d579225f82c..15b0f6f0da3a9 100644
--- a/doc/src/SUMMARY.md
+++ b/doc/src/SUMMARY.md
@@ -17,4 +17,4 @@
   - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
   - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
   - [Inductive data type](./challenges/0005-linked-list.md)
-  - [Memory safety of the `btree::node` module](./challenges/0006-btree-node.md)
+  - [Memory safety of BTreeMap's `btree::node` module](./challenges/0006-btree-node.md)
diff --git a/doc/src/challenges/0006-btree-node.md b/doc/src/challenges/0006-btree-node.md
index 39b8685ef2e08..6f252e9bd4bfa 100644
--- a/doc/src/challenges/0006-btree-node.md
+++ b/doc/src/challenges/0006-btree-node.md
@@ -1,4 +1,4 @@
-# Challenge 4: Towards the memory safety of BTreeMap
+# Challenge 4: Memory safety of BTreeMap's `btree::node` module
 
 - **Status:** Open
 - **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25)
@@ -59,7 +59,7 @@ The verification must be unbounded for functions that are recursive or that cont
 All proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
 
 * Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
-* Reading from uninitialized memory except for padding or unions.
+* Reading from uninitialized memory.
 * Mutating immutable bytes.
 * Producing an invalid value