diff --git a/.github/scripts/linux-setup.sh b/.github/scripts/linux-setup.sh
index dbe729eb..419ab3d3 100755
--- a/.github/scripts/linux-setup.sh
+++ b/.github/scripts/linux-setup.sh
@@ -50,6 +50,7 @@ main() {
   mkdir -p "$DEPS_DIR/community"
   wget -nv https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar \
         -O "$DEPS_DIR/community/modules.jar"
+  unzip "$DEPS_DIR/community/modules.jar" -d "$DEPS_DIR/community"
   # Get TLAPS modules
   wget -nv https://github.com/tlaplus/tlapm/archive/main.tar.gz -O /tmp/tlapm.tar.gz
   tar -xzf /tmp/tlapm.tar.gz --directory "$DEPS_DIR"
diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 6999b008..cf626601 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -135,13 +135,17 @@ jobs:
       - name: Check proofs
         if: matrix.os != 'windows-latest' && !matrix.unicode
         run: |
-          # Extract community modules for TLAPM
-          mkdir -p $DEPS_DIR/community/modules
-          unzip -q -o $DEPS_DIR/community/modules.jar -d $DEPS_DIR/community/modules
-          python $SCRIPT_DIR/check_proofs.py                       \
-            --tlapm_path $DEPS_DIR/tlapm                           \
-            --community_modules_path $DEPS_DIR/community/modules   \
-            --examples_root .
+          set -o pipefail
+          find specifications -iname "manifest.json" -print0 \
+          | xargs --null --no-run-if-empty \
+          jq --join-output '
+            .modules
+            | map(select(has("proof")))
+            | map(select(.path != "specifications/LoopInvariance/SumSequence.tla"))
+            | map(.path + "\u0000")
+            | join("")' \
+          | xargs --verbose --null --no-run-if-empty -I {TLA_FILE} \
+          "$DEPS_DIR/tlapm/bin/tlapm" "{TLA_FILE}" -I "$DEPS_DIR/community" --stretch 5
       - name: Smoke-test manifest generation script
         run: |
           python $SCRIPT_DIR/generate_manifest.py \