diff --git a/tests/cbmc/proofs/Makefile.common b/tests/cbmc/proofs/Makefile.common
index f4faa231c26..a34de06200a 100644
--- a/tests/cbmc/proofs/Makefile.common
+++ b/tests/cbmc/proofs/Makefile.common
@@ -4,7 +4,7 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
 
-CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.8.8
+CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.10+
 
 ################################################################
 # The CBMC Starter Kit depends on the files Makefile.common and
@@ -211,10 +211,13 @@ CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER)
 
 ifeq ($(strip $(ENABLE_POOLS)),)
   POOL =
+  INIT_POOLS =
 else ifeq ($(strip $(EXPENSIVE)),)
   POOL =
+  INIT_POOLS =
 else
   POOL = --pool expensive
+  INIT_POOLS = --pools expensive:1
 endif
 
 # Similar to the pool feature above. If Litani is new enough, enable
@@ -229,29 +232,31 @@ endif
 #
 # Each variable below controls a specific property checking flag
 # within CBMC. If desired, a property flag can be disabled within
-# a particular proof by nulling the corresponding variable. For
-# instance, the following line:
+# a particular proof by nulling the corresponding variable when CBMC's default
+# is not to perform such checks, or setting to --no-<CHECK>-check when CBMC's
+# default is to perform such checks. For instance, the following lines:
 #
-#     CHECK_FLAG_POINTER_CHECK =
+#     CBMC_FLAG_POINTER_CHECK = --no-pointer-check
+#     CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK =
 #
-# would disable the --pointer-check CBMC flag within:
+# would disable pointer checks and unsigned overflow checks with CBMC flag
+# within:
 #   * an entire project when added to Makefile-project-defines
 #   * a specific proof when added to the harness Makefile
 
-CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail
-CBMC_FLAG_MALLOC_FAIL_NULL ?= --malloc-fail-null
-CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check
+CBMC_FLAG_MALLOC_MAY_FAIL ?= # set to --no-malloc-may-fail to disable
+CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable
 CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
-CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check
+CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable
 CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check
 CBMC_FLAG_NAN_CHECK ?= --nan-check
-CBMC_FLAG_POINTER_CHECK ?= --pointer-check
+CBMC_FLAG_POINTER_CHECK ?= #set to --no-pointer-check to disable
 CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= --pointer-overflow-check
-CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= --pointer-primitive-check
-CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= --signed-overflow-check
-CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= --undefined-shift-check
+CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= # set to --no-pointer-primitive-check to disable
+CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= # set to --no-signed-overflow-check to disable
+CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= # set to --no-undefined-shift-check to disable
 CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check
-CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions
+CBMC_FLAG_UNWINDING_ASSERTIONS ?= # set to --no-unwinding-assertions to disable
 CBMC_DEFAULT_UNWIND ?= --unwind 1
 CBMC_FLAG_FLUSH ?= --flush
 
@@ -410,7 +415,7 @@ endif
 
 # Optional configuration library flags
 OPT_CONFIG_LIBRARY ?=
-CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_FLAG_MALLOC_FAIL_NULL) $(CBMC_STRING_ABSTRACTION)
+CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_STRING_ABSTRACTION)
 
 # Proof writers could add function contracts in their source code.
 # These contracts are ignored by default, but may be enabled in two distinct
@@ -456,6 +461,24 @@ ifdef APPLY_LOOP_CONTRACTS
   endif
 endif
 
+# The default unwind should only be used in DFCC mode without loop contracts.
+# When loop contracts are applied, we only unwind specified loops.
+# If any loops remain after loop contracts have been applied, CBMC might try
+# to unwind the program indefinetly, because we do not pass default unwind
+# (i.e., --unwind 1) to CBMC when in DFCC mode.
+# We must not use a default unwind command in DFCC mode, because contract instrumentation
+# introduces loops encoding write set inclusion checks that must be dynamically unwound during
+# symex.
+ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
+ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
+  UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
+  UNWIND_0500_DESC="$(PROOF_UID): unwinding specified subset of loops"
+else
+  UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
+  UNWIND_0500_DESC="$(PROOF_UID): unwinding all loops"
+endif
+endif
+
 # Silence makefile output (eg, long litani commands) unless VERBOSE is set.
 ifndef VERBOSE
     MAKEFLAGS := $(MAKEFLAGS) -s
@@ -609,7 +632,7 @@ $(REWRITTEN_SOURCES):
 # Build targets that make the relevant .goto files
 
 # Compile project sources
-$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
+$(PROJECT_GOTO)0100.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -621,7 +644,7 @@ $(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
 	  --description "$(PROOF_UID): building project binary"
 
 # Compile proof sources
-$(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
+$(PROOF_GOTO)0100.goto: $(PROOF_SOURCES)
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -633,7 +656,7 @@ $(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
 	  --description "$(PROOF_UID): building proof binary"
 
 # Remove function bodies from project sources
-$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
+$(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
@@ -645,7 +668,7 @@ $(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
 	  --description "$(PROOF_UID): removing function bodies from project sources"
 
 # Link project and proof sources into the proof harness
-$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
+$(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto
 	$(LITANI) add-job \
 	  --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \
 	  --inputs $^ \
@@ -656,7 +679,7 @@ $(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
 	  --description "$(PROOF_UID): linking project to proof"
 
 # Restrict function pointers
-$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
+$(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \
@@ -668,7 +691,7 @@ $(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
 	  --description "$(PROOF_UID): restricting function pointers in project sources"
 
 # Fill static variable with unconstrained values
-$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
+$(HARNESS_GOTO)0300.goto: $(HARNESS_GOTO)0200.goto
 ifneq ($(strip $(CODE_CONTRACTS)),)
 	$(LITANI) add-job \
 	  --command 'cp $^ $@' \
@@ -691,7 +714,7 @@ else
 endif
 
 # Link CPROVER library if DFCC mode is on
-$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
+$(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto
 ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
 	$(LITANI) add-job \
 	  --command \
@@ -714,17 +737,17 @@ else
 endif
 
 # Early unwind all loops on DFCC mode; otherwise, only unwind loops in proof and project code
-$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
+$(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto
 ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
 	$(LITANI) add-job \
 	  --command \
-	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
+	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
 	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
-	  --description "$(PROOF_UID): unwinding all loops"
+	  --description $(UNWIND_0500_DESC)
 else ifneq ($(strip $(CODE_CONTRACTS)),)
 	$(LITANI) add-job \
 	  --command \
@@ -740,14 +763,14 @@ else
 	  --command 'cp $^ $@' \
 	  --inputs $^ \
 	  --outputs $@ \
-	  --stdout-file $(LOGDIR)/linking-library-models-log.txt \
+	  --stdout-file $(LOGDIR)/unwind_loops-log.txt \
 	  --pipeline-name "$(PROOF_UID)" \
 	  --ci-stage build \
 	  --description "$(PROOF_UID): not unwinding loops"
 endif
 
 # Replace function contracts, check function contracts, instrument for loop contracts
-$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
+$(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
@@ -759,7 +782,7 @@ $(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
 	  --description "$(PROOF_UID): checking function contracts"
 
 # Omit initialization of unused global variables (reduces problem size)
-$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
+$(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
@@ -771,7 +794,7 @@ $(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
 	  --description "$(PROOF_UID): slicing global initializations"
 
 # Omit unused functions (sharpens coverage calculations)
-$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
+$(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto
 	$(LITANI) add-job \
 	  --command \
 	    '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
@@ -783,7 +806,7 @@ $(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
 	  --description "$(PROOF_UID): dropping unused functions"
 
 # Final name for proof harness
-$(HARNESS_GOTO).goto: $(HARNESS_GOTO)8.goto
+$(HARNESS_GOTO).goto: $(HARNESS_GOTO)0800.goto
 	$(LITANI) add-job \
 	  --command 'cp $< $@' \
 	  --inputs $^ \
@@ -799,7 +822,7 @@ ifdef CBMCFLAGS
   ifeq ($(strip $(CODE_CONTRACTS)),)
     CBMCFLAGS += $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY)
   else ifeq ($(strip $(USE_DYNAMIC_FRAMES)),)
-    CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY)
+    CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY)
   endif
 endif
 
@@ -820,6 +843,23 @@ $(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
 	  --stderr-file $(LOGDIR)/result-err-log.txt \
 	  --description "$(PROOF_UID): checking safety properties"
 
+$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  $(POOL) \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  $(MEMORY_PROFILING) \
+	  --ignore-returns 10 \
+	  --timeout $(CBMC_TIMEOUT) \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --tags "stats-group:safety checks" \
+	  --stderr-file $(LOGDIR)/result-err-log.txt \
+	  --description "$(PROOF_UID): checking safety properties"
+
 $(LOGDIR)/property.xml: $(HARNESS_GOTO).goto
 	$(LITANI) add-job \
 	  --command \
@@ -885,7 +925,7 @@ litani-path:
 _goto: $(HARNESS_GOTO).goto
 goto:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _goto
 	@ echo Running 'litani build'
@@ -894,7 +934,7 @@ goto:
 _result: $(LOGDIR)/result.txt
 result:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _result
 	@ echo Running 'litani build'
@@ -903,7 +943,7 @@ result:
 _property: $(LOGDIR)/property.xml
 property:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _property
 	@ echo Running 'litani build'
@@ -912,7 +952,7 @@ property:
 _coverage: $(LOGDIR)/coverage.xml
 coverage:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _coverage
 	@ echo Running 'litani build'
@@ -921,7 +961,7 @@ coverage:
 _report: $(PROOFDIR)/report
 report:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _report
 	@ echo Running 'litani build'
diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile b/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile
new file mode 100644
index 00000000000..923076301c7
--- /dev/null
+++ b/tests/cbmc/proofs/s2n_constant_time_equals_partial/Makefile
@@ -0,0 +1,45 @@
+#
+#
+# Licensed under the Apache License, Version 2.0 (the "License"). You may not use
+# this file except in compliance with the License. A copy of the License is
+# located at
+#
+#     http://aws.amazon.com/apache2.0/
+#
+# or in the "license" file accompanying this file. This file is distributed on an
+# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+# implied. See the License for the specific language governing permissions and
+# limitations under the License.
+
+
+# Use the default set of CBMC flags
+CHECKFLAGS +=
+
+PROOF_UID = s2n_constant_time_equals_partial
+HARNESS_ENTRY = $(PROOF_UID)_harness
+HARNESS_FILE = $(HARNESS_ENTRY).c
+
+# Uncomment and complete this if this function calls other functions that have pre- and post-conditions
+#USE_FUNCTION_CONTRACTS =
+
+CHECK_FUNCTION_CONTRACTS=$(PROOF_UID)
+FUNCTION_NAME = $(PROOF_UID)
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Use SMT back-end and disable default SAT backend
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--bitwuzla
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
+
+# Set Verbose=on to see what litani is actually running
+VERBOSE=on
+
+
+#PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
+REWRITTEN_SOURCES = $(PROOFDIR)/s2n_safety.i
+include ../Makefile.common
+$(PROOFDIR)/s2n_safety.i_SOURCE = $(SRCDIR)/utils/s2n_safety.c
+$(PROOFDIR)/s2n_safety.i_FUNCTIONS = s2n_constant_time_equals_partial
+$(PROOFDIR)/s2n_safety.i_OBJECTS =
diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_partial/cbmc-proof.txt b/tests/cbmc/proofs/s2n_constant_time_equals_partial/cbmc-proof.txt
new file mode 100644
index 00000000000..6ed46f1258c
--- /dev/null
+++ b/tests/cbmc/proofs/s2n_constant_time_equals_partial/cbmc-proof.txt
@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.
diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c b/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c
new file mode 100644
index 00000000000..1cc44ce2466
--- /dev/null
+++ b/tests/cbmc/proofs/s2n_constant_time_equals_partial/s2n_constant_time_equals_partial_harness.c
@@ -0,0 +1,33 @@
+/*
+ * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+#include <assert.h>
+
+#include "utils/s2n_safety.h"
+
+bool s2n_constant_time_equals_partial(const uint8_t* const a,
+                                      const uint8_t* const b,
+                                      const uint32_t len);
+
+void s2n_constant_time_equals_partial_harness()
+{
+    /* Non-deterministic inputs. */
+    uint32_t len;
+    uint8_t *a;
+    uint8_t *b;
+    bool result;
+
+    result = s2n_constant_time_equals_partial(a, b, len);
+}
diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile b/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile
new file mode 100644
index 00000000000..ef7006c952b
--- /dev/null
+++ b/tests/cbmc/proofs/s2n_constant_time_equals_total/Makefile
@@ -0,0 +1,44 @@
+#
+#
+# Licensed under the Apache License, Version 2.0 (the "License"). You may not use
+# this file except in compliance with the License. A copy of the License is
+# located at
+#
+#     http://aws.amazon.com/apache2.0/
+#
+# or in the "license" file accompanying this file. This file is distributed on an
+# "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+# implied. See the License for the specific language governing permissions and
+# limitations under the License.
+
+
+# Use the default set of CBMC flags
+CHECKFLAGS +=
+
+PROOF_UID = s2n_constant_time_equals_total
+HARNESS_ENTRY = $(PROOF_UID)_harness
+HARNESS_FILE = $(HARNESS_ENTRY).c
+
+# Uncomment and complete this if this function calls other functions that have pre- and post-conditions
+USE_FUNCTION_CONTRACTS = s2n_constant_time_equals_partial
+
+CHECK_FUNCTION_CONTRACTS=$(PROOF_UID)
+FUNCTION_NAME = $(PROOF_UID)
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Use SMT back-end and disable default SAT backend
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--bitwuzla
+
+# Tell CBMC not to name-mangle and export file-local symbols
+EXPORT_FILE_LOCAL_SYMBOLS=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
+
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
+
+# Set Verbose=on to see what litani is actually running
+VERBOSE=on
+
+include ../Makefile.common
diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_total/cbmc-proof.txt b/tests/cbmc/proofs/s2n_constant_time_equals_total/cbmc-proof.txt
new file mode 100644
index 00000000000..6ed46f1258c
--- /dev/null
+++ b/tests/cbmc/proofs/s2n_constant_time_equals_total/cbmc-proof.txt
@@ -0,0 +1 @@
+# This file marks this directory as containing a CBMC proof.
diff --git a/tests/cbmc/proofs/s2n_constant_time_equals_total/s2n_constant_time_equals_total_harness.c b/tests/cbmc/proofs/s2n_constant_time_equals_total/s2n_constant_time_equals_total_harness.c
new file mode 100644
index 00000000000..59c022e2cd5
--- /dev/null
+++ b/tests/cbmc/proofs/s2n_constant_time_equals_total/s2n_constant_time_equals_total_harness.c
@@ -0,0 +1,29 @@
+/*
+ * Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License").
+ * You may not use this file except in compliance with the License.
+ * A copy of the License is located at
+ *
+ *  http://aws.amazon.com/apache2.0
+ *
+ * or in the "license" file accompanying this file. This file is distributed
+ * on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
+ * express or implied. See the License for the specific language governing
+ * permissions and limitations under the License.
+ */
+
+#include <assert.h>
+
+#include "utils/s2n_safety.h"
+
+void s2n_constant_time_equals_total_harness()
+{
+    /* Non-deterministic inputs. */
+    uint32_t len;
+    uint8_t *a;
+    uint8_t *b;
+    bool result;
+
+    result = s2n_constant_time_equals_total(a, b, len);
+}
diff --git a/utils/s2n_ensure.h b/utils/s2n_ensure.h
index 866db937db0..5404f6ed520 100644
--- a/utils/s2n_ensure.h
+++ b/utils/s2n_ensure.h
@@ -139,6 +139,7 @@ void *s2n_ensure_memmove_trace(void *to, const void *from, size_t size);
     #define CONTRACT_ASSIGNS(...)     __CPROVER_assigns(__VA_ARGS__)
     #define CONTRACT_ASSIGNS_ERR(...) CONTRACT_ASSIGNS(__VA_ARGS__, _s2n_debug_info, s2n_errno)
     #define CONTRACT_ASSUME(...)      __CPROVER_assume(__VA_ARGS__)
+    #define CONTRACT_DECREASES(...)    __CPROVER_decreases(__VA_ARGS__)
     #define CONTRACT_REQUIRES(...)    __CPROVER_requires(__VA_ARGS__)
     #define CONTRACT_ENSURES(...)     __CPROVER_ensures(__VA_ARGS__)
     #define CONTRACT_INVARIANT(...)   __CPROVER_loop_invariant(__VA_ARGS__)
@@ -148,6 +149,7 @@ void *s2n_ensure_memmove_trace(void *to, const void *from, size_t size);
     #define CONTRACT_ASSIGNS(...)
     #define CONTRACT_ASSIGNS_ERR(...)
     #define CONTRACT_ASSUME(...)
+    #define CONTRACT_DECREASES(...)
     #define CONTRACT_REQUIRES(...)
     #define CONTRACT_ENSURES(...)
     #define CONTRACT_INVARIANT(...)
diff --git a/utils/s2n_safety.c b/utils/s2n_safety.c
index 6b2457b00bf..e07a4cf352c 100644
--- a/utils/s2n_safety.c
+++ b/utils/s2n_safety.c
@@ -78,6 +78,54 @@ bool s2n_constant_time_equals(const uint8_t *a, const uint8_t *b, const uint32_t
     return (xor == 0);
 }
 
+/* Returns true if a and b are equal. Execution time may depend on len */
+/* but not on the value of the data denoted by a or b                  */
+/* Note that if len == 0, then returns true                            */
+static bool s2n_constant_time_equals_partial(const uint8_t* const a,
+                                             const uint8_t* const b,
+                                             const uint32_t len)
+CONTRACT_REQUIRES(a != NULL && __CPROVER_is_fresh(a, len))
+CONTRACT_REQUIRES(b != NULL && __CPROVER_is_fresh(b, len))
+CONTRACT_ENSURES(CONTRACT_RETURN_VALUE == __CPROVER_forall { unsigned k; (k >= 0 && k < len) ==> (a[k] == b[k]) })
+{
+    bool arrays_equal = true;
+    /* iterate over each byte in the slices */
+    for (uint32_t i = 0; i < len; i++)
+    CONTRACT_ASSIGNS(i, arrays_equal)
+    CONTRACT_INVARIANT(i <= len)
+    CONTRACT_INVARIANT(arrays_equal ==
+                       __CPROVER_forall { uint32_t j; (j >= 0 && j < i) ==> (a[j] == b[j]) })
+    CONTRACT_DECREASES(len - i)
+    {
+        arrays_equal = arrays_equal && (a[i] == b[i]);
+    }
+
+    /* Substitute i = len into the loop invariant to get... */
+    CONTRACT_ASSERT(arrays_equal ==
+                    __CPROVER_forall { uint32_t j; (j >= 0 && j < len) ==> (a[j] == b[j]) },
+                    "Post-loop assertion");
+    return arrays_equal;
+}
+
+
+/*  See specification of this function in s2n_safety.h */
+bool s2n_constant_time_equals_total(const uint8_t *const a,
+                                    const uint8_t *const b,
+                                    const uint32_t len)
+{
+    if (len == 0) {
+        return true;
+    }
+
+    if (a == NULL || b == NULL) {
+        return false;
+    }
+
+    return s2n_constant_time_equals_partial(a, b, len);
+}
+
+
+
 /**
  * Given arrays "dest" and "src" of length "len", conditionally copy "src" to "dest"
  * The execution time of this function is independent of the values
diff --git a/utils/s2n_safety.h b/utils/s2n_safety.h
index d0ac5f2fc1a..d22c77b56c9 100644
--- a/utils/s2n_safety.h
+++ b/utils/s2n_safety.h
@@ -47,6 +47,28 @@ bool s2n_in_test();
 /* Returns true if a and b are equal, in constant time */
 bool s2n_constant_time_equals(const uint8_t* a, const uint8_t* b, const uint32_t len);
 
+/* If len == 0, then returns true, regardless of the values of a and b     */
+/*                                                                         */
+/* If len != 0 then                                                        */
+/*   If BOTH a and n are non-NULL then                                     */
+/*     Returns true if a and b are equal. Execution time may depend on len */
+/*     but not on the value of the data denoted by a or b.                 */
+/*                                                                         */
+/*   If either of a or b is NULL, then returns false                       */
+bool s2n_constant_time_equals_total(const uint8_t* const a,
+                                    const uint8_t* const b,
+                                    const uint32_t len)
+CONTRACT_REQUIRES(__CPROVER_is_fresh(a, len))
+CONTRACT_REQUIRES(__CPROVER_is_fresh(b, len))
+CONTRACT_ENSURES(((len == 0) && CONTRACT_RETURN_VALUE == true)
+                 ||
+                 ((len != 0 && a != NULL && b != NULL) &&
+                  CONTRACT_RETURN_VALUE == __CPROVER_forall { unsigned k; (k >= 0 && k < len) ==> (a[k] == b[k]) })
+                 ||
+                 ((len != 0) && (a == NULL || b == NULL) && CONTRACT_RETURN_VALUE == false)
+                );
+
+
 /* Copy src to dst, or don't copy it, in constant time */
 int s2n_constant_time_copy_or_dont(uint8_t* dst, const uint8_t* src, uint32_t len, uint8_t dont);