diff --git a/.github/workflows/proof_ci.yaml b/.github/workflows/proof_ci.yaml
index f8596b83028..351c906da35 100644
--- a/.github/workflows/proof_ci.yaml
+++ b/.github/workflows/proof_ci.yaml
@@ -1,6 +1,6 @@
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 # SPDX-License-Identifier: MIT-0
-# CBMC starter kit 2.9
+# CBMC starter kit 2.10
 name: Run CBMC proofs
 on:
   push:
@@ -38,11 +38,11 @@ jobs:
       - name: Parse config file
         run: |
           CONFIG_FILE='.github/workflows/proof_ci_resources/config.yaml'
-          for setting in cadical-tag cbmc-version cbmc-viewer-version kissat-tag litani-version proofs-dir run-cbmc-proofs-command; do
+          for setting in cadical-tag cbmc-version cbmc-viewer-version kissat-tag litani-version z3-version bitwuzla-version proofs-dir run-cbmc-proofs-command; do
             VAR=$(echo $setting | tr "[:lower:]" "[:upper:]" | tr - _)
             echo "${VAR}"=$(yq .$setting $CONFIG_FILE) >> $GITHUB_ENV
           done
-      - name: Ensure CBMC, CBMC viewer, Litani versions have been specified
+      - name: Ensure CBMC, CBMC viewer, Litani, Z3, Bitwuzla versions have been specified
         shell: bash
         run: |
           should_exit=false
@@ -58,6 +58,22 @@ jobs:
             echo "You must specify a Litani version (e.g. 'latest' or '1.27.0')"
             should_exit=true
           fi
+          if [ "${{ env.Z3_VERSION }}" == "" ]; then
+            echo "You must specify a Z3 version (e.g. '4.13.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.Z3_VERSION }}" == "latest" ]; then
+            echo "Z3 latest not supported at this time. You must specify an exact Z3 version (e.g. '4.13.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.BITWUZLA_VERSION }}" == "" ]; then
+            echo "You must specify a Bitwuzla version (e.g. '0.5.0')"
+            should_exit=true
+          fi
+          if [ "${{ env.BITWUZLA_VERSION }}" == "latest" ]; then
+            echo "Bitwuzla latest not supported at this time. You must specify an exact version (e.g. '0.5.0')"
+            should_exit=true
+          fi
           if [[ "$should_exit" == true ]]; then exit 1; fi
       - name: Install latest CBMC
         if: ${{ env.CBMC_VERSION == 'latest' }}
