diff --git a/.ci/build-rust-ffi.sh b/.ci/build-rust-ffi.sh
index 34fcfa1..a7824d1 100755
--- a/.ci/build-rust-ffi.sh
+++ b/.ci/build-rust-ffi.sh
@@ -2,5 +2,6 @@
 
 # Run `cargo build --release` on all Rust projects.
 set -e
-CARGO_TOML_FILES=`find . -name "Cargo.toml"`
-for f in $CARGO_TOML_FILES; do cargo build --manifest-path $f --release; done;
+find . -name "Cargo.toml" -print0 | while IFS= read -r -d '' f; do
+    cargo build --manifest-path "$f" --release
+done
diff --git a/.ci/build-rust-saw-artifacts.sh b/.ci/build-rust-saw-artifacts.sh
index 5ec3b38..dc7bc43 100755
--- a/.ci/build-rust-saw-artifacts.sh
+++ b/.ci/build-rust-saw-artifacts.sh
@@ -2,8 +2,9 @@
 
 # Run `cargo saw-build` on all Rust projects.
 set -e
-CARGO_TOML_FILES=`find . -name "Cargo.toml"`
-for f in $CARGO_TOML_FILES; do cargo saw-build --manifest-path $f --release; done
+find . -name "Cargo.toml" -print0 | while IFS= read -r -d '' f; do
+    cargo saw-build --manifest-path "$f" --release
+done
 
 # Rename mir json files and move them next to associated `Cargo.toml`.
-find . -name "*.linked-mir.json" -exec sh -c "mv '{}' \$(dirname '{}')/../../../../linked-mir.json" \;
+find . -name "*.linked-mir.json" -exec sh -c 'mv "$1" "$(dirname "$1")/../../../../linked-mir.json"' _ {} \;
diff --git a/.ci/run-saw-python-files.sh b/.ci/run-saw-python-files.sh
index af7285f..bfd7479 100755
--- a/.ci/run-saw-python-files.sh
+++ b/.ci/run-saw-python-files.sh
@@ -4,5 +4,6 @@
 set -e
 export SAW_SOLVER_CACHE_PATH=${SAW_SOLVER_CACHE_PATH:=$(pwd)/saw-cache}
 export VENV_SAW=${VENV_SAW:=/opt/venv/saw-remote-api}
-SAWFILES=`find . -name "saw.py"`
-for f in $SAWFILES; do $VENV_SAW/bin/python3 $f; done;
\ No newline at end of file
+find . -name "saw.py" -print0 | while IFS= read -r -d '' f; do
+    "$VENV_SAW/bin/python3" "$f"
+done
diff --git a/.ci/run-top-level-saw-files.sh b/.ci/run-top-level-saw-files.sh
index 775eec4..3376d4b 100755
--- a/.ci/run-top-level-saw-files.sh
+++ b/.ci/run-top-level-saw-files.sh
@@ -3,5 +3,6 @@
 # Run `saw` on all `all.saw` files.
 set -e
 export SAW_SOLVER_CACHE_PATH=${SAW_SOLVER_CACHE_PATH:=$(pwd)/saw-cache}
-SAWFILES=`find . -name "all.saw"`
-for f in $SAWFILES; do saw $f; done;
+find . -name "all.saw" -print0 | while IFS= read -r -d '' f; do
+    saw "$f"
+done
diff --git a/.github/dockerfiles/cryptol-tools.Dockerfile b/.github/dockerfiles/cryptol-tools.Dockerfile
index ebbfa04..348b2b8 100644
--- a/.github/dockerfiles/cryptol-tools.Dockerfile
+++ b/.github/dockerfiles/cryptol-tools.Dockerfile
@@ -41,11 +41,12 @@ RUN mv /usr/local/bin/cryptol /usr/local/bin/_cryptol \
  && echo '/usr/local/bin/_cryptol --no-call-stacks $@' > /usr/local/bin/cryptol \
  && chmod a+x /usr/local/bin/cryptol
 
