diff --git a/docs/engineering.md b/docs/engineering.md
index 6076512e..85666911 100644
--- a/docs/engineering.md
+++ b/docs/engineering.md
@@ -195,11 +195,15 @@ Verilator regressions.
 `make CONFIG=configs/ci/ihp130.mk formal` proves selected
 protocol invariants with SymbiYosys, Yosys, `sv2v`, and Bitwuzla. The current
 targets are `bus`, `rib_adapter`, `rib2apb`, `sysctrl`, `pll_rcu`, `gpio`,
-`ws2812`, `uart`, `i2c`, `timer`, `clint`, `dvp`, `i2s`, `psram`, and `dma`;
+`ws2812`, `uart`, `i2c`, `timer`, `clint`, `dvp`, `i2s`, `psram`,
+`onchip_ram`, `opipsram`, `dma`, and `sdio`;
 each uses an SBY bounded proof task plus a `cover` task. The default depth is 20;
 `ws2812` uses depth 120 and a 120-second per-task limit to cover a complete
 serialized word and reset path. `i2c` uses depth 80 and a 300-second per-task
-limit to reach a complete receive path and export its witness. `dma` uses a
+limit to reach a complete receive path and export its witness. `opipsram` uses
+depth 40 for prove, cover, and BMC; prove and cover retain a 300-second limit,
+while BMC uses 600 seconds to preserve the full bound on variable-speed hosted
+runners. `dma` uses a
 depth-24 BMC task, depth-32 covers, and a 120-second per-task limit for the narrowest supported four-channel,
 32-bit/4-beat/4-word `dma_core` configuration. Its constrained native AXI4
 responder and AXI4-Stream environment prove source stability under
diff --git a/rtl/mini/mk/formal.mk b/rtl/mini/mk/formal.mk
index 94ed8fca..11ee9886 100644
--- a/rtl/mini/mk/formal.mk
+++ b/rtl/mini/mk/formal.mk
@@ -20,6 +20,7 @@ FORMAL_TIMEOUT               ?= 60
 FORMAL_WS2812_TIMEOUT        ?= 120
 FORMAL_I2C_TIMEOUT           ?= 300
 FORMAL_OPIPSRAM_TIMEOUT      ?= 300
+FORMAL_OPIPSRAM_BMC_TIMEOUT  ?= 600
 FORMAL_DMA_TIMEOUT           ?= 120
 FORMAL_SDIO_TIMEOUT          ?= 120
 FORMAL_COMPACT_COVER_TARGETS := i2c opipsram dma
@@ -238,7 +239,7 @@ $(FORMAL_DIR)/opipsram/bmc.stamp: $(FORMAL_DIR)/opipsram/bmc.sby \
 		--log $(@D)/bmc.log --result $(@D)/result-bmc.json \
 		--env RETROSOC_BITWUZLA=$(FORMAL_BITWUZLA) \
 		--env PATH=$(FORMAL_SOLVER_DIR):$(PATH) \
-		-- timeout --foreground --kill-after=5s $(FORMAL_OPIPSRAM_TIMEOUT)s $(FORMAL_SBY) \
+		-- timeout --foreground --kill-after=5s $(FORMAL_OPIPSRAM_BMC_TIMEOUT)s $(FORMAL_SBY) \
 		-f -d $(@D)/bmc $<
 	@test "$$(awk '{print $$1}' $(@D)/bmc/status)" = PASS
 	@touch $@
diff --git a/tests/test_script_tools.py b/tests/test_script_tools.py
index 9b56c522..9cf3e469 100644
--- a/tests/test_script_tools.py
+++ b/tests/test_script_tools.py
@@ -423,6 +423,16 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
     assert ROOT / "rtl/mini/formal/opipsram_formal.sv" in opipsram.files
 
 
+def test_opipsram_formal_keeps_full_depth_with_hosted_runner_budget() -> None:
+    formal_makefile = (ROOT / "rtl/mini/mk/formal.mk").read_text(encoding="utf-8")
+
+    assert re.search(r"^FORMAL_OPIPSRAM_DEPTH\s+\?= 40$", formal_makefile, re.MULTILINE)
+    assert re.search(r"^FORMAL_OPIPSRAM_BMC_DEPTH\s+\?= 40$", formal_makefile, re.MULTILINE)
+    assert re.search(r"^FORMAL_OPIPSRAM_TIMEOUT\s+\?= 300$", formal_makefile, re.MULTILINE)
+    assert re.search(r"^FORMAL_OPIPSRAM_BMC_TIMEOUT\s+\?= 600$", formal_makefile, re.MULTILINE)
+    assert "$(FORMAL_OPIPSRAM_BMC_TIMEOUT)s $(FORMAL_SBY)" in formal_makefile
+
+
 def test_sysctrl_formal_properties_use_exported_user_core_shape() -> None:
     design = (ROOT / "rtl/mini/formal/sysctrl_formal.sv").read_text(encoding="utf-8")
     properties = (ROOT / "rtl/mini/formal/sysctrl_formal_props.sv").read_text(encoding="utf-8")