diff --git a/.gitmodules b/.gitmodules
index e5c13b8f0e..7b798103ff 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -49,3 +49,6 @@
 [submodule "deps/lmdb"]
 	path = deps/lmdb
 	url = https://github.com/GaloisInc/lmdb.git
+[submodule "deps/mir-json"]
+	path = deps/mir-json
+	url = https://github.com/GaloisInc/mir-json.git
diff --git a/README.md b/README.md
index 18bfd91120..d64bcef920 100644
--- a/README.md
+++ b/README.md
@@ -88,6 +88,26 @@ will be possible for all language constructs. There are various
 instructions that are not supported during verification. However,
 any failure during `llvm_load_module` should be considered a bug.
 
+## Notes on Rust
+
+SAW has experimental support for analyzing Rust programs. To do so, one must
+compile Rust code using [`mir-json`](https://github.com/GaloisInc/mir-json), a
+tool which compiles Rust code to a machine-readable, JSON-based format.
+Note that:
+
+* Each version of SAW understands the JSON output of a particular version of
+  `mir-json`, so make sure that you build the version `mir-json` that is
+  included in the `mir-json` submodule (located in `deps/mir-json`).
+* Moreover, SAW requires slightly modified versions of the Rust standard
+  libraries that are suited to verification purposes. SAW consults the value
+  of the `SAW_RUST_LIBRARY_PATH` environment variable to determine where to
+  look for these modified standard libraries.
+
+For complete instructions on how to install `mir-json`, the modified Rust
+standard libraries, and how to defined the `SAW_RUST_LIBRARY_PATH` environment
+variable, follow the instructions
+[here](https://github.com/GaloisInc/mir-json#installation-instructions).
+
 ## Notes on Windows
 
 If you have trouble loading the SAW REPL on Windows, try invoking it
diff --git a/deps/mir-json b/deps/mir-json
new file mode 160000
index 0000000000..131980a17b
--- /dev/null
+++ b/deps/mir-json
@@ -0,0 +1 @@
+Subproject commit 131980a17bb27c2c3c616a1e8bfb4253a528c328
diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index 7a1cf0baa6..c98e7b517a 100644
--- a/doc/manual/manual.md
+++ b/doc/manual/manual.md
@@ -1812,7 +1812,54 @@ In order to verify Rust code, SAW analyzes Rust's MIR (mid-level intermediate
 representation) language. In particular, SAW analyzes a particular form of MIR
 that the [`mir-json`](https://github.com/GaloisInc/mir-json) tool produces. You
 will need to intall `mir-json` and run it on Rust code in order to produce MIR
-JSON files that SAW can load (see [this section](#loading-mir)).
+JSON files that SAW can load (see [this section](#loading-mir)). You will also
+need to use `mir-json` to build custom versions of the Rust standard libraries
+that are more suited to verification purposes.
+
+If you are working from a checkout of the `saw-script` repo, you can install
+the `mir-json` tool and the custom Rust standard libraries by performing the
+following steps:
+
+1. Clone the [`crucible`](https://github.com/GaloisInc/crucible) and `mir-json`
+   submodules like so:
+
+   ```
+   $ git submodule update deps/crucible deps/mir-json
+   ```
+
+2. Navigate to the `mir-json` submodule:
+
+   ```
+   $ cd deps/mir-json
+   ```
+
+3. Follow the instructions laid out in the [`mir-json` installation
+   instructions](https://github.com/GaloisInc/mir-json#installation-instructions)
+   in order to install `mir-json`.
+
+4. Navigate to the
+   [`crux-mir`](https://github.com/GaloisInc/crucible/tree/master/crux-mir)
+   subdirectory of the `crucible` submodule:
+
+   ```
+   $ cd ../crucible/crux-mir/
+   ```
+
+5. Run the `translate_libs.sh` script:
+
+   ```
+   $ ./translate_libs.sh
+   ```
+
+   This will compile the custom versions of the Rust standard libraries using
+   `mir-json`, placing the results under the `rlibs` subdirectory.
+
+6. Finally, define a `SAW_RUST_LIBRARY_PATH` environment variable that points
+   to the newly created `rlibs` subdirectory:
+
+   ```
+   $ export SAW_RUST_LIBRARY_PATH=<...>/crucible/crux-mir/rlibs
+   ```
 
 For `cargo`-based projects, `mir-json` provides a `cargo` subcommand called
 `cargo saw-build` that builds a JSON file suitable for use with SAW. `cargo
@@ -1820,7 +1867,7 @@ saw-build` integrates directly with `cargo`, so you can pass flags to it like
 any other `cargo` subcommand. For example:
 
 ```
-$ export SAW_RUST_LIBRARY_PATH=<...>
+# Make sure that SAW_RUST_LIBRARY_PATH is defined, as described above
 $ cargo saw-build <other cargo flags>
 <snip>
 linking 11 mir files into <...>/example-364cf2df365c7055.linked-mir.json
@@ -1840,7 +1887,7 @@ Note that:
 `rustc` accepts. For example:
 
 ```
-$ export SAW_RUST_LIBRARY_PATH=<...>
+# Make sure that SAW_RUST_LIBRARY_PATH is defined, as described above
 $ saw-rustc example.rs <other rustc flags>
 <snip>
 linking 11 mir files into <...>/example.linked-mir.json
diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf
index 74ffc233af..3f088d6e6a 100644
Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