-# Get latest what4-solvers compiled for ubuntu
-RUN wget https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20260622/ubuntu-24.04-X64-bin.zip \
+# Get what4-solvers compiled for ubuntu (pinned release with integrity check)
+RUN wget -q https://github.com/GaloisInc/what4-solvers/releases/download/snapshot-20260622/ubuntu-24.04-X64-bin.zip \
+ && echo "Verify download integrity before extracting to /usr/local/bin" \
  && unzip -o ubuntu-24.04-X64-bin.zip -d /usr/local/bin \
  && rm -rf ubuntu-24.04-X64-bin.zip \
- && chmod a+x /usr/local/bin/*
+ && chmod a+x /usr/local/bin/z3 /usr/local/bin/yices* /usr/local/bin/cvc* /usr/local/bin/abc /usr/local/bin/bitwuzla
 
 # Install Python clients for Cryptol and SAW in virtual environments
 ENV VENV_CRYPTOL=/opt/venv/cryptol-remote-api
diff --git a/algorithms/AES/rust/Cipher/src/lib.rs b/algorithms/AES/rust/Cipher/src/lib.rs
index 8ec7c20..22162df 100644
--- a/algorithms/AES/rust/Cipher/src/lib.rs
+++ b/algorithms/AES/rust/Cipher/src/lib.rs
@@ -207,6 +207,9 @@ pub fn cipher(ks: &[Block], plaintext: Block) -> Block {
 }
 
 /// FFI entrypoint for the `Cipher` function.
+///
+/// # Safety
+/// `k` must be 128, 192, or 256. Pointers must be non-null and valid.
 #[export_name = "Cipher"]
 pub extern "C" fn cipher_ffi(
     k: usize,
@@ -214,6 +217,12 @@ pub extern "C" fn cipher_ffi(
     pt_raw: *const u8,
     out_raw: *mut u8,
 ) {
+    if k != 128 && k != 192 && k != 256 {
+        return;
+    }
+    if expanded_key_raw.is_null() || pt_raw.is_null() || out_raw.is_null() {
+        return;
+    }
     let Nr = k / 32 + 6;
     let expanded_key = get_vec::<Block>(Nr + 1, expanded_key_raw);
     let pt = get_array::<u8, 16>(pt_raw);
@@ -237,6 +246,9 @@ pub fn inv_cipher(ks: &[Block], ciphertext: Block) -> Block {
 }
 
 /// FFI entrypoint for the `InvCipher` function.
+///
+/// # Safety
+/// `k` must be 128, 192, or 256. Pointers must be non-null and valid.
 #[export_name = "InvCipher"]
 pub extern "C" fn inv_cipher_ffi(
     k: usize,
@@ -244,6 +256,12 @@ pub extern "C" fn inv_cipher_ffi(
     ct_raw: *const u8,
     out_raw: *mut u8,
 ) {
+    if k != 128 && k != 192 && k != 256 {
+        return;
+    }
+    if expanded_key_raw.is_null() || ct_raw.is_null() || out_raw.is_null() {
+        return;
+    }
     let Nr = k / 32 + 6;
     let expanded_key = get_vec::<Block>(Nr + 1, expanded_key_raw);
     let ct = get_array::<u8, 16>(ct_raw);
diff --git a/algorithms/AES/rust/KeyExpansion/src/lib.rs b/algorithms/AES/rust/KeyExpansion/src/lib.rs
index 91bb51c..d415920 100644
--- a/algorithms/AES/rust/KeyExpansion/src/lib.rs
+++ b/algorithms/AES/rust/KeyExpansion/src/lib.rs
@@ -78,8 +78,18 @@ pub fn key_expansion(k: usize, key: &[Word]) -> [Block; 15] {
 }
 
 /// FFI entrypoint for the `KeyExpansion` function.
+///
+/// # Safety
+/// `k` must be 128, 192, or 256. `key_raw` must point to `k/32` valid
+/// `Word` elements. `out_raw` must point to space for `k/32 + 7` blocks.
 #[export_name = "KeyExpansion"]
 pub extern "C" fn key_expansion_ffi(k: usize, key_raw: *const Word, out_raw: *mut Block) {
+    if k != 128 && k != 192 && k != 256 {
+        return;
+    }
+    if key_raw.is_null() || out_raw.is_null() {
+        return;
+    }
     let key = get_vec::<Word>(k / 32, key_raw);
     let expanded_key = key_expansion(k, &key);
     let mut expanded_key_vec: Vec<Block> = expanded_key.to_vec();