diff --git a/.github/workflows/proof_ci_resources/config.yaml b/.github/workflows/proof_ci_resources/config.yaml
index 4a362f2db..83407e8d9 100644
--- a/.github/workflows/proof_ci_resources/config.yaml
+++ b/.github/workflows/proof_ci_resources/config.yaml
@@ -1,7 +1,7 @@
 # Use exact versions (instead of "latest") so we're not broken by surprise upgrades.
 cadical-tag: "rel-2.0.0" # tag of latest release: https://github.com/arminbiere/cadical/releases
-cbmc-version: "6.0.0" # semver of latest release: https://github.com/diffblue/cbmc/releases
-cbmc-viewer-version: "3.8" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases
+cbmc-version: "6.1.0" # semver of latest release: https://github.com/diffblue/cbmc/releases
+cbmc-viewer-version: "3.9" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases
 kissat-tag: "rel-3.1.1" # tag of latest release: https://github.com/arminbiere/kissat/releases
 litani-version: "1.29.0" # semver of latest release: https://github.com/awslabs/aws-build-accumulator/releases
 proofs-dir: verification/cbmc/proofs
diff --git a/source/posix/thread.c b/source/posix/thread.c
index af7fac84c..34b5dbe94 100644
--- a/source/posix/thread.c
+++ b/source/posix/thread.c
@@ -275,6 +275,25 @@ int aws_thread_launch(
             if (attr_return) {
                 goto cleanup;
             }
+        } else if (!options->stack_size) {
+            /**
+             * On some systems, the default stack size is too low (128KB on musl at the time of writing this), which can
+             * cause stack overflow when the dependency chain is long. Increase the stack size to at
+             * least 1MB, which is the default on Windows.
+             */
+            size_t min_stack_size = (size_t)1 * 1024 * 1024;
+            size_t current_stack_size;
+            attr_return = pthread_attr_getstacksize(attributes_ptr, &current_stack_size);
+            if (attr_return) {
+                goto cleanup;
+            }
+
+            if (current_stack_size < min_stack_size) {
+                attr_return = pthread_attr_setstacksize(attributes_ptr, min_stack_size);
+                if (attr_return) {
+                    goto cleanup;
+                }
+            }
         }
 
 /* AFAIK you can't set thread affinity on apple platforms, and it doesn't really matter since all memory
diff --git a/source/windows/device_random.c b/source/windows/device_random.c
index 6cb92d43e..0398241dd 100644
--- a/source/windows/device_random.c
+++ b/source/windows/device_random.c
@@ -5,26 +5,11 @@
 #include <aws/common/device_random.h>
 
 #include <aws/common/byte_buf.h>
-#include <aws/common/thread.h>
 
 #include <windows.h>
 
 #include <bcrypt.h>
 
-static BCRYPT_ALG_HANDLE s_alg_handle = NULL;
-static aws_thread_once s_rand_init = AWS_THREAD_ONCE_STATIC_INIT;
-
-static void s_init_rand(void *user_data) {
-    (void)user_data;
-    NTSTATUS status = 0;
-
-    status = BCryptOpenAlgorithmProvider(&s_alg_handle, BCRYPT_RNG_ALGORITHM, NULL, 0);
-
-    if (!BCRYPT_SUCCESS(status)) {
-        abort();
-    }
-}
-
 int aws_device_random_buffer(struct aws_byte_buf *output) {
     return aws_device_random_buffer_append(output, output->capacity - output->len);
 }
@@ -32,8 +17,6 @@ int aws_device_random_buffer(struct aws_byte_buf *output) {
 int aws_device_random_buffer_append(struct aws_byte_buf *output, size_t n) {
     AWS_PRECONDITION(aws_byte_buf_is_valid(output));
 
-    aws_thread_call_once(&s_rand_init, s_init_rand, NULL);
-
     size_t space_available = output->capacity - output->len;
     if (space_available < n) {
         AWS_POSTCONDITION(aws_byte_buf_is_valid(output));
@@ -47,7 +30,8 @@ int aws_device_random_buffer_append(struct aws_byte_buf *output, size_t n) {
     while (n > 0) {
         uint32_t capped_n = (uint32_t)aws_min_size(n, UINT32_MAX);
 
-        NTSTATUS status = BCryptGenRandom(s_alg_handle, output->buffer + output->len, capped_n, 0 /*flags*/);
+        NTSTATUS status =
+            BCryptGenRandom(NULL, output->buffer + output->len, capped_n, BCRYPT_USE_SYSTEM_PREFERRED_RNG);
 
         if (!BCRYPT_SUCCESS(status)) {
             output->len = original_len;