diff --git a/rmc-docs/README.md b/rmc-docs/README.md
index 2ba0528e9ffd..2b21255dd43d 100644
--- a/rmc-docs/README.md
+++ b/rmc-docs/README.md
@@ -8,3 +8,15 @@ ssh -t -L 3000:127.0.0.1:3000 rmc-host 'cd rmc/rmc-docs/ && ./mdbook serve'
 
 This command will connect to `rmc-host` where it assumes RMC is checked out in `rmc/` and the documentation has been built once successfully.
 It will automatically detect changes to the docs and rebuild, allowing you to quickly refresh in your local browser when you visit: `http://127.0.0.1:3000/`
+
+## Documentation tests
+
+The code in `src/tutorial/` is tested with `compiletest`.
+This means each file should be buildable independently (i.e. you can run `rmc` on each `.rs` file).
+It also means the necessary `rmc-` flag-comments must appear in each file.
+
+To run just these tests, return to the RMC root directory and run:
+
+```
+./x.py test -i --stage 1 rmc-docs
+```
diff --git a/rmc-docs/build-docs.sh b/rmc-docs/build-docs.sh
index 93a9fa869d4c..4422dde2bf09 100755
--- a/rmc-docs/build-docs.sh
+++ b/rmc-docs/build-docs.sh
@@ -42,6 +42,9 @@ mkdir -p book
 ./mdbook build
 touch book/.nojekyll
 
-# TODO: Test all the code examples from our documentation
+# Testing of the code in the documentation is done via the usual
+# ./scripts/rmc-regression.sh script. A note on running just the
+# doc tests is in README.md. We don't run them here because
+# that would cause CI to run these tests twice.
 
 echo "Finished documentation build successfully."
diff --git a/rmc-docs/src/dev-documentation.md b/rmc-docs/src/dev-documentation.md
index 6084ac9af9da..74e573172a89 100644
--- a/rmc-docs/src/dev-documentation.md
+++ b/rmc-docs/src/dev-documentation.md
@@ -21,7 +21,7 @@
 ```
 ```bash
 # Test suite run (to run a specific suite from src/test/, just remove the others)
-./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc
+./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc rmc-docs
 ```
 ```bash
 # Dashboard run
diff --git a/rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs b/rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs
index d9da2e2f8cbc..9ec80f040fa4 100644
--- a/rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs
+++ b/rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // ANCHOR: code
 /// Wrap "too-large" indexes back into a valid range for the array
diff --git a/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs b/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs
index 44331863f607..2542810a788b 100644
--- a/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs
+++ b/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // ANCHOR: code
 fn find_midpoint(low: u32, high: u32) -> u32 {
diff --git a/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs b/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs
index b45bc50c8f7b..ae754004d16a 100644
--- a/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs
+++ b/rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // ANCHOR: code
 fn simple_addition(a: u32, b: u32) -> u32 {
diff --git a/rmc-docs/src/tutorial/loops-unwinding/src/lib.rs b/rmc-docs/src/tutorial/loops-unwinding/src/lib.rs
index 3afe0dca1bde..cc1d210bf860 100644
--- a/rmc-docs/src/tutorial/loops-unwinding/src/lib.rs
+++ b/rmc-docs/src/tutorial/loops-unwinding/src/lib.rs
@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-flags: --cbmc-args --unwind 11
+// rmc-verify-fail
 
 // ANCHOR: code
 fn initialize_prefix(length: usize, buffer: &mut [u8]) {
diff --git a/rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs b/rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs
index 776ff52b00c5..4894b8c423cb 100644
--- a/rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs
+++ b/rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs
@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // ANCHOR: code
 fn estimate_size(x: u32) -> u32 {
diff --git a/scripts/rmc-regression.sh b/scripts/rmc-regression.sh
index ebe91b776505..b2f4dadba83e 100755
--- a/scripts/rmc-regression.sh
+++ b/scripts/rmc-regression.sh
@@ -25,7 +25,7 @@ check-cbmc-viewer-version.py --major 2 --minor 5
 ./scripts/setup/build_rmc_lib.sh
 
 # Standalone rmc tests, expected tests, and cargo tests
-./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc
+./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc rmc-docs
 ./x.py test -i --stage 0 compiler/cbmc
 
 # Check codegen for the standard library
diff --git a/src/bootstrap/builder.rs b/src/bootstrap/builder.rs
index e6097089ab68..1cd2d750c985 100644
--- a/src/bootstrap/builder.rs
+++ b/src/bootstrap/builder.rs
@@ -473,6 +473,7 @@ impl<'a> Builder<'a> {
                 test::Expected,
                 test::Dashboard,
                 test::Stub,
+                test::RmcDocs,
                 // Run run-make last, since these won't pass without make on Windows
                 test::RunMake,
             ),
diff --git a/src/bootstrap/test.rs b/src/bootstrap/test.rs
index b14d0031b828..a832dc385e5f 100644
--- a/src/bootstrap/test.rs
+++ b/src/bootstrap/test.rs
@@ -1229,6 +1229,8 @@ default_test!(Expected { path: "src/test/expected", mode: "expected", suite: "ex
 
 default_test!(Dashboard { path: "src/test/dashboard", mode: "rmc", suite: "dashboard" });
 
+default_test!(RmcDocs { path: "src/test/rmc-docs", mode: "rmc", suite: "rmc-docs" });
+
 default_test!(Stub { path: "src/test/stub-tests", mode: "stub-tests", suite: "stub-tests" });
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
diff --git a/src/test/rmc-docs b/src/test/rmc-docs
new file mode 120000
index 000000000000..ae7201c2a17b
--- /dev/null
+++ b/src/test/rmc-docs
@@ -0,0 +1 @@
+../../rmc-docs/src/tutorial
\ No newline at end of file