diff --git a/dv/formal/Makefile b/dv/formal/Makefile
index bdb2706f..db1afdaf 100644
--- a/dv/formal/Makefile
+++ b/dv/formal/Makefile
@@ -1,3 +1,5 @@
+IBEX_ROOT=../..
+
 SAIL=sail
 
 SAIL_RISCV_MODEL_DIR=../sail-riscv/model
@@ -16,6 +18,25 @@ SAIL_SV_FLAGS=-sv -sv-comb -sv-inregs -sv-outregs -sv-nostrings -sv-nopacked -sv
 	-sv-fun2wires wX \
 	-sv-fun2wires 2:rX \
 
+# Use fusesoc to resolve the tree of components, copy all resolved source files into the build/ directory,
+# and then generate a filelist for jasper to ingest.
+# Finally, apply a number of small RTL patches necessary to make the formal flow work. (see files in patches/)
+# (Only patch the duplicated source files that fusesoc has copied into build/fusesoc/src, not the version-controlled originals)
+# - Note. we use the 'vcs' fusesoc backend flow to generate the filelist. This is because fusesoc does not currently implement a
+#   JasperGold backend, but this is not an issue as the file-format generated by the vcs flow is compatible with jasper.
+.PHONY: fusesoc
+fusesoc:
+	mkdir -p build/fusesoc
+	fusesoc \
+	  --cores-root $(IBEX_ROOT) \
+	  run \
+	  --build-root build/fusesoc \
+	  --tool vcs \
+	  --setup \
+	  lowrisc:ibex:ibex_formal:0.1
+	patch -p0 < patches/ibex_top.diff
+	patch -p0 < patches/ibex_id_stage.diff
+
 .PHONY: sv
 sv:
 	mkdir -p build
