diff --git a/docs/user/FlowVariables.md b/docs/user/FlowVariables.md
index 161e77d5a2..abdf496263 100644
--- a/docs/user/FlowVariables.md
+++ b/docs/user/FlowVariables.md
@@ -170,8 +170,8 @@ configuration file.
 | <a name="KLAYOUT_TECH_FILE"></a>KLAYOUT_TECH_FILE| A mapping from LEF/DEF to GDS using the KLayout tool.| |
 | <a name="LATCH_MAP_FILE"></a>LATCH_MAP_FILE| Optional mapping file supplied to Yosys to map latches| |
 | <a name="LAYER_PARASITICS_FILE"></a>LAYER_PARASITICS_FILE| Path to per layer parasitics file. Defaults to $(PLATFORM_DIR)/setRC.tcl.| |
-| <a name="LEC_AUX_VERILOG_FILES"></a>LEC_AUX_VERILOG_FILES| Additional Verilog files (e.g. blackbox stubs) to include in LEC equivalence checks. Appended to the generated Verilog netlist before running the formal equivalence check.| |
-| <a name="LEC_CHECK"></a>LEC_CHECK| Perform a formal equivalence check between before and after netlists. If this fails, report an issue to OpenROAD.| 0|
+| <a name="LEC_AUX_VERILOG_FILES"></a>LEC_AUX_VERILOG_FILES| Additional Verilog files (e.g. blackbox stubs) to include in generated netlists for formal equivalence checks.| |
+| <a name="LEC_CHECK"></a>LEC_CHECK| Perform formal equivalence checks between before and after netlists. This checks CTS repair timing and the initial synthesis netlist against the final netlist. If this fails, report an issue to OpenROAD.| 0|
 | <a name="LIB_FILES"></a>LIB_FILES| A Liberty file of the standard cell library with PVT characterization, input and output characteristics, timing and power definitions for each cell.| |
 | <a name="LIB_MODEL"></a>LIB_MODEL| Selects between NLDM and CCS timing models for the ASAP7 platform. Valid values: NLDM (default), CCS. Used in flow/platforms/asap7/config.mk to pick the LIB_DIR subdirectory and accumulate the corresponding $(CORNER)_$(LIB_MODEL)_LIB_FILES list, and in flow/scripts/load.tcl to gate CCS-specific Tcl branches.| NLDM|
 | <a name="MACRO_BLOCKAGE_HALO"></a>MACRO_BLOCKAGE_HALO| Distance beyond the edges of a macro that will also be covered by the blockage generated for that macro. Note that the default macro blockage halo comes from the largest of the specified MACRO_PLACE_HALO x or y values. This variable overrides that calculation.| |
@@ -270,6 +270,7 @@ configuration file.
 | <a name="SDC_FILE"></a>SDC_FILE| The path to design constraint (SDC) file.| |
 | <a name="SDC_GUT"></a>SDC_GUT| Load design and remove all internal logic before doing synthesis. This is useful when creating a mock .lef abstract that has a smaller area than the amount of logic would allow. bazel-orfs uses this to mock SRAMs, for instance.| |
 | <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="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_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|
 | <a name="SET_RC_TCL"></a>SET_RC_TCL| Metal & Via RC definition file path.| |
@@ -344,11 +345,14 @@ configuration file.
 - [DFF_LIB_FILE](#DFF_LIB_FILE)
 - [DFF_MAP_FILE](#DFF_MAP_FILE)
 - [LATCH_MAP_FILE](#LATCH_MAP_FILE)
+- [LEC_AUX_VERILOG_FILES](#LEC_AUX_VERILOG_FILES)
+- [LEC_CHECK](#LEC_CHECK)
 - [MIN_BUF_CELL_AND_PORTS](#MIN_BUF_CELL_AND_PORTS)
 - [POST_SYNTH_TCL](#POST_SYNTH_TCL)
 - [PRE_SYNTH_TCL](#PRE_SYNTH_TCL)
 - [SDC_FILE](#SDC_FILE)
 - [SDC_GUT](#SDC_GUT)
+- [SEC_CHECK](#SEC_CHECK)
 - [SLANG_PLUGIN_PATH](#SLANG_PLUGIN_PATH)
 - [SYNTH_ARGS](#SYNTH_ARGS)
 - [SYNTH_BLACKBOXES](#SYNTH_BLACKBOXES)
@@ -590,6 +594,8 @@ configuration file.
 - [CDL_FILE](#CDL_FILE)
 - [GDS_ALLOW_EMPTY](#GDS_ALLOW_EMPTY)
 - [GND_NETS_VOLTAGES](#GND_NETS_VOLTAGES)
+- [LEC_AUX_VERILOG_FILES](#LEC_AUX_VERILOG_FILES)
+- [LEC_CHECK](#LEC_CHECK)
 - [MAX_ROUTING_LAYER](#MAX_ROUTING_LAYER)
 - [MIN_ROUTING_LAYER](#MIN_ROUTING_LAYER)
 - [POST_DENSITY_FILL_TCL](#POST_DENSITY_FILL_TCL)
@@ -599,6 +605,7 @@ configuration file.
 - [PWR_NETS_VOLTAGES](#PWR_NETS_VOLTAGES)
 - [REPORT_CLOCK_SKEW](#REPORT_CLOCK_SKEW)
 - [ROUTING_LAYER_ADJUSTMENT](#ROUTING_LAYER_ADJUSTMENT)
+- [SEC_CHECK](#SEC_CHECK)
 - [SKIP_DETAILED_ROUTE](#SKIP_DETAILED_ROUTE)
 - [SKIP_REPORT_METRICS](#SKIP_REPORT_METRICS)
 
diff --git a/flow/scripts/cts.tcl b/flow/scripts/cts.tcl
index 1378c9e7b9..d8393322cb 100644
--- a/flow/scripts/cts.tcl
+++ b/flow/scripts/cts.tcl
@@ -1,6 +1,6 @@
 utl::set_metrics_stage "cts__{}"
 source $::env(SCRIPTS_DIR)/load.tcl
-source $::env(SCRIPTS_DIR)/lec_check.tcl
+source $::env(SCRIPTS_DIR)/formal_check.tcl
 erase_non_stage_variables cts
 load_design 3_place.odb 3_place.sdc
 source_step_tcl PRE CTS
diff --git a/flow/scripts/final_report.tcl b/flow/scripts/final_report.tcl
index d81acc986e..c70492b72a 100644
--- a/flow/scripts/final_report.tcl
+++ b/flow/scripts/final_report.tcl
@@ -1,5 +1,6 @@
 utl::set_metrics_stage "finish__{}"
 source $::env(SCRIPTS_DIR)/load.tcl
+source $::env(SCRIPTS_DIR)/formal_check.tcl
 erase_non_stage_variables final
 load_design 6_1_fill.odb 6_1_fill.sdc
 source_step_tcl PRE FINAL_REPORT
@@ -19,6 +20,18 @@ write_def $::env(RESULTS_DIR)/6_final.def
 write_verilog $::env(RESULTS_DIR)/6_final.v \
   -remove_cells [find_physical_only_masters]
 
+if { $::env(LEC_CHECK) || $::env(SEC_CHECK) } {
+  write_lec_verilog 6_final_lec.v
+}
+
+if { $::env(LEC_CHECK) } {
+  run_lec_test 6_final 1_synth_lec.v 6_final_lec.v
+}
+
+if { $::env(SEC_CHECK) } {
+  run_sec_test 6_final 1_synth_lec.v 6_final_lec.v
+}
+
 # Run extraction and STA
 if {
   [env_var_exists_and_non_empty RCX_RULES]
diff --git a/flow/scripts/lec_check.tcl b/flow/scripts/formal_check.tcl
similarity index 59%
rename from flow/scripts/lec_check.tcl
rename to flow/scripts/formal_check.tcl
index 3b3384c055..fec16a5350 100644
--- a/flow/scripts/lec_check.tcl
+++ b/flow/scripts/formal_check.tcl
@@ -46,6 +46,29 @@ proc write_lec_script { step file1 file2 } {
   close $outfile
 }
 
+proc write_sec_script { step file1 file2 } {
+  set outfile [open "$::env(OBJECTS_DIR)/${step}_sec_test.yml" w]
+  puts $outfile "format: verilog"
+  puts $outfile "verification: sec"
+  puts $outfile "sec_engine: pdr"
+  puts $outfile "input_paths:"
+  puts $outfile "  - $::env(RESULTS_DIR)/${file1}"
+  puts $outfile "  - $::env(RESULTS_DIR)/${file2}"
+  puts $outfile "liberty_files:"
+  foreach libFile $::env(LIB_FILES) {
+    puts $outfile " - $libFile"
+  }
+  puts $outfile "log_file: $::env(LOG_DIR)/${step}_sec_check.log"
+  close $outfile
+}
+
+proc formal_check_label { step } {
+  if { [string equal $step 4_rsz] } {
+    return "Repair timing output"
+  }
+  return "Global output"
+}
+
 proc run_lec_test { step file1 file2 } {
   write_lec_script $step $file1 $file2
   # tclint-disable-next-line command-args
@@ -56,9 +79,27 @@ proc run_lec_test { step file1 file2 } {
     # This block executes if grep returns a non-zero exit code
     set count 0
   }
+  set label [formal_check_label $step]
+  if { $count > 0 } {
+    error "$label failed lec test"
+  } else {
+    puts "$label passed lec test"
+  }
+}
+
+proc run_sec_test { step file1 file2 } {
+  write_sec_script $step $file1 $file2
+  # tclint-disable-next-line command-args
+  eval exec $::env(KEPLER_FORMAL_EXE) --config $::env(OBJECTS_DIR)/${step}_sec_test.yml
+  try {
+    set count [exec grep -c "SEC found a counterexample" $::env(LOG_DIR)/${step}_sec_check.log]
+  } trap CHILDSTATUS {results options} {
+    # This block executes if grep returns a non-zero exit code
+    set count 0
+  }
   if { $count > 0 } {
-    error "Repair timing output failed lec test"
+    error "Global output failed sec test"
   } else {
-    puts "Repair timing output passed lec test"
+    puts "Global output passed sec test"
   }
 }
diff --git a/flow/scripts/synth_odb.tcl b/flow/scripts/synth_odb.tcl
index d6f53cda3e..c233f79b36 100644
--- a/flow/scripts/synth_odb.tcl
+++ b/flow/scripts/synth_odb.tcl
@@ -1,5 +1,6 @@
 utl::set_metrics_stage "floorplan__{}"
 source $::env(SCRIPTS_DIR)/load.tcl
+source $::env(SCRIPTS_DIR)/formal_check.tcl
 erase_non_stage_variables synth
 load_design 1_2_yosys.v 1_2_yosys.sdc
 source_step_tcl PRE SYNTH
@@ -31,3 +32,6 @@ orfs_write_db $::env(RESULTS_DIR)/1_synth.odb
 # which are read in here and a canonicalized version is written
 # out by OpenSTA that has no dependencies.
 orfs_write_sdc $::env(RESULTS_DIR)/1_synth.sdc
+if { $::env(LEC_CHECK) || $::env(SEC_CHECK) } {
+  write_lec_verilog 1_synth_lec.v
+}
diff --git a/flow/scripts/variables.json b/flow/scripts/variables.json
index 369ed53179..ec0d852bca 100644
--- a/flow/scripts/variables.json
+++ b/flow/scripts/variables.json
@@ -468,16 +468,20 @@
     "type": "string"
   },
   "LEC_AUX_VERILOG_FILES": {
-    "description": "Additional Verilog files (e.g. blackbox stubs) to include in LEC equivalence checks. Appended to the generated Verilog netlist before running the formal equivalence check.\n",
+    "description": "Additional Verilog files (e.g. blackbox stubs) to include in generated netlists for formal equivalence checks.\n",
     "stages": [
-      "cts"
+      "synth",
+      "cts",
+      "final"
     ]
   },
   "LEC_CHECK": {
     "default": 0,
-    "description": "Perform a formal equivalence check between before and after netlists. If this fails, report an issue to OpenROAD.\n",
+    "description": "Perform formal equivalence checks between before and after netlists. This checks CTS repair timing and the initial synthesis netlist against the final netlist. If this fails, report an issue to OpenROAD.\n",
     "stages": [
-      "cts"
+      "synth",
+      "cts",
+      "final"
     ]
   },
   "LIB_FILES": {
@@ -1081,6 +1085,14 @@
   "SEAL_GDS": {
     "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",
+    "stages": [
+      "synth",
+      "final"
+    ]
+  },
   "SETUP_MOVE_SEQUENCE": {
     "description": "Passed as -sequence to repair_timing. This should be a string of move keywords separated by commas.\n",
     "stages": [
diff --git a/flow/scripts/variables.yaml b/flow/scripts/variables.yaml
index 6eee57b4c2..3fe14d5242 100644
--- a/flow/scripts/variables.yaml
+++ b/flow/scripts/variables.yaml
@@ -1563,18 +1563,31 @@ WRITE_ODB_AND_SDC_EACH_STAGE:
   default: 1
 LEC_CHECK:
   description: >
-    Perform a formal equivalence check between before and after netlists.
-    If this fails, report an issue to OpenROAD.
+    Perform formal equivalence checks between before and after netlists.
+    This checks CTS repair timing and the initial synthesis netlist against
+    the final netlist. If this fails, report an issue to OpenROAD.
   default: 0
   stages:
+    - synth
     - cts
+    - final
+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
+  stages:
+    - synth
+    - final
 LEC_AUX_VERILOG_FILES:
   description: >
-    Additional Verilog files (e.g. blackbox stubs) to include in LEC
-    equivalence checks. Appended to the generated Verilog netlist before
-    running the formal equivalence check.
+    Additional Verilog files (e.g. blackbox stubs) to include in generated
+    netlists for formal equivalence checks.
   stages:
+    - synth
     - cts
+    - final
 REMOVE_CELLS_FOR_LEC:
   description: >
     String patterns directly passed to write_verilog -remove_cells <> for
diff --git a/flow/settings.mk b/flow/settings.mk
index 413a40682c..28a18b17e6 100644
--- a/flow/settings.mk
+++ b/flow/settings.mk
@@ -1,5 +1,6 @@
-# Enable LEC (Logical Equivalence Check) only if kepler-formal is installed.
+# Enable formal checks only if kepler-formal is installed.
 # kepler-formal is primarily an OpenROAD/ORFS developer tool, not an end-user
-# tool. End-users would typically run LEC transactionally at project completion,
-# not in every CI run where it wastes CI time.
+# tool. End-users would typically run these checks transactionally at project
+# completion, not in every CI run where it wastes CI time.
 export LEC_CHECK ?= $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)
+export SEC_CHECK ?= $(if $(wildcard $(KEPLER_FORMAL_EXE)),1,0)
diff --git a/tools/kepler-formal b/tools/kepler-formal
index b596df4121..d92cee701f 160000
--- a/tools/kepler-formal
+++ b/tools/kepler-formal
@@ -1 +1 @@
-Subproject commit b596df4121f2b13ac1b6fd03920a3b2053ae80f5
+Subproject commit d92cee701f2484e73aa388bcb1f137fe60b97539