@@ -84,7 +100,7 @@ jobs:
         run: |
           CBMC_VIEWER_REL="https://api.github.com/repos/model-checking/cbmc-viewer/releases/latest"
           CBMC_VIEWER_VERSION=$(curl -s $CBMC_VIEWER_REL --header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' | jq -r .name | sed  's/viewer-//')
-          pip3 install cbmc-viewer==$CBMC_VIEWER_VERSION
+          sudo pip3 install cbmc-viewer==$CBMC_VIEWER_VERSION
       - name: Install CBMC viewer ${{ env.CBMC_VIEWER_VERSION }}
         if: ${{ env.CBMC_VIEWER_VERSION != 'latest' }}
         shell: bash
@@ -92,7 +108,7 @@ jobs:
           sudo apt-get update
           sudo apt-get install --no-install-recommends --yes \
             build-essential universal-ctags
-          pip3 install cbmc-viewer==${{ env.CBMC_VIEWER_VERSION }}
+          sudo pip3 install cbmc-viewer==${{ env.CBMC_VIEWER_VERSION }}
       - name: Install latest Litani
         if: ${{ env.LITANI_VERSION == 'latest' }}
         shell: bash
@@ -114,6 +130,37 @@ jobs:
           sudo apt-get update
           sudo apt-get install --no-install-recommends --yes ./litani.deb
           rm ./litani.deb
+      - name: Install Z3 ${{ env.Z3_VERSION }}
+        if: ${{ env.Z3_VERSION != 'latest' }}
+        shell: bash
+        run: |
+          curl -o z3.zip -L \
+            https://github.com/Z3Prover/z3/releases/download/z3-${{ env.Z3_VERSION }}/z3-${{ env.Z3_VERSION }}-x64-glibc-2.31.zip
+          sudo apt-get install --no-install-recommends --yes unzip
+          unzip z3.zip
+          cd z3-${{ env.Z3_VERSION }}-x64-glibc-2.31/bin \
+            && echo "Adding $(pwd) to PATH for Z3" \
+            && echo "$(pwd)" >> $GITHUB_PATH
+          rm ../../z3.zip
+      - name: Build and Install Bitwuzla ${{ env.BITWUZLA_VERSION }}
+        if: ${{ env.BITWUZLA_VERSION != 'latest' }}
+        shell: bash
+        run: |
+          echo "Installing Bitwuzla dependencies"
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends --yes libgmp-dev cmake
+          sudo pip3 install meson
+          echo "Building Bitwuzla"
+          BITWUZLA_TAG_NAME=${{ env.BITWUZLA_VERSION }}
+          git clone https://github.com/bitwuzla/bitwuzla.git \
+            && cd bitwuzla \
+            && git checkout $BITWUZLA_TAG_NAME \
+            && ./configure.py \
+            && cd build \
+            && ninja;
+          cd src/main \
+            && echo "Adding $(pwd) to PATH for Bitwuzla" \
+            && echo "$(pwd)" >> $GITHUB_PATH
       - name: Install ${{ env.KISSAT_TAG }} kissat
         if: ${{ env.KISSAT_TAG != '' }}
         shell: bash
diff --git a/.github/workflows/proof_ci_resources/config.yaml b/.github/workflows/proof_ci_resources/config.yaml
index 0356dd1f288..6c44d965a6b 100644
--- a/.github/workflows/proof_ci_resources/config.yaml
+++ b/.github/workflows/proof_ci_resources/config.yaml
@@ -1,7 +1,9 @@
 cadical-tag: latest
-cbmc-version: "5.95.1"
+cbmc-version: "6.1.0"
 cbmc-viewer-version: latest
 kissat-tag: latest
 litani-version: latest
+z3-version: "4.13.0"
+bitwuzla-version: "0.5.0"
 proofs-dir: tests/cbmc/proofs
 run-cbmc-proofs-command: ./run-cbmc-proofs.py
diff --git a/tests/cbmc/proofs/Makefile-project-defines b/tests/cbmc/proofs/Makefile-project-defines
index 281dba0ffb6..d0e92588782 100644
--- a/tests/cbmc/proofs/Makefile-project-defines
+++ b/tests/cbmc/proofs/Makefile-project-defines
@@ -46,7 +46,6 @@ CHECKFLAGS += --pointer-primitive-check
 
 # We override abort() to be assert(0)
 PROOF_SOURCES += $(PROOF_STUB)/abort_override_assert_false.c
-REMOVE_FUNCTION_BODY += abort
 
 # Useful for setting unwind limits to one more than some value.
 addone = $(shell echo $$(( $(1) + 1)))
diff --git a/tests/cbmc/proofs/Makefile.common b/tests/cbmc/proofs/Makefile.common
index 43a3cab6aa6..f4faa231c26 100644
--- a/tests/cbmc/proofs/Makefile.common
+++ b/tests/cbmc/proofs/Makefile.common
@@ -259,6 +259,11 @@ CBMC_FLAG_FLUSH ?= --flush
 
 CBMCFLAGS += $(CBMC_FLAG_FLUSH)
 
+# CBMC 6.0.0 enables all standard checks by default, which can make coverage analysis
+# very slow. See https://github.com/diffblue/cbmc/issues/8389
+# For now, we disable these checks when generating coverage info.
+COVERFLAGS ?= --no-standard-checks
+
 # CBMC flags used for property checking
 
 CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK)
@@ -382,6 +387,7 @@ PROJECT_SOURCES ?=
 # PROOF_SOURCES is the list of proof source files to compile, including
 # the proof harness, and including any function stubs being used.
 PROOF_SOURCES ?=
+PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 # The number of seconds that CBMC should be allowed to run for before
 # being forcefully terminated. Currently, this is set to be less than
@@ -492,7 +498,6 @@ COMMA :=,
 # Set C compiler defines
 
 CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
-COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
 DEFINES += -DCBMC=1
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
diff --git a/tests/cbmc/proofs/s2n_array_new/Makefile b/tests/cbmc/proofs/s2n_array_new/Makefile
index 6cd64107a73..87a2c94ac76 100644
--- a/tests/cbmc/proofs/s2n_array_new/Makefile
+++ b/tests/cbmc/proofs/s2n_array_new/Makefile
@@ -25,6 +25,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/memset_havoc.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_client/Makefile b/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_client/Makefile
index cb7a239897c..39833089310 100644
--- a/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_client/Makefile
+++ b/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_client/Makefile
@@ -26,6 +26,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
diff --git a/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_server/Makefile b/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_server/Makefile
index 518b7eefddf..866f6f441b3 100644
--- a/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_server/Makefile
+++ b/tests/cbmc/proofs/s2n_dh_compute_shared_secret_as_server/Makefile
@@ -25,9 +25,11 @@ PROOF_SOURCES += $(OPENSSL_SOURCE)/bn_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_ensure.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
diff --git a/tests/cbmc/proofs/s2n_dh_generate_ephemeral_key/Makefile b/tests/cbmc/proofs/s2n_dh_generate_ephemeral_key/Makefile
index f57f5afb42a..b7f5e6b28c8 100644
--- a/tests/cbmc/proofs/s2n_dh_generate_ephemeral_key/Makefile
+++ b/tests/cbmc/proofs/s2n_dh_generate_ephemeral_key/Makefile
@@ -29,6 +29,7 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile b/tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile
index 08f38129a3e..7c3d58165d5 100644
--- a/tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile
+++ b/tests/cbmc/proofs/s2n_dh_p_g_Ys_to_dh_params/Makefile
@@ -31,6 +31,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_dh_params_check/Makefile b/tests/cbmc/proofs/s2n_dh_params_check/Makefile
index a1e4b14871d..334ae42c373 100644
--- a/tests/cbmc/proofs/s2n_dh_params_check/Makefile
+++ b/tests/cbmc/proofs/s2n_dh_params_check/Makefile
@@ -21,6 +21,7 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(OPENSSL_SOURCE)/dh_override.c
+PROOF_SOURCES += $(OPENSSL_SOURCE)/bn_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
@@ -28,6 +29,7 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_dh_params_copy/Makefile b/tests/cbmc/proofs/s2n_dh_params_copy/Makefile
index 9958084d620..9db65a488a9 100644
--- a/tests/cbmc/proofs/s2n_dh_params_copy/Makefile
+++ b/tests/cbmc/proofs/s2n_dh_params_copy/Makefile
@@ -29,6 +29,7 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_dh_params_free/Makefile b/tests/cbmc/proofs/s2n_dh_params_free/Makefile
index a9a497874de..23bc9c5499e 100644
--- a/tests/cbmc/proofs/s2n_dh_params_free/Makefile
+++ b/tests/cbmc/proofs/s2n_dh_params_free/Makefile
@@ -29,6 +29,7 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_dhe.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_free/Makefile b/tests/cbmc/proofs/s2n_free/Makefile
index c3812b54e4c..0d11a263432 100644
--- a/tests/cbmc/proofs/s2n_free/Makefile
+++ b/tests/cbmc/proofs/s2n_free/Makefile
@@ -29,6 +29,7 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 
diff --git a/tests/cbmc/proofs/s2n_free_object/Makefile b/tests/cbmc/proofs/s2n_free_object/Makefile
index 8e7bc5d0ac6..4517211c1d1 100644
--- a/tests/cbmc/proofs/s2n_free_object/Makefile
+++ b/tests/cbmc/proofs/s2n_free_object/Makefile
@@ -28,6 +28,7 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 
diff --git a/tests/cbmc/proofs/s2n_free_or_wipe/Makefile b/tests/cbmc/proofs/s2n_free_or_wipe/Makefile
index 4f30e96ef79..3cd080754c1 100644
--- a/tests/cbmc/proofs/s2n_free_or_wipe/Makefile
+++ b/tests/cbmc/proofs/s2n_free_or_wipe/Makefile
@@ -29,6 +29,7 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
 
diff --git a/tests/cbmc/proofs/s2n_hash_free/Makefile b/tests/cbmc/proofs/s2n_hash_free/Makefile
index 8bed36899ef..47028287c60 100644
--- a/tests/cbmc/proofs/s2n_hash_free/Makefile
+++ b/tests/cbmc/proofs/s2n_hash_free/Makefile
@@ -37,7 +37,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_hash_allow_md5_for_fips
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
 
 UNWINDSET +=
diff --git a/tests/cbmc/proofs/s2n_hash_update/Makefile b/tests/cbmc/proofs/s2n_hash_update/Makefile
index 4c5a539b6d0..203d16970a7 100644
--- a/tests/cbmc/proofs/s2n_hash_update/Makefile
+++ b/tests/cbmc/proofs/s2n_hash_update/Makefile
@@ -36,7 +36,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_digest
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_hash_digest_size
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_digest
 
 UNWINDSET +=
