diff --git a/.github/ci.sh b/.github/ci.sh
index 6d86bb867d..e549c98acf 100755
--- a/.github/ci.sh
+++ b/.github/ci.sh
@@ -2,6 +2,7 @@
 set -Eeuxo pipefail
 
 [[ "$RUNNER_OS" == 'Windows' ]] && IS_WIN=true || IS_WIN=false
+[[ "$RUNNER_OS" == 'Linux' ]] && IS_LINUX=true || IS_LINUX=false
 BIN=$(pwd)/bin
 EXT=""
 $IS_WIN && EXT=".exe"
@@ -93,6 +94,9 @@ bundle_files() {
   cp LICENSE README.md dist/
   $IS_WIN || chmod +x dist/bin/*
 
+  if $IS_LINUX; then
+    cp -r deps/crucible/crux-mir/rlibs dist/lib
+  fi
   (cd deps/cryptol-specs && git archive --prefix=cryptol-specs/ --format=tar HEAD) | (cd dist/deps && tar x)
   cp doc/extcore.md dist/doc
   cp doc/tutorial/sawScriptTutorial.pdf dist/doc/tutorial.pdf
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 3fd05777f7..2053d3f720 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -19,6 +19,12 @@ env:
   CACHE_VERSION: 1
   DISABLED_TESTS: "test0000 test_FNV_a1_rev test0010_jss_cnf_exp test0039_rust test_boilerplate test_external_abc"
 
+  # Keep this in sync with the mir-json version documented in
+  # deps/mir-json/README.md.
+  RUST_TOOLCHAIN_VERSION: "nightly-2020-03-22"
+  # Work around https://github.com/rust-lang/cargo/issues/10303
+  CARGO_NET_GIT_FETCH_WITH_CLI: true
+
   # Solver package snapshot date - also update in the following locations:
   # ./saw/Dockerfile
   # ./saw-remote-api/Dockerfile
@@ -119,6 +125,22 @@ jobs:
           cabal user-config update -a "extra-include-dirs: \"\""
           cabal user-config update -a "extra-lib-dirs: \"\""
 
+      - name: Install Rust toolchain
+        uses: actions-rs/toolchain@v1
+        # For now, we only run Rust-related steps on Linux. mir-json does not
+        # currently support Windows, and mir-json is currently broken on macOS
+        # due to https://github.com/GaloisInc/mir-json/issues/31.
+        if: runner.os == 'Linux'
+        with:
+          toolchain: ${{ env.RUST_TOOLCHAIN_VERSION }}
+          override: true
+          components: rustc-dev
+
+      - name: Install mir-json
+        shell: bash
+        if: runner.os == 'Linux'
+        run: cd deps/mir-json && cargo install --locked --force
+
       - shell: bash
         run: .github/ci.sh install_system_deps
         env:
@@ -146,6 +168,11 @@ jobs:
       - shell: bash
         run: .github/ci.sh build
 
+      - name: Translate Rust standard libraries with mir-json
+        shell: bash
+        if: runner.os == 'Linux'
+        run: cd deps/crucible/crux-mir && bash ./translate_libs.sh
+
       - shell: bash
         env:
           RELEASE: ${{ needs.config.outputs.release }}
diff --git a/.gitmodules b/.gitmodules
index 926212c99c..941a80948a 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -46,3 +46,6 @@
 [submodule "deps/language-sally"]
 	path = deps/language-sally
 	url = https://github.com/GaloisInc/language-sally
+[submodule "deps/mir-json"]
+	path = deps/mir-json
+	url = https://github.com/GaloisInc/mir-json
diff --git a/deps/mir-json b/deps/mir-json
new file mode 160000
index 0000000000..3a621e1023
--- /dev/null
+++ b/deps/mir-json
@@ -0,0 +1 @@
+Subproject commit 3a621e102350582d610dfc726d2cb7263b150bf2
diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index f34ed84e1c..943a00b369 100644
--- a/doc/manual/manual.md
+++ b/doc/manual/manual.md
@@ -1715,7 +1715,19 @@ Note that:
   the `.linked-mir.json` file that appears after `linking X mir files into`, as
   that is the JSON file that must be loaded with SAW.
 * `SAW_RUST_LIBRARY_PATH` should point to the the MIR JSON files for the Rust
-  standard library.
+  standard libraries.
+
+  SAW binary distributions include these MIR JSON files, so if you are using a
+  SAW binary distribution, it suffices to define
+  `SAW_RUST_LIBRARY_PATH=<saw-directory>/lib/rlibs`. If you are building SAW
+  from source, you must also build the MIR JSON files for the Rust standard
+  libraries from source. To do so, run the following commands:
+
+  ```
+  $ cd deps/crucible/crux-mir
+  $ ./translate_libs.sh
+  $ export SAW_RUST_LIBRARY_PATH=$(pwd)/rlibs
+  ```
 
 `mir-json` also supports compiling individual `.rs` files through `mir-json`'s
 `saw-rustc` command. As the name suggests, it accepts all of the flags that