diff --git a/dv/formal/README.md b/dv/formal/README.md
index 9be85293..6ff4042f 100644
--- a/dv/formal/README.md
+++ b/dv/formal/README.md
@@ -5,6 +5,15 @@ Prerequisities (in your PATH):
 - [psgen](https://github.com/mndstrmr/psgen)
 
 Build instructions:
+- Clone this repository
+- `cd dv/formal`
+- `nix develop .#formal`
+- `make` invokes JasperGold in batch-mode, and attempts to prove everything. (for regressions)
+- `make jg` invokes JasperGold interactively, halting after sourcing the contents of `verify.tcl`.
+
+Building as above invokes the following steps, which can also be done manually during development:
+- `make fusesoc` fetches the necessary RTL using the Fusesoc tool, and makes a local copy inside `build/`. This also creates a filelist (`.scr`) that Jasper knows how to ingest.
+  - This step also patches the Ibex RTL with the changes described [in the section below](#rtl-changes).
 - `git submodule init`
 - `make psgen` to build the SV for the proofs given in `thm/`
 - `make sv` to build the SV translation of the Sail compiler. Will invoke `buildspec.py`, which can be configured to adjust which instructions are defined. By default all of them are, this is correct but slow.
diff --git a/dv/formal/ibex_formal.core b/dv/formal/ibex_formal.core
new file mode 100644
index 00000000..b1958ed3
--- /dev/null
+++ b/dv/formal/ibex_formal.core
@@ -0,0 +1,31 @@
+CAPI=2:
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+name: "lowrisc:ibex:ibex_formal:0.1"
+description: "Ibex formal module used to prove equivalence with Sail"
+
+filesets:
+  files_rtl:
+    depend:
+      - lowrisc:ibex:ibex_pkg
+      - lowrisc:ibex:ibex_core
+      - lowrisc:prim:buf
+      - lowrisc:prim:clock_gating
+      - lowrisc:prim:secded
+      - lowrisc:prim:assert
+      - lowrisc:prim:ram_1p_pkg
+      - lowrisc:prim_generic:buf
+      - lowrisc:prim_generic:clock_gating
+    files:
+      - ../../rtl/ibex_register_file_ff.sv # generic FF-based
+      - ../../rtl/ibex_register_file_fpga.sv # FPGA
+      - ../../rtl/ibex_register_file_latch.sv # ASIC
+      - ../../rtl/ibex_top.sv
+    file_type: systemVerilogSource
+
+targets:
+  default:
+    filesets:
+      - files_rtl
+    toplevel: ibex_top
diff --git a/dv/formal/patches/ibex_id_stage.diff b/dv/formal/patches/ibex_id_stage.diff
new file mode 100644
index 00000000..b0012c45
--- /dev/null
+++ b/dv/formal/patches/ibex_id_stage.diff
@@ -0,0 +1,11 @@
+--- build/fusesoc/src/lowrisc_ibex_ibex_core_0.1/rtl/ibex_id_stage.sv	2024-08-25 12:37:56.787684672 +0100
++++ build/fusesoc/src/lowrisc_ibex_ibex_core_0.1/rtl/ibex_id_stage.sv	2024-08-25 12:39:23.606231887 +0100
+@@ -522,7 +522,7 @@
+     // - When modifying any PMP CSR, PMP check of the next instruction might get invalidated.
+     //   Hence, a pipeline flush is needed to instantiate another PMP check with the updated CSRs.
+     // - When modifying debug CSRs.
+-    if (csr_op_en_o == 1'b1 && (csr_op_o == CSR_OP_WRITE || csr_op_o == CSR_OP_SET)) begin
++    if (csr_op_en_o == 1'b1 && (csr_op_o == CSR_OP_WRITE || csr_op_o == CSR_OP_SET || csr_op_o == CSR_OP_CLEAR)) begin
+       if (csr_num_e'(instr_rdata_i[31:20]) == CSR_MSTATUS ||
+           csr_num_e'(instr_rdata_i[31:20]) == CSR_MIE     ||
+           csr_num_e'(instr_rdata_i[31:20]) == CSR_MSECCFG ||
diff --git a/dv/formal/patches/ibex_top.diff b/dv/formal/patches/ibex_top.diff
new file mode 100644
index 00000000..626c9028
--- /dev/null
+++ b/dv/formal/patches/ibex_top.diff
@@ -0,0 +1,31 @@
+--- build/fusesoc/rtl/ibex_top.sv	2024-08-25 12:49:31.975238123 +0100
++++ build/fusesoc/rtl/ibex_top.sv	2024-08-25 12:51:45.786743599 +0100
+@@ -142,7 +142,7 @@
+ );
+ 
+   localparam bit          Lockstep              = SecureIbex;
+-  localparam bit          ResetAll              = Lockstep;
++  localparam bit          ResetAll              = 1;
+   localparam bit          DummyInstructions     = SecureIbex;
+   localparam bit          RegFileECC            = SecureIbex;
+   localparam bit          RegFileWrenCheck      = SecureIbex;
+@@ -236,12 +236,13 @@
+ 
+   assign core_sleep_o = ~clock_en;
+ 
+-  prim_clock_gating core_clock_gate_i (
+-    .clk_i    (clk_i),
+-    .en_i     (clock_en),
+-    .test_en_i(test_en_i),
+-    .clk_o    (clk)
+-  );
++  assign clk = clk_i;
++  // prim_clock_gating core_clock_gate_i (
++  //   .clk_i    (clk_i),
++  //   .en_i     (clock_en),
++  //   .test_en_i(test_en_i),
++  //   .clk_o    (clk)
++  // );
+ 
+   ////////////////////////
+   // Core instantiation //
diff --git a/dv/formal/verify.tcl b/dv/formal/verify.tcl
index d2206dbe..8a4b9fe6 100644
--- a/dv/formal/verify.tcl
+++ b/dv/formal/verify.tcl
@@ -13,44 +13,13 @@ set_prove_cache_mode coi
 
 set_prove_per_property_time_limit 10s
 
-set ibex_root ../../
-set sail_lib_dir $env(SAIL_DIR)/lib/sv
-set prim $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/
-set dv $ibex_root/vendor/lowrisc_ip/dv/sv/dv_utils/
-
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_pkg.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_alu.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_compressed_decoder.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_controller.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_cs_registers.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_decoder.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_ex_block.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_id_stage.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_if_stage.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_wb_stage.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_load_store_unit.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_multdiv_slow.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_counter.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_multdiv_fast.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_prefetch_buffer.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_fetch_fifo.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_pmp.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_core.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_csr.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_register_file_ff.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/prim_secded_pkg.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/prim_assert.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim/rtl/prim_ram_1p_pkg.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_generic_buf.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/vendor/lowrisc_ip/ip/prim_generic/rtl/prim_generic_clock_gating.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/dv/uvm/core_ibex/common/prim/prim_buf.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/dv/uvm/core_ibex/common/prim/prim_pkg.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/dv/uvm/core_ibex/common/prim/prim_clock_gating.sv
-analyze -sv12 +define+SYNTHESIS -incdir $prim -incdir $dv $ibex_root/rtl/ibex_top.sv
+# Load all Ibex RTL, using the filelist generated by fusesoc
+analyze -sv12 +define+SYNTHESIS -f_relative_to_file_location build/fusesoc/default-vcs/lowrisc_ibex_ibex_formal_0.1.scr
 
+set sail_lib_dir $env(LOWRISC_SAIL_SRC)/lib/sv
 analyze -sv12 -incdir $sail_lib_dir build/ibexspec.sv
-analyze -sv12 spec/stub.sv
 
+analyze -sv12 spec/stub.sv
 analyze -sv12 spec/spec_api.sv
 
 # analyze -sv12 bound/binder.sv