diff --git a/Makefile b/Makefile
index 17495118..5c310e64 100644
--- a/Makefile
+++ b/Makefile
@@ -38,6 +38,12 @@ CSVS	    = $(wildcard $(CSV_DIR)/*.csv)
 GEN_DIR     = $(SRC_DIR)/generated
 SCRIPTS_DIR = $(SRC_DIR)/scripts
 
+# Downloaded Sail Asciidoc JSON, which includes all of
+# the Sail code and can be embedded. We don't vendor it
+# into this repo since it's quite large (~4MB).
+SAIL_ASCIIDOC_JSON_URL_FILE = riscv_RV64.json.url
+SAIL_ASCIIDOC_JSON = $(GEN_DIR)/riscv_RV64.json
+
 # Output files
 PDF_RESULT    := $(BUILD_DIR)/riscv-cheri.pdf
 HTML_RESULT   := $(BUILD_DIR)/riscv-cheri.html
@@ -89,7 +95,8 @@ ASCIIDOC_OPTIONS  = --trace --verbose                                \
                     --failure-level=ERROR $(EXTRA_ASCIIDOC_OPTIONS)
 ASCIIDOC_REQUIRES = --require=asciidoctor-bibtex       \
                     --require=asciidoctor-diagram      \
-                    --require=asciidoctor-mathematical
+                    --require=asciidoctor-mathematical \
+                    --require=asciidoctor-sail
 
 # File extension to backend map.
 ASCIIDOC_BACKEND_.html = html5
@@ -130,11 +137,11 @@ $(BUILD_DIR):
 	@echo "  DIR $@"
 	@mkdir -p $@
 
-%.pdf: $(SRCS) $(IMGS) $(GEN_SRC) | $(BUILD_DIR)
+%.pdf: $(SRCS) $(IMGS) $(GEN_SRC) $(SAIL_ASCIIDOC_JSON) | $(BUILD_DIR)
 	@echo "  DOC $@"
 	$(BUILD_COMMAND)
 
-%.html: $(SRCS) $(IMGS) $(GEN_SRC) | $(BUILD_DIR)
+%.html: $(SRCS) $(IMGS) $(GEN_SRC) $(SAIL_ASCIIDOC_JSON) | $(BUILD_DIR)
 	@echo "  DOC $@"
 	$(BUILD_COMMAND)
 
@@ -143,9 +150,14 @@ $(GEN_SRC) &: $(CSVS) $(GEN_SCRIPT)
 	@echo "  GEN $@"
 	@$(GEN_SCRIPT) -o $(GEN_DIR) --csr $(CSV_DIR)/CHERI_CSR.csv --isa $(CSV_DIR)/CHERI_ISA.csv
 
+# Download the Sail JSON. The URL is stored in a file so if the URL changes
+# Make will know to download it again.
+$(SAIL_ASCIIDOC_JSON): $(SAIL_ASCIIDOC_JSON_URL_FILE)
+	@curl --location '$(shell cat $<)' --output $@
+
 # Clean
 clean:
 	@echo "  CLEAN"
-	@$(RM) -r $(PDF_RESULT) $(HTML_RESULT) $(GEN_SRC)
+	@$(RM) -r $(PDF_RESULT) $(HTML_RESULT) $(GEN_SRC) $(SAIL_ASCIIDOC_JSON)
 
 .PHONY: all generate clean
diff --git a/riscv_RV64.json.url b/riscv_RV64.json.url
new file mode 100644
index 00000000..85b94f02
--- /dev/null
+++ b/riscv_RV64.json.url
@@ -0,0 +1 @@
+https://github.com/CHERI-Alliance/sail-cheri-riscv/releases/download/2025-01-02/riscv_RV64.json
diff --git a/src/attributes.adoc b/src/attributes.adoc
index c756c011..ba87d512 100644
--- a/src/attributes.adoc
+++ b/src/attributes.adoc
@@ -36,6 +36,9 @@ endif::[]
 :xrefstyle: short
 :attribute-missing: warn
 
+// Sail source code
+:sail-doc: src/generated/riscv_RV64.json
+
 ///////////////////////////////////////////////////////////////////////////////
 // Top-level CHERI definitions
 ///////////////////////////////////////////////////////////////////////////////
diff --git a/src/insns/acperm_32bit.adoc b/src/insns/acperm_32bit.adoc
index 30a483ce..af877d26 100644
--- a/src/insns/acperm_32bit.adoc
+++ b/src/insns/acperm_32bit.adoc
@@ -88,6 +88,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO: Sail does not have the new encoding of the permissions field.
---
+sail::execute[clause="ACPERM(_, _, _)",part=body,unindent]
diff --git a/src/insns/addi16sp_16bit.adoc b/src/insns/addi16sp_16bit.adoc
index e8b1c661..03645123 100644
--- a/src/insns/addi16sp_16bit.adoc
+++ b/src/insns/addi16sp_16bit.adoc
@@ -38,6 +38,4 @@ Prerequisites for {cheri_int_mode_name}::
 
 {cheri_cap_mode_name} Operation::
 +
---
-TODO
---
+sail::execute[clause="C_ADDI16SP_capmode(_)",part=body,unindent]
diff --git a/src/insns/addi4spn_16bit.adoc b/src/insns/addi4spn_16bit.adoc
index 52534fa6..324049a8 100644
--- a/src/insns/addi4spn_16bit.adoc
+++ b/src/insns/addi4spn_16bit.adoc
@@ -37,6 +37,4 @@ Prerequisites for C.ADDI4SPN::
 
 {cheri_cap_mode_name} Operation::
 +
---
-TODO
---
+sail::execute[clause="C_ADDI4SPN_capmode(_, _)",part=body,unindent]
diff --git a/src/insns/adduw_32bit.adoc b/src/insns/adduw_32bit.adoc
index 4cbaaa95..433c4fae 100644
--- a/src/insns/adduw_32bit.adoc
+++ b/src/insns/adduw_32bit.adoc
@@ -38,13 +38,9 @@ Prerequisites for {cheri_int_mode_name}::
 RV64, {cheri_default_ext_name}, Zba
 
 {cheri_cap_mode_name} Operation::
-[source,SAIL,subs="verbatim,quotes"]
---
-TBD
---
++
+sail::execute[clause="ZBA_RTYPEUW_capmode(_, _, _, _)",part=body,unindent]
 
 {cheri_int_mode_name} Operation::
 +
---
-TODO
---
+sail::execute[clause="ZBA_RTYPEUW(_, _, _, _)",part=body,unindent]
diff --git a/src/insns/auipc_32bit.adoc b/src/insns/auipc_32bit.adoc
index bc3be14e..e29ddd84 100644
--- a/src/insns/auipc_32bit.adoc
+++ b/src/insns/auipc_32bit.adoc
@@ -39,6 +39,4 @@ Prerequisites for {cheri_int_mode_name}::
 
 Operation for AUIPC::
 +
---
-TODO
---
+sail::execute[clause="AUIPC_capmode(_, _)",part=body,unindent]
diff --git a/src/insns/cadd_32bit.adoc b/src/insns/cadd_32bit.adoc
index 3de64d49..2b269e13 100644
--- a/src/insns/cadd_32bit.adoc
+++ b/src/insns/cadd_32bit.adoc
@@ -58,12 +58,8 @@ Prerequisites::
 
 Operation (CADD)::
 +
---
-TODO
---
+sail::execute[clause="CADD(_, _, _)",part=body,unindent]
 
 Operation (CADDI)::
 +
---
-TODO
---
+sail::execute[clause="CADDI(_, _, _)",part=body,unindent]
diff --git a/src/insns/cbld_32bit.adoc b/src/insns/cbld_32bit.adoc
index 776cbe79..7ba1eefb 100644
--- a/src/insns/cbld_32bit.adoc
+++ b/src/insns/cbld_32bit.adoc
@@ -49,23 +49,6 @@ include::require_cre.adoc[]
 Prerequisites::
 {cheri_base_ext_name}
 
-Simplified Operation TODO #not debugged much easier to read than the existing SAIL# ::
-[source,SAIL,subs="verbatim,quotes"]
---
-let cs1_val = C(cs1);
-let cs2_val = C(cs2) [with tag=1];
-//isCapSubset includes derivability checks on both operands
-let subset  = isCapSubset(cs1_val, cs2_val);
-//Clear cd.tag if cs2 isn't a subset of cs1, or if
-//cs1 is untagged or sealed, or if either is underivable
-C(cd)       = clearTagIf(cs2_val, not(subset) |
-                                  not(cs1_val.tag) |
-                                  isCapSealed(cs1_val));
-RETIRE_SUCCESS
---
-
 Operation::
 +
---
-TODO: Original Sail looks at otype field, etc that don't exist
---
+sail::execute[clause="CBLD(_, _, _)",part=body,unindent]
diff --git a/src/insns/cmv_32bit.adoc b/src/insns/cmv_32bit.adoc
index abc7ad01..8776e2a4 100644
--- a/src/insns/cmv_32bit.adoc
+++ b/src/insns/cmv_32bit.adoc
@@ -39,6 +39,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="CMV(_, _)",part=body,unindent]
diff --git a/src/insns/cram_32bit.adoc b/src/insns/cram_32bit.adoc
index 49546944..b2f96ed9 100644
--- a/src/insns/cram_32bit.adoc
+++ b/src/insns/cram_32bit.adoc
@@ -25,6 +25,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="CRAM(_, _)",part=body,unindent]
diff --git a/src/insns/gcbase_32bit.adoc b/src/insns/gcbase_32bit.adoc
index 96b072d7..1a39d392 100644
--- a/src/insns/gcbase_32bit.adoc
+++ b/src/insns/gcbase_32bit.adoc
@@ -32,6 +32,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCBASE(_, _)",part=body,unindent]
diff --git a/src/insns/gchi_32bit.adoc b/src/insns/gchi_32bit.adoc
index 4afc04e4..a874b160 100644
--- a/src/insns/gchi_32bit.adoc
+++ b/src/insns/gchi_32bit.adoc
@@ -29,6 +29,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCHI(_, _)",part=body,unindent]
diff --git a/src/insns/gclen_32bit.adoc b/src/insns/gclen_32bit.adoc
index 2703b0ab..2fad31e3 100644
--- a/src/insns/gclen_32bit.adoc
+++ b/src/insns/gclen_32bit.adoc
@@ -36,6 +36,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCLEN(_, _)",part=body,unindent]
diff --git a/src/insns/gcmode_32bit.adoc b/src/insns/gcmode_32bit.adoc
index 1f7cb056..fdfacf3e 100644
--- a/src/insns/gcmode_32bit.adoc
+++ b/src/insns/gcmode_32bit.adoc
@@ -27,7 +27,5 @@ Prerequisites::
 {cheri_default_ext_name}
 
 Operation::
-[source,SAIL,subs="verbatim,quotes"]
---
-TODO
---
++
+sail::execute[clause="GCMODE(_, _)",part=body,unindent]
diff --git a/src/insns/gcperm_32bit.adoc b/src/insns/gcperm_32bit.adoc
index 6333060b..36c06a42 100644
--- a/src/insns/gcperm_32bit.adoc
+++ b/src/insns/gcperm_32bit.adoc
@@ -41,6 +41,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO: The encoding of permissions changed.
---
+sail::execute[clause="GCPERM(_, _)",part=body,unindent]
diff --git a/src/insns/gctag_32bit.adoc b/src/insns/gctag_32bit.adoc
index 4a5cf898..8a924b94 100644
--- a/src/insns/gctag_32bit.adoc
+++ b/src/insns/gctag_32bit.adoc
@@ -28,6 +28,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCTAG(_, _)",part=body,unindent]
diff --git a/src/insns/gctype_32bit.adoc b/src/insns/gctype_32bit.adoc
index c0b69b70..fd9448c9 100644
--- a/src/insns/gctype_32bit.adoc
+++ b/src/insns/gctype_32bit.adoc
@@ -43,6 +43,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="GCTYPE(_, _)",part=body,unindent]
diff --git a/src/insns/jal_32bit.adoc b/src/insns/jal_32bit.adoc
index 8d6522cb..f4a036d9 100644
--- a/src/insns/jal_32bit.adoc
+++ b/src/insns/jal_32bit.adoc
@@ -48,8 +48,6 @@ Prerequisites for {cheri_cap_mode_name}::
 Prerequisites for {cheri_int_mode_name}::
 {cheri_default_ext_name}
 
-Operation::
+{cheri_cap_mode_name} Operation::
 +
---
-TODO
---
+sail::execute[clause="JAL_capmode(_, _)",part=body,unindent]
diff --git a/src/insns/jalr_32bit.adoc b/src/insns/jalr_32bit.adoc
index 532640fe..a9d9ca8a 100644
--- a/src/insns/jalr_32bit.adoc
+++ b/src/insns/jalr_32bit.adoc
@@ -65,8 +65,6 @@ Prerequisites {cheri_cap_mode_name}::
 Prerequisites {cheri_int_mode_name}::
 {cheri_default_ext_name}
 
-Operation::
+{cheri_cap_mode_name} Operation::
 +
---
-TBD
---
+sail::execute[clause="JALR_capmode(_, _)",part=body,unindent]
diff --git a/src/insns/modesw_32bit.adoc b/src/insns/modesw_32bit.adoc
index 7b3f015f..14956405 100644
--- a/src/insns/modesw_32bit.adoc
+++ b/src/insns/modesw_32bit.adoc
@@ -34,7 +34,5 @@ Prerequisites::
 {cheri_default_ext_name}
 
 Operation::
-[source,SAIL,subs="verbatim,quotes"]
---
-TODO
---
++
+sail::execute[clause="MODESW()",part=body,unindent]
diff --git a/src/insns/scaddr_32bit.adoc b/src/insns/scaddr_32bit.adoc
index 1952825d..812366d6 100644
--- a/src/insns/scaddr_32bit.adoc
+++ b/src/insns/scaddr_32bit.adoc
@@ -34,6 +34,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SCADDR(_, _, _)",part=body,unindent]
diff --git a/src/insns/scbnds_32bit.adoc b/src/insns/scbnds_32bit.adoc
index 5b6455b9..9947fe6c 100644
--- a/src/insns/scbnds_32bit.adoc
+++ b/src/insns/scbnds_32bit.adoc
@@ -54,12 +54,8 @@ Prerequisites::
 
 Operation for SCBNDS::
 +
---
-TODO
---
+sail::execute[clause="SCBNDS(_, _, _)",part=body,unindent]
 
 Operation for SCBNDSI::
 +
---
-TODO
---
+sail::execute[clause="SCBNDSI(_, _, _, _)",part=body,unindent]
diff --git a/src/insns/scbndsr_32bit.adoc b/src/insns/scbndsr_32bit.adoc
index 67bb9bf2..da695b59 100644
--- a/src/insns/scbndsr_32bit.adoc
+++ b/src/insns/scbndsr_32bit.adoc
@@ -36,6 +36,4 @@ Prerequisites::
 
 Operation for SCBNDSR::
 +
---
-TODO
---
+sail::execute[clause="SCBNDSR(_, _, _)",part=body,unindent]
diff --git a/src/insns/sceq_32bit.adoc b/src/insns/sceq_32bit.adoc
index e9087519..3e60d7ec 100644
--- a/src/insns/sceq_32bit.adoc
+++ b/src/insns/sceq_32bit.adoc
@@ -30,6 +30,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SCEQ(_, _, _)",part=body,unindent]
diff --git a/src/insns/schi_32bit.adoc b/src/insns/schi_32bit.adoc
index 496070e8..23dba696 100644
--- a/src/insns/schi_32bit.adoc
+++ b/src/insns/schi_32bit.adoc
@@ -30,6 +30,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SCHI(_, _, _)",part=body,unindent]
diff --git a/src/insns/scmode_32bit.adoc b/src/insns/scmode_32bit.adoc
index 9d7a1045..f5d0c7f8 100644
--- a/src/insns/scmode_32bit.adoc
+++ b/src/insns/scmode_32bit.adoc
@@ -35,7 +35,5 @@ Prerequisites::
 {cheri_default_ext_name}
 
 Operation ::
-[source,SAIL,subs="verbatim,quotes"]
---
-TODO
---
++
+sail::execute[clause="SCMODE(_, _, _)",part=body,unindent]
diff --git a/src/insns/scss_32bit.adoc b/src/insns/scss_32bit.adoc
index c9db1951..17c882ac 100644
--- a/src/insns/scss_32bit.adoc
+++ b/src/insns/scss_32bit.adoc
@@ -42,6 +42,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SCSS(_, _, _)",part=body,unindent]
diff --git a/src/insns/sentry_32bit.adoc b/src/insns/sentry_32bit.adoc
index 1f16255b..6ac01bd0 100644
--- a/src/insns/sentry_32bit.adoc
+++ b/src/insns/sentry_32bit.adoc
@@ -36,6 +36,4 @@ Prerequisites::
 
 Operation::
 +
---
-TODO
---
+sail::execute[clause="SENTRY(_, _)",part=body,unindent]
diff --git a/src/insns/sh123add_32bit.adoc b/src/insns/sh123add_32bit.adoc
index f4f83f94..a472c2db 100644
--- a/src/insns/sh123add_32bit.adoc
+++ b/src/insns/sh123add_32bit.adoc
@@ -57,13 +57,9 @@ Prerequisites for {cheri_int_mode_name}::
 {cheri_default_ext_name}, Zba
 
 {cheri_cap_mode_name} Operation::
-[source,SAIL,subs="verbatim,quotes"]
---
-TODO
---
++
+sail::execute[clause="ZBA_RTYPE_capmode(_, _, _, _)",part=body,unindent]
 
 {cheri_int_mode_name} Operation::
 +
---
-TODO
---
+sail::execute[clause="ZBA_RTYPE(_, _, _, _)",part=body,unindent]
diff --git a/src/insns/sh123adduw_32bit.adoc b/src/insns/sh123adduw_32bit.adoc
index 91e32d78..36cea502 100644
--- a/src/insns/sh123adduw_32bit.adoc
+++ b/src/insns/sh123adduw_32bit.adoc
@@ -57,13 +57,9 @@ Prerequisites for {cheri_int_mode_name}::
 RV64, {cheri_default_ext_name}, Zba
 
 {cheri_cap_mode_name} Operation::
-[source,SAIL,subs="verbatim,quotes"]
---
-TODO
---
++
+sail::execute[clause="ZBA_RTYPEUW_capmode(_, _, _, _)",part=body,unindent]
 
 {cheri_int_mode_name} Operation::
 +
---
-TODO
---
+sail::execute[clause="ZBA_RTYPEUW(_, _, _, _)",part=body,unindent]
diff --git a/src/insns/sh4add_32bit.adoc b/src/insns/sh4add_32bit.adoc
index 53c75cb7..342f4d0d 100644
--- a/src/insns/sh4add_32bit.adoc
+++ b/src/insns/sh4add_32bit.adoc
@@ -51,12 +51,9 @@ Prerequisites for {cheri_int_mode_name}::
 RV64, {sh4add_ext_name}
 
 {cheri_cap_mode_name} Operation::
-[source,SAIL,subs="verbatim,quotes"]
---
-TBD
---
++
+sail::execute[clause="ZBA_SH4ADD_capmode(_, _, _)",part=body,unindent]
 
 {cheri_int_mode_name} Operation::
---
-TBD
---
++
+sail::execute[clause="ZBA_SH4ADD(_, _, _)",part=body,unindent]
diff --git a/src/insns/sh4adduw_32bit.adoc b/src/insns/sh4adduw_32bit.adoc
index 3c30ccab..71bc17f0 100644
--- a/src/insns/sh4adduw_32bit.adoc
+++ b/src/insns/sh4adduw_32bit.adoc
@@ -47,12 +47,9 @@ Prerequisites for {cheri_int_mode_name}::
 RV64, {sh4add_ext_name}
 
 {cheri_cap_mode_name} Operation::
-[source,SAIL,subs="verbatim,quotes"]
---
-TBD
---
++
+sail::execute[clause="ZBA_SH4ADDUW_capmode(_, _, _)",part=body,unindent]
 
 {cheri_int_mode_name} Operation::
---
-TBD
---
++
+sail::execute[clause="ZBA_SH4ADDUW(_, _, _)",part=body,unindent]