diff --git a/docs/user/FlowVariables.md b/docs/user/FlowVariables.md
index 22a089672e..084d004311 100644
--- a/docs/user/FlowVariables.md
+++ b/docs/user/FlowVariables.md
@@ -280,7 +280,7 @@ configuration file.
 | <a name="SC_LEF"></a>SC_LEF| Path to technology standard cell LEF file.| |
 | <a name="SDC_FILE"></a>SDC_FILE| The path to design constraint (SDC) file.| |
 | <a name="SEAL_GDS"></a>SEAL_GDS| Seal macro to place around the design.| |
-| <a name="SEC_CHECK"></a>SEC_CHECK| Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. If this fails, report an issue to OpenROAD.| 0|
+| <a name="SEC_CHECK"></a>SEC_CHECK| Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. Hard macros, the sub-blocks listed in BLOCKS and every BLOCK-class cell such as SRAM macros, are checked as black boxes (proof boundaries): they are the same cells in both netlists and their abstracts carry no logic. If this fails, report an issue to OpenROAD.| $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)|
 | <a name="SETUP_MOVE_SEQUENCE"></a>SETUP_MOVE_SEQUENCE| Passed as -sequence to repair_timing. This should be a string of move keywords separated by commas.| |
 | <a name="SETUP_REPAIR_PHASES"></a>SETUP_REPAIR_PHASES| Passed as -phases to repair_timing. This should be a string of setup repair phase names separated by spaces. Set to PARALLEL_EVAL to repair setup timing with the experimental parallel evaluation policy. When unset, repair_timing runs its default phases.| |
 | <a name="SETUP_SLACK_MARGIN"></a>SETUP_SLACK_MARGIN| Specifies a time margin for the slack when fixing setup violations. This option allows you to overfix or underfix(negative value, terminate retiming before 0 or positive slack). See HOLD_SLACK_MARGIN for more details.| 0|
diff --git a/flow/designs/asap7/chi_async_bridge/config.mk b/flow/designs/asap7/chi_async_bridge/config.mk
index e8691faa2d..1f88d5ae1b 100644
--- a/flow/designs/asap7/chi_async_bridge/config.mk
+++ b/flow/designs/asap7/chi_async_bridge/config.mk
@@ -37,4 +37,8 @@ export VERILOG_TOP_PARAMS     = REQ_W 32 RSP_W 16 DAT_W 64 SNP_W 24 DEPTH 4
 else ifeq ($(FLOW_VARIANT),medium)
 export VERILOG_TOP_PARAMS     = DEPTH 4
 endif
+
+# Temporary disabling: the asynchronous clock-domain crossings are outside
+# the sequential check.
+export SEC_CHECK = 0
 export SETUP_REPAIR_PHASES = PARALLEL_EVAL
diff --git a/flow/designs/asap7/cva6/config.mk b/flow/designs/asap7/cva6/config.mk
index 3e393c28a8..01f6cfe6b6 100644
--- a/flow/designs/asap7/cva6/config.mk
+++ b/flow/designs/asap7/cva6/config.mk
@@ -82,11 +82,6 @@ export SYNTH_VERILOG_SURGERY  = $(DESIGN_HOME)/$(PLATFORM)/cva6/surgery.py
 export AUTO_MEMORIES          = 1
 export ADDITIONAL_MEMORIES    = $(DESIGN_HOME)/$(PLATFORM)/cva6/cva6.memories
 
-# Kepler LEC off for now: kepler-formal stops on the macros AUTO_MEMORIES
-# makes ("cva6_icache_data_sram cannot be found"). A new kepler-formal is
-# in the works; the Kepler team rewires LEC for cva6 with it.
-export LEC_CHECK              = 0
-
 export SDC_FILE               = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NAME)/constraint.sdc
 
 export CORE_UTILIZATION       = 70
diff --git a/flow/designs/asap7/ethmac/config.mk b/flow/designs/asap7/ethmac/config.mk
index 4c14fa8f65..b6d8a06abd 100644
--- a/flow/designs/asap7/ethmac/config.mk
+++ b/flow/designs/asap7/ethmac/config.mk
@@ -13,3 +13,7 @@ export PLACE_DENSITY          = 0.75
 export GPL_PLACE_IOS          = 1
 
 export HOLD_SLACK_MARGIN      = -10
+
+# Temporary disabling: the design has several clock domains and the
+# sequential check does not yet cover logic crossing between them.
+export SEC_CHECK = 0
diff --git a/flow/designs/asap7/ethmac_lvt/config.mk b/flow/designs/asap7/ethmac_lvt/config.mk
index eee9cdc19a..0b4cd0ce17 100644
--- a/flow/designs/asap7/ethmac_lvt/config.mk
+++ b/flow/designs/asap7/ethmac_lvt/config.mk
@@ -17,4 +17,7 @@ export ASAP7_USE_VT           = LVT
 
 export RECOVER_POWER          = 1
 
+# Temporary disabling: the design has several clock domains and the
+# sequential check does not yet cover logic crossing between them.
+export SEC_CHECK = 0
 export SETUP_REPAIR_PHASES = PARALLEL_EVAL
diff --git a/flow/designs/asap7/swerv_wrapper/config.mk b/flow/designs/asap7/swerv_wrapper/config.mk
index 055969887d..fda0ec874e 100644
--- a/flow/designs/asap7/swerv_wrapper/config.mk
+++ b/flow/designs/asap7/swerv_wrapper/config.mk
@@ -65,3 +65,7 @@ export SYNTH_USE_SYN = 1
 export OPENROAD_HIERARCHICAL = 1
 
 export GPL_RANDOM_SEED = 2
+
+# Temporary disabling: the design has several clock domains and the
+# sequential check does not yet cover logic crossing between them.
+export SEC_CHECK = 0
diff --git a/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk b/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk
index d42b756487..3e6081a765 100644
--- a/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk
+++ b/flow/designs/ihp-sg13g2/i2c-gpio-expander/config.mk
@@ -56,3 +56,7 @@ export PDN_TCL = $(DESIGN_HOME)/$(PLATFORM)/$(DESIGN_NICKNAME)/pdn.tcl
 
 export BLOCKS = I2cDeviceCtrl
 
+
+# Temporary disabling: the bidirectional IO pads are outside the sequential
+# check.
+export SEC_CHECK = 0
diff --git a/flow/designs/nangate45/mempool_group/config.mk b/flow/designs/nangate45/mempool_group/config.mk
index 8cca19fda0..8be9e2bcf9 100644
--- a/flow/designs/nangate45/mempool_group/config.mk
+++ b/flow/designs/nangate45/mempool_group/config.mk
@@ -78,3 +78,7 @@ export CORE_AREA   = 10 12 1090 1090
 export RTLMP_MIN_CHANNEL_SIZE = 20 20
 
 export SYNTH_HDL_FRONTEND = slang
+
+# Temporary disabling: the hierarchical netlist leaves memory write-mask pins
+# undriven, which the sequential check cannot verify.
+export SEC_CHECK = 0
diff --git a/flow/designs/nangate45/swerv/config.mk b/flow/designs/nangate45/swerv/config.mk
index ecb13be9cf..b66f6e80f4 100644
--- a/flow/designs/nangate45/swerv/config.mk
+++ b/flow/designs/nangate45/swerv/config.mk
@@ -13,3 +13,7 @@ export TNS_END_PERCENT        = 100
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+# Temporary disabling: the design has several clock domains and the
+# sequential check does not yet cover logic crossing between them.
+export SEC_CHECK = 0
diff --git a/flow/designs/nangate45/swerv_wrapper/config.mk b/flow/designs/nangate45/swerv_wrapper/config.mk
index 861bc792a4..6921c366a5 100644
--- a/flow/designs/nangate45/swerv_wrapper/config.mk
+++ b/flow/designs/nangate45/swerv_wrapper/config.mk
@@ -24,3 +24,7 @@ export TNS_END_PERCENT        = 100
 
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
+
+# Temporary disabling: the design has several clock domains and the
+# sequential check does not yet cover logic crossing between them.
+export SEC_CHECK = 0
diff --git a/flow/designs/sky130hd/chameleon/config.mk b/flow/designs/sky130hd/chameleon/config.mk
index 471431dc90..18db3023dc 100644
--- a/flow/designs/sky130hd/chameleon/config.mk
+++ b/flow/designs/sky130hd/chameleon/config.mk
@@ -51,3 +51,7 @@ export TNS_END_PERCENT    = 100
 export SETUP_REPAIR_PHASES = PARALLEL_EVAL
 
 export RTLMP_MIN_CHANNEL_SIZE = 70 70
+
+# Temporary disabling: the hard macros carry no logic in their Liberty, which
+# leaves no output for the sequential check to verify.
+export SEC_CHECK = 0
diff --git a/flow/designs/sky130hd/microwatt/config.mk b/flow/designs/sky130hd/microwatt/config.mk
index b813db69b2..a6837f25ae 100644
--- a/flow/designs/sky130hd/microwatt/config.mk
+++ b/flow/designs/sky130hd/microwatt/config.mk
@@ -49,5 +49,7 @@ endif
 export SWAP_ARITH_OPERATORS = 1
 export OPENROAD_HIERARCHICAL = 1
 
-# Temporary disabling
+# Temporary disabling: the hierarchical netlist is rejected by the
+# equivalence checker (duplicate wire declaration).
 export LEC_CHECK = 0
+export SEC_CHECK = 0
diff --git a/flow/platforms/ihp-sg13g2/config.mk b/flow/platforms/ihp-sg13g2/config.mk
index e1daf3a001..a2eb83c5c0 100644
--- a/flow/platforms/ihp-sg13g2/config.mk
+++ b/flow/platforms/ihp-sg13g2/config.mk
@@ -169,7 +169,7 @@ export KLAYOUT_DRC_FILE ?= $(PLATFORM_DIR)/drc/sg13g2_minimal.lydrc
 export CDL_FILE ?= $(PLATFORM_DIR)/cdl/sg13g2_stdcell.cdl
 #export KLAYOUT_LVS_FILE = $(PLATFORM_DIR)/lvs/$(PLATFORM).lylvs
 
-export REMOVE_CELLS_FOR_LEC ?= "bondpad_70* sg13g2*"
+export REMOVE_CELLS_FOR_LEC ?= "bondpad_70*"
 
 # ---------------------------------------------------------
 #  Final
diff --git a/flow/scripts/formal_check.tcl b/flow/scripts/formal_check.tcl
index 10c3187c20..fc603c3d79 100644
--- a/flow/scripts/formal_check.tcl
+++ b/flow/scripts/formal_check.tcl
@@ -41,18 +41,34 @@ proc write_lec_verilog { filename } {
   }
 }
 
+# Liberty files for kepler-formal: the ones read_liberty.tcl reads, LIB_FILES
+# plus the AUTO_MEMORIES views generated under RESULTS_DIR/memories. Without
+# the latter the generated macros are unknown cells and netlist loading stops.
+# The _pre_layout variants are skipped, as in read_liberty.tcl.
+proc formal_lib_files { } {
+  set lib_list $::env(LIB_FILES)
+  if { [env_var_equals AUTO_MEMORIES 1] } {
+    foreach lib_file [glob -nocomplain $::env(RESULTS_DIR)/memories/*.lib] {
+      if { ![string match *_pre_layout.lib $lib_file] } {
+        lappend lib_list $lib_file
+      }
+    }
+  }
+  return $lib_list
+}
+
 proc write_lec_script { step file1 file2 } {
   # Exclude select Liberty files from being passed to kepler-formal
   if { [env_var_exists_and_non_empty REMOVE_LIBS_FOR_LEC] } {
     foreach lib_to_remove $::env(REMOVE_LIBS_FOR_LEC) {
       set remove_libs_set($lib_to_remove) 1
     }
-    set lib_list [lmap item $::env(LIB_FILES) {
+    set lib_list [lmap item [formal_lib_files] {
       if { [info exists remove_libs_set($item)] } { continue }
       set item
     }]
   } else {
-    set lib_list $::env(LIB_FILES)
+    set lib_list [formal_lib_files]
   }
   set outfile [open "$::env(OBJECTS_DIR)/${step}_lec_test.yml" w]
   puts $outfile "format: verilog"
@@ -67,6 +83,86 @@ proc write_lec_script { step file1 file2 } {
   close $outfile
 }
 
+# Hardened sub-blocks (BLOCKS) enter the parent netlist as timing-only
+# abstracts with no logic model, so a formal check would treat every output
+# cone that reaches one as opaque. Return the instance paths of all block
+# instances in the loaded design; both netlists come from the same run, so the
+# same path exists in both and each instance can be paired with itself.
+# Escapes every unescaped `/` in an instance name as `\/`, the OpenSTA SDC
+# convention kepler-formal reads: `/` separates hierarchy levels and `\/` is a
+# literal slash inside one name. Existing escapes are kept as they are.
+proc formal_escape_slashes { name } {
+  set escaped ""
+  set length [string length $name]
+  for { set i 0 } { $i < $length } { incr i } {
+    set ch [string index $name $i]
+    if { $ch eq "\\" } {
+      incr i
+      append escaped "\\" [string index $name $i]
+    } elseif { $ch eq "/" } {
+      append escaped "\\/"
+    } else {
+      append escaped $ch
+    }
+  }
+  return $escaped
+}
+
+# Mirrors dbNetwork::stripParentPrefix: in a hierarchical database write_verilog
+# names a leaf by what follows the last unescaped `/` of its database name.
+proc formal_strip_parent_prefix { name } {
+  set pos [string last "/" $name]
+  while { $pos >= 0 } {
+    if { $pos == 0 || [string index $name [expr { $pos - 1 }]] ne "\\" } {
+      return [string range $name [expr { $pos + 1 }] end]
+    }
+    set pos [string last "/" $name [expr { $pos - 2 }]]
+  }
+  return $name
+}
+
+# Boundary path of a block instance exactly as write_verilog names it: in a flat
+# database the whole instance name is one leaf (`\u0/r0 ` in Verilog, so the
+# path is `u0\/r0`); in a hierarchical database the leaf keeps its module
+# instance path and loses the parent prefix. Paths are never reinterpreted.
+proc formal_boundary_path { inst } {
+  set name [$inst getName]
+  set prefix ""
+  if { [[ord::get_db] hasHierarchy] } {
+    set mod_inst [[$inst getModule] getModInst]
+    if { $mod_inst != "NULL" } {
+      set prefix "[$mod_inst getHierarchicalName]/"
+    }
+    set name [formal_strip_parent_prefix $name]
+  }
+  return "$prefix[formal_escape_slashes $name]"
+}
+
+# Hard macros are proof boundaries: the instances of the masters listed in
+# BLOCKS, and every instance of a BLOCK-class master (SRAM macros, hardened
+# sub-blocks). A macro is the same cell in both netlists, so only its
+# connections need checking; expanding its contents into state would only make
+# the proof slower.
+proc formal_block_instance_paths { } {
+  set paths {}
+  set blocks {}
+  if { [env_var_exists_and_non_empty BLOCKS] } {
+    set blocks $::env(BLOCKS)
+  }
+  set block [ord::get_db_block]
+  foreach inst [$block getInsts] {
+    set master [$inst getMaster]
+    if { [$master isBlock] || [lsearch -exact $blocks [$master getName]] >= 0 } {
+      lappend paths [formal_boundary_path $inst]
+    }
+  }
+  return [lsort $paths]
+}
+
+proc formal_yaml_quote { text } {
+  return "\"[string map {\\ \\\\ \" \\\"} $text]\""
+}
+
 proc write_sec_script { step file1 file2 } {
   set outfile [open "$::env(OBJECTS_DIR)/${step}_sec_test.yml" w]
   puts $outfile "format: verilog"
@@ -76,9 +172,20 @@ proc write_sec_script { step file1 file2 } {
   puts $outfile "  - $::env(RESULTS_DIR)/${file1}"
   puts $outfile "  - $::env(RESULTS_DIR)/${file2}"
   puts $outfile "liberty_files:"
-  foreach libFile $::env(LIB_FILES) {
+  foreach libFile [formal_lib_files] {
     puts $outfile " - $libFile"
   }
+  # Each macro instance becomes a proof boundary: its input pins are compared
+  # across the two netlists and its output pins are shared free inputs, so the
+  # macro is checked as a black box instead of hiding the cones behind it.
+  set boundaries [formal_block_instance_paths]
+  if { [llength $boundaries] > 0 } {
+    puts $outfile "set_as_boundary:"
+    foreach path $boundaries {
+      set quoted [formal_yaml_quote $path]
+      puts $outfile "  - \[$quoted, $quoted\]"
+    }
+  }
   puts $outfile "log_file: $::env(LOG_DIR)/${step}_sec_check.log"
   close $outfile
 }
diff --git a/flow/scripts/variables.json b/flow/scripts/variables.json
index cfd396c5f6..a07802dc09 100644
--- a/flow/scripts/variables.json
+++ b/flow/scripts/variables.json
@@ -1164,8 +1164,8 @@
     "description": "Seal macro to place around the design.\n"
   },
   "SEC_CHECK": {
-    "default": 0,
-    "description": "Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. If this fails, report an issue to OpenROAD.\n",
+    "default": "$(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)",
+    "description": "Perform a sequential equivalence check between the initial synthesis netlist and final netlist with the Kepler Formal PDR engine. Hard macros, the sub-blocks listed in BLOCKS and every BLOCK-class cell such as SRAM macros, are checked as black boxes (proof boundaries): they are the same cells in both netlists and their abstracts carry no logic. If this fails, report an issue to OpenROAD.\n",
     "stages": [
       "synth",
       "final"
diff --git a/flow/scripts/variables.yaml b/flow/scripts/variables.yaml
index cf5042b072..b6b85f0599 100644
--- a/flow/scripts/variables.yaml
+++ b/flow/scripts/variables.yaml
@@ -1738,9 +1738,12 @@ LEC_CHECK:
 SEC_CHECK:
   description: >
     Perform a sequential equivalence check between the initial synthesis
-    netlist and final netlist with the Kepler Formal PDR engine. If this
-    fails, report an issue to OpenROAD.
-  default: 0
+    netlist and final netlist with the Kepler Formal PDR engine. Hard macros,
+    the sub-blocks listed in BLOCKS and every BLOCK-class cell such as SRAM
+    macros, are checked as black boxes (proof boundaries): they are the same
+    cells in both netlists and their abstracts carry no logic. If this fails,
+    report an issue to OpenROAD.
+  default: $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)
   stages:
     - synth
     - final
diff --git a/tools/kepler-formal b/tools/kepler-formal
index f70c2e3859..6870bd1abd 160000
--- a/tools/kepler-formal
+++ b/tools/kepler-formal
@@ -1 +1 @@
-Subproject commit f70c2e38592d704c8cccf68433b091e82c8118f0
+Subproject commit 6870bd1abd8c1792c2b98b9c69e60659faa8ff9f