diff --git a/tests/cbmc/proofs/s2n_hmac_free/Makefile b/tests/cbmc/proofs/s2n_hmac_free/Makefile
index 2100f42af63..bb614e0ba6c 100644
--- a/tests/cbmc/proofs/s2n_hmac_free/Makefile
+++ b/tests/cbmc/proofs/s2n_hmac_free/Makefile
@@ -23,6 +23,7 @@ PROOF_SOURCES += $(OPENSSL_SOURCE)/bn_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/ec_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 
@@ -37,8 +38,6 @@ REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_init
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_hash_allow_md5_for_fips
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_hmac_free/s2n_hmac_free_harness.c b/tests/cbmc/proofs/s2n_hmac_free/s2n_hmac_free_harness.c
index c10f670b4d3..aeff29282ad 100644
--- a/tests/cbmc/proofs/s2n_hmac_free/s2n_hmac_free_harness.c
+++ b/tests/cbmc/proofs/s2n_hmac_free/s2n_hmac_free_harness.c
@@ -43,7 +43,7 @@ void s2n_hmac_free_harness()
         assert(state->inner_just_key.hash_impl->free != NULL);
         assert(state->outer.hash_impl->free != NULL);
         assert(state->outer_just_key.hash_impl->free != NULL);
-        
+
         if (s2n_is_in_fips_mode()) {
             assert(state->inner.digest.high_level.evp.ctx == NULL);
             assert(state->inner.digest.high_level.evp_md5_secondary.ctx == NULL);
@@ -93,7 +93,7 @@ void s2n_hmac_free_harness()
          */
         free_rc_keys_from_hash_state(&saved_inner_hash_state);
         free_rc_keys_from_hash_state(&saved_inner_just_key_hash_state);
-        free_rc_keys_from_hash_state(&saved_inner_hash_state);
+        free_rc_keys_from_hash_state(&saved_outer_hash_state);
         free_rc_keys_from_hash_state(&saved_outer_just_key_hash_state);
     }
     /* 3. free our heap-allocated `state` since `s2n_hash_free` only `free`s the contents. */
diff --git a/tests/cbmc/proofs/s2n_hmac_init/Makefile b/tests/cbmc/proofs/s2n_hmac_init/Makefile
index d08ff2430e1..9538174d3a6 100644
--- a/tests/cbmc/proofs/s2n_hmac_init/Makefile
+++ b/tests/cbmc/proofs/s2n_hmac_init/Makefile
@@ -17,12 +17,16 @@ PROOF_UID = s2n_hmac_init
 HARNESS_ENTRY = $(PROOF_UID)_harness
 HARNESS_FILE = $(HARNESS_ENTRY).c
 
+CBMC_OBJECT_BITS ?= 10
+
 PROOF_SOURCES += $(OPENSSL_SOURCE)/evp_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/md5_override.c
 PROOF_SOURCES += $(OPENSSL_SOURCE)/sha_override.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_is_in_fips_mode.c
+PROOF_SOURCES += $(PROOF_STUB)/s2n_libcrypto_is_awslc.c
+PROOF_SOURCES += $(PROOF_STUB)/darwin_check_fd_set_overflow.c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 
 PROJECT_SOURCES += $(SRCDIR)/crypto/s2n_hash.c
@@ -35,15 +39,9 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_reset
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_free
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_digest
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_update
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_free
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_new
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_reset
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_digest
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_update
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_allow_md5_for_fips
-REMOVE_FUNCTION_BODY += s2n_hash_allow_md5_for_fips
 
 # The upper bound limit for these loops is me maximum possible value for xor_pad_size field
 # in struct s2n_hmac_state (128) plus one. See definition for struct s2n_hmac_state
diff --git a/tests/cbmc/proofs/s2n_hmac_update/Makefile b/tests/cbmc/proofs/s2n_hmac_update/Makefile
index e5ff4fbc15b..70701519f7c 100644
--- a/tests/cbmc/proofs/s2n_hmac_update/Makefile
+++ b/tests/cbmc/proofs/s2n_hmac_update/Makefile
@@ -37,7 +37,6 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract these functions because manual inspection demonstrates they are unreachable.
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_evp_hash_digest
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_hash_digest_size
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_hash_c_s2n_low_level_hash_digest
 
 UNWINDSET +=
diff --git a/tests/cbmc/proofs/s2n_mem_cleanup/Makefile b/tests/cbmc/proofs/s2n_mem_cleanup/Makefile
index ca291de46fa..579f5a92400 100644
--- a/tests/cbmc/proofs/s2n_mem_cleanup/Makefile
+++ b/tests/cbmc/proofs/s2n_mem_cleanup/Makefile
@@ -29,8 +29,9 @@ PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
-REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
+REMOVE_FUNCTION_BODY +=
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_mem_init/Makefile b/tests/cbmc/proofs/s2n_mem_init/Makefile
index ee3596eff9c..ee12bcc2c53 100644
--- a/tests/cbmc/proofs/s2n_mem_init/Makefile
+++ b/tests/cbmc/proofs/s2n_mem_init/Makefile
@@ -22,6 +22,7 @@ PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract this function because manual inspection demonstrates it is unreachable.
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
diff --git a/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile b/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile
index db954284f82..bba60be57aa 100644
--- a/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_alloc/Makefile
@@ -26,6 +26,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_string/Makefile b/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_string/Makefile
index 0e009f40207..4973e76a372 100644
--- a/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_string/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_alloc_ro_from_string/Makefile
@@ -24,6 +24,8 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_text.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_copy/Makefile b/tests/cbmc/proofs/s2n_stuffer_copy/Makefile
index b9977b9e0c4..78fa8daf14d 100644
--- a/tests/cbmc/proofs/s2n_stuffer_copy/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_copy/Makefile
@@ -24,6 +24,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_extract_blob/Makefile b/tests/cbmc/proofs/s2n_stuffer_extract_blob/Makefile
index 7aadbf68947..d756a5b2b32 100644
--- a/tests/cbmc/proofs/s2n_stuffer_extract_blob/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_extract_blob/Makefile
@@ -23,6 +23,8 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 
 PROJECT_SOURCES += $(SRCDIR)/error/s2n_errno.c
@@ -34,7 +36,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract this function because manual inspection demonstrates it is unreachable.
-REMOVE_FUNCTION_BODY +=  s2n_blob_slice
+REMOVE_FUNCTION_BODY +=
 
 UNWINDSET +=
 
diff --git a/tests/cbmc/proofs/s2n_stuffer_free/Makefile b/tests/cbmc/proofs/s2n_stuffer_free/Makefile
index e486db6e5d8..dbfae88dcf5 100644
--- a/tests/cbmc/proofs/s2n_stuffer_free/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_free/Makefile
@@ -31,6 +31,7 @@ PROJECT_SOURCES += $(SRCDIR)/utils/s2n_mem.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_ensure.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_result.c
+PROJECT_SOURCES += $(SRCDIR)/utils/s2n_safety.c
 
 # We abstract this function because manual inspection demonstrates it is unreachable.
 REMOVE_FUNCTION_BODY += __CPROVER_file_local_s2n_mem_c_s2n_mem_cleanup_impl
diff --git a/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile b/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile
index 4a11bcc8189..e1ac1b1dde7 100644
--- a/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_growable_alloc/Makefile
@@ -24,6 +24,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c b/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c
index e1b5dbbd162..dacc51c8c57 100644
--- a/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c
+++ b/tests/cbmc/proofs/s2n_stuffer_printf/s2n_stuffer_printf_harness.c
@@ -23,6 +23,11 @@
 
 int nondet_int(void);
 
+/* The MacOS.sdk defines a macro called "vsnprintf" which breaks the
+ * function definition below, so make sure it's undef'd here.
+ */
+#undef vsnprintf
+
 int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
 {
     if (size > 0)
diff --git a/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile b/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile
index d5a9f516084..197796980c2 100644
--- a/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_private_key_from_pem/Makefile
@@ -52,6 +52,6 @@ REMOVE_FUNCTION_BODY += s2n_add_overflow
 UNWINDSET += strlen.0:5 # size of S2N_PEM_PKCS1_RSA_PRIVATE_KEY
 UNWINDSET += strncmp.0:5 # size of S2N_PEM_END_TOKEN
 UNWINDSET += __CPROVER_file_local_s2n_stuffer_pem_c_s2n_stuffer_pem_read_contents.11:$(call addone,$(MAX_BLOB_SIZE))
-UNWINDSET += s2n_stuffer_skip_to_char.3:$(call addone,$(MAX_BLOB_SIZE))
+UNWINDSET += s2n_stuffer_skip_to_char.0:$(call addone,$(MAX_BLOB_SIZE))
 
 include ../Makefile.common
diff --git a/tests/cbmc/proofs/s2n_stuffer_raw_write/Makefile b/tests/cbmc/proofs/s2n_stuffer_raw_write/Makefile
index 7f76ba4f14d..c6eecdec7ef 100644
--- a/tests/cbmc/proofs/s2n_stuffer_raw_write/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_raw_write/Makefile
@@ -22,6 +22,9 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_read_base64/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_base64/Makefile
index 54d2b65cd2e..d58aa0bc120 100644
--- a/tests/cbmc/proofs/s2n_stuffer_read_base64/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_read_base64/Makefile
@@ -26,6 +26,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile
index 527e2146b25..de878adf70e 100644
--- a/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_read_hex/Makefile
@@ -26,6 +26,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_read_line/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_line/Makefile
index 1da09371b7e..af71a41ee48 100644
--- a/tests/cbmc/proofs/s2n_stuffer_read_line/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_read_line/Makefile
@@ -26,6 +26,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_read_token/Makefile b/tests/cbmc/proofs/s2n_stuffer_read_token/Makefile
index 011dd35381d..ab8c054b957 100644
--- a/tests/cbmc/proofs/s2n_stuffer_read_token/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_read_token/Makefile
@@ -25,6 +25,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 
diff --git a/tests/cbmc/proofs/s2n_stuffer_recv_from_fd/Makefile b/tests/cbmc/proofs/s2n_stuffer_recv_from_fd/Makefile
index 33f0af8d613..d1dbe1ec2da 100644
--- a/tests/cbmc/proofs/s2n_stuffer_recv_from_fd/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_recv_from_fd/Makefile
@@ -24,6 +24,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/read.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_reserve/Makefile b/tests/cbmc/proofs/s2n_stuffer_reserve/Makefile
index 0a042b5988a..b60c92f86f6 100644
--- a/tests/cbmc/proofs/s2n_stuffer_reserve/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_reserve/Makefile
@@ -24,6 +24,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_reserve_space/Makefile b/tests/cbmc/proofs/s2n_stuffer_reserve_space/Makefile
index 6f34f7f018f..58669d39a4f 100644
--- a/tests/cbmc/proofs/s2n_stuffer_reserve_space/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_reserve_space/Makefile
@@ -25,6 +25,9 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/error/s2n_errno.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_reserve_uint16/Makefile b/tests/cbmc/proofs/s2n_stuffer_reserve_uint16/Makefile
index ea6cf169256..58354660f67 100644
--- a/tests/cbmc/proofs/s2n_stuffer_reserve_uint16/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_reserve_uint16/Makefile
@@ -23,6 +23,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 
diff --git a/tests/cbmc/proofs/s2n_stuffer_reserve_uint24/Makefile b/tests/cbmc/proofs/s2n_stuffer_reserve_uint24/Makefile
index e3f4f6e310c..38f0f17b27a 100644
--- a/tests/cbmc/proofs/s2n_stuffer_reserve_uint24/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_reserve_uint24/Makefile
@@ -23,6 +23,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 
diff --git a/tests/cbmc/proofs/s2n_stuffer_resize/Makefile b/tests/cbmc/proofs/s2n_stuffer_resize/Makefile
index 7be49e367f7..4dbaa98db62 100644
--- a/tests/cbmc/proofs/s2n_stuffer_resize/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_resize/Makefile
@@ -24,6 +24,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile b/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile
index 41b69d86b55..5f5e673310d 100644
--- a/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/Makefile
@@ -22,6 +22,8 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 
 PROJECT_SOURCES += $(SRCDIR)/error/s2n_errno.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_skip_write/Makefile b/tests/cbmc/proofs/s2n_stuffer_skip_write/Makefile
index 11735a22923..933228c81ad 100644
--- a/tests/cbmc/proofs/s2n_stuffer_skip_write/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_skip_write/Makefile
@@ -24,6 +24,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write/Makefile b/tests/cbmc/proofs/s2n_stuffer_write/Makefile
index e326b10df92..ad39ed44ebb 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write/Makefile
@@ -22,6 +22,9 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_base64/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_base64/Makefile
index 44f07ca60c2..e8cea785c8b 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_base64/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_base64/Makefile
@@ -26,6 +26,7 @@ PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/mlock.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/posix_memalign_override.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_bytes/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_bytes/Makefile
index 0a1bedffa74..3bc38d997c8 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_bytes/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_bytes/Makefile
@@ -22,6 +22,9 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/utils/s2n_blob.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile
index a09b7f8a6e8..c6c8c1d3974 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_hex/Makefile
@@ -26,6 +26,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_network_order/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_network_order/Makefile
index ba093b9041a..4ac20af933e 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_network_order/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_network_order/Makefile
@@ -22,6 +22,8 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
 PROOF_SOURCES += $(PROOF_STUB)/sysconf.c
 
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint16/Makefile
index de513abf4e9..80ad99457f6 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_uint16/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16/Makefile
@@ -23,6 +23,9 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile
index 255787c81b9..0fd96bd3162 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_uint16_hex/Makefile
@@ -23,6 +23,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint24/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint24/Makefile
index 0ee330db573..d5f36fd153f 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_uint24/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_uint24/Makefile
@@ -23,6 +23,9 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint32/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint32/Makefile
index bec46adf7eb..c0ef76ced01 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_uint32/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_uint32/Makefile
@@ -23,6 +23,9 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint64/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint64/Makefile
index 8e339851469..08465311f7b 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_uint64/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_uint64/Makefile
@@ -23,6 +23,9 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint8/Makefile
index 82fc51dd59f..975c8af6cf9 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_uint8/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8/Makefile
@@ -22,6 +22,9 @@ HARNESS_FILE = $(HARNESS_ENTRY).c
 PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_network_order.c
diff --git a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile
index 6a5695128fc..b943356821f 100644
--- a/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile
+++ b/tests/cbmc/proofs/s2n_stuffer_write_uint8_hex/Makefile
@@ -23,6 +23,9 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE)
 PROOF_SOURCES += $(PROOF_SOURCE)/cbmc_utils.c
 PROOF_SOURCES += $(PROOF_SOURCE)/make_common_datastructures.c
 PROOF_SOURCES += $(PROOF_STUB)/s2n_calculate_stacktrace.c
+PROOF_SOURCES += $(PROOF_STUB)/mlock.c
+PROOF_SOURCES += $(PROOF_STUB)/munlock.c
+PROOF_SOURCES += $(PROOF_STUB)/madvise.c
 
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer_hex.c
 PROJECT_SOURCES += $(SRCDIR)/stuffer/s2n_stuffer.c
diff --git a/tests/cbmc/sources/cbmc_utils.c b/tests/cbmc/sources/cbmc_utils.c
index d544391882c..733c87fb9e1 100644
--- a/tests/cbmc/sources/cbmc_utils.c
+++ b/tests/cbmc/sources/cbmc_utils.c
@@ -16,6 +16,7 @@
 #include <assert.h>
 #include <crypto/s2n_hash.h>
 #include <utils/s2n_mem.h>
+#include <utils/s2n_ensure.h>
 #include <cbmc_proof/cbmc_utils.h>
 
 /**
@@ -80,7 +81,7 @@ void assert_bytes_match(const uint8_t *const a, const uint8_t *const b, const si
     assert(!a == !b);
     if (len > 0 && a != NULL && b != NULL) {
         size_t i;
-        __CPROVER_assume(i < len && len < MAX_MALLOC); /* prevent spurious pointer overflows */
+        CONTRACT_ASSUME(i < len && len < MAX_MALLOC); /* prevent spurious pointer overflows */
         assert(a[ i ] == b[ i ]);
     }
 }
@@ -89,7 +90,7 @@ void assert_all_bytes_are(const uint8_t *const a, const uint8_t c, const size_t
 {
     if (len > 0 && a != NULL) {
         size_t i;
-        __CPROVER_assume(i < len);
+        CONTRACT_ASSUME(i < len);
         assert(a[ i ] == c);
     }
 }
@@ -110,7 +111,7 @@ void save_byte_from_array(const uint8_t *const array, const size_t size, struct
 {
     if (size > 0 && array && storage) {
         storage->idx = nondet_size_t();
-        __CPROVER_assume(storage->idx < size);
+        CONTRACT_ASSUME(storage->idx < size);
         storage->byte = array[ storage->idx ];
     }
 }
@@ -137,11 +138,11 @@ int uninterpreted_compare(const void *const a, const void *const b)
     assert(b != NULL);
     int rval = __CPROVER_uninterpreted_compare(a, b);
     /* Compare is reflexive */
-    __CPROVER_assume(IMPLIES(a == b, rval == 0));
+    CONTRACT_ASSUME(IMPLIES(a == b, rval == 0));
     /* Compare is anti-symmetric*/
-    __CPROVER_assume(__CPROVER_uninterpreted_compare(b, a) == -rval);
+    CONTRACT_ASSUME(__CPROVER_uninterpreted_compare(b, a) == -rval);
     /* If two things are equal, their hashes are also equal */
-    if (rval == 0) { __CPROVER_assume(__CPROVER_uninterpreted_hasher(a) == __CPROVER_uninterpreted_hasher(b)); }
+    if (rval == 0) { CONTRACT_ASSUME(__CPROVER_uninterpreted_hasher(a) == __CPROVER_uninterpreted_hasher(b)); }
     return rval;
 }
 
@@ -160,11 +161,11 @@ bool uninterpreted_equals(const void *const a, const void *const b)
 {
     bool rval = __CPROVER_uninterpreted_equals(a, b);
     /* Equals is reflexive */
-    __CPROVER_assume(IMPLIES(a == b, rval));
+    CONTRACT_ASSUME(IMPLIES(a == b, rval));
     /* Equals is symmetric */
-    __CPROVER_assume(__CPROVER_uninterpreted_equals(b, a) == rval);
+    CONTRACT_ASSUME(__CPROVER_uninterpreted_equals(b, a) == rval);
     /* If two things are equal, their hashes are also equal */
-    if (rval) { __CPROVER_assume(__CPROVER_uninterpreted_hasher(a) == __CPROVER_uninterpreted_hasher(b)); }
+    if (rval) { CONTRACT_ASSUME(__CPROVER_uninterpreted_hasher(a) == __CPROVER_uninterpreted_hasher(b)); }
     return rval;
 }
 
diff --git a/tests/cbmc/stubs/darwin_check_fd_set_overflow.c b/tests/cbmc/stubs/darwin_check_fd_set_overflow.c
new file mode 100644
index 00000000000..e1130b4f8d9
--- /dev/null
+++ b/tests/cbmc/stubs/darwin_check_fd_set_overflow.c
@@ -0,0 +1,25 @@
+/*
+ * 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 <cbmc_proof/nondet.h>
+
+/* A reference to this function appears as a side-effect of  */
+/* building on macOS with some versions of XCode installed   */
+/* A dummy stub is supplied here to prevent CBMC complaining */
+/* of a missing body.                                        */
+int __darwin_check_fd_set_overflow(int x, const void *y, int z)
+{
+    return nondet_int();
+}
diff --git a/tests/cbmc/stubs/s2n_is_in_fips_mode.c b/tests/cbmc/stubs/s2n_is_in_fips_mode.c
index 7ee61b05510..54b45dc71d2 100644
--- a/tests/cbmc/stubs/s2n_is_in_fips_mode.c
+++ b/tests/cbmc/stubs/s2n_is_in_fips_mode.c
@@ -17,7 +17,7 @@
 
 #include "crypto/s2n_fips.h"
 
-static bool flag = 0;
+static bool s2n_fips_mode_flag = 0;
 static bool s2n_fips_mode_enabled = 0;
 
 /**
@@ -26,9 +26,9 @@ static bool s2n_fips_mode_enabled = 0;
  */
 bool s2n_is_in_fips_mode()
 {
-    if (flag == 0) {
+    if (s2n_fips_mode_flag == 0) {
         s2n_fips_mode_enabled = nondet_bool() ? 1 : 0;
-        flag = 1;
+        s2n_fips_mode_flag = 1;
     }
     return s2n_fips_mode_enabled;
 }
diff --git a/utils/s2n_ensure.h b/utils/s2n_ensure.h
index 890cca162b5..866db937db0 100644
--- a/utils/s2n_ensure.h
+++ b/utils/s2n_ensure.h
@@ -135,15 +135,19 @@ void *s2n_ensure_memmove_trace(void *to, const void *from, size_t size);
  * Violations of the function contracts are undefined behaviour.
  */
 #ifdef CBMC
+    #define CONTRACT_ASSERT(...)      __CPROVER_assert(__VA_ARGS__)
     #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_REQUIRES(...)    __CPROVER_requires(__VA_ARGS__)
     #define CONTRACT_ENSURES(...)     __CPROVER_ensures(__VA_ARGS__)
     #define CONTRACT_INVARIANT(...)   __CPROVER_loop_invariant(__VA_ARGS__)
     #define CONTRACT_RETURN_VALUE     (__CPROVER_return_value)
 #else
+    #define CONTRACT_ASSERT(...)
     #define CONTRACT_ASSIGNS(...)
     #define CONTRACT_ASSIGNS_ERR(...)
+    #define CONTRACT_ASSUME(...)
     #define CONTRACT_REQUIRES(...)
     #define CONTRACT_ENSURES(...)
     #define CONTRACT_INVARIANT(...)