diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 00000000..6f6f76e7
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,103 @@
+name: Build & Test
+on:
+  pull_request:
+    branches: [main]
+  push:
+    branches: [main]
+jobs:
+    test:
+        name: Build & Test
+        runs-on: ${{ matrix.os }}
+        strategy:
+          fail-fast: false
+          matrix:
+            os: [ubuntu-latest, macos-latest]
+            ocaml-compiler: ['0', '1']
+        env:
+          EXAMPLES_DIR: "tlaplus-examples"
+          SCRIPT_DIR: "tlaplus-examples/.github/scripts"
+          DEPS_DIR: "tlaplus-examples/deps"
+          DIST_DIR: "tlatools/org.lamport.tlatools/dist"
+        steps:
+            - name: Clone repo
+              uses: actions/checkout@v4
+            - name: Install deps
+              if: matrix.os == 'ubuntu-latest'
+              run: |
+                sudo apt-get update
+                sudo apt-get install --yes time
+            - name: Set up Python
+              uses: actions/setup-python@v5
+              with:
+                python-version: '3.12'
+            - name: Get OCaml version
+              run: |
+                INDEX=${{ matrix.ocaml-compiler }}
+                OCAML_VERSION=\
+                `python .github/workflows/ocaml_versions.py $INDEX`
+                echo "OCAML_VERSION=$OCAML_VERSION" \
+                >> $GITHUB_ENV
+                echo "OCAML_VERSION = $OCAML_VERSION"
+            - uses: ocaml/setup-ocaml@v2
+              with:
+                ocaml-compiler: ${{ env.OCAML_VERSION }}
+            # - uses: actions/cache@v3
+            #   id: cache
+            #   with:
+            #     path: _build_cache
+            #     key: ${{ runner.os }}_build_cache
+            - name: Build TLAPM
+              run: |
+                eval $(opam env)
+                opam install ./ --deps-only --yes
+                make
+                make release
+            - name: Clone tlaplus/examples
+              uses: actions/checkout@v4
+              with:
+                repository: tlaplus/examples
+                path: ${{ env.EXAMPLES_DIR }}
+            - name: Check proofs in TLA+ examples
+              run: |
+                mkdir -p "$DEPS_DIR"
+                cp ./_build/tlaps*.tar.gz "$DEPS_DIR/tlaps.tar.gz"
+                tar -xzf "$DEPS_DIR/tlaps.tar.gz" -C "$DEPS_DIR"
+                rm "$DEPS_DIR/tlaps.tar.gz"
+                mv $DEPS_DIR/tlaps* "$DEPS_DIR/tlapm-install"
+                SKIP=(
+                  # Missing operator ENABLEDrules; will be fixed after
+                  # updated_enabled_cdot branch is merged.
+                  "specifications/ewd998/AsyncTerminationDetection.tla"
+                  # General proof failure
+                  "specifications/Bakery-Boulangerie/Bakery.tla"
+                  "specifications/Bakery-Boulangerie/Boulanger.tla"
+                  "specifications/bcastByz/bcastByz.tla"
+                  "specifications/byzpaxos/Consensus.tla"
+                  "specifications/byzpaxos/VoteProof.tla"
+                  "specifications/ewd998/AsyncTerminationDetection_proof.tla"
+                  "specifications/ewd998/EWD998_proof.tla"
+                  "specifications/LearnProofs/FindHighest.tla"
+                  "specifications/LoopInvariance/BinarySearch.tla"
+                  "specifications/LoopInvariance/Quicksort.tla"
+                  "specifications/LoopInvariance/SumSequence.tla"
+                  "specifications/MisraReachability/ReachabilityProofs.tla"
+                  "specifications/Paxos/Consensus.tla"
+                  "specifications/PaxosHowToWinATuringAward/Consensus.tla"
+                  "specifications/lamport_mutex/LamportMutex_proofs.tla"
+                  "specifications/TeachingConcurrency/SimpleRegular.tla"
+                  # Long-running
+                  "specifications/byzpaxos/BPConProof.tla" # Takes about 30 minutes
+                )
+                python "$SCRIPT_DIR/check_proofs.py"            \
+                  --tlapm_path "$DEPS_DIR/tlapm-install"        \
+                  --manifest_path "$EXAMPLES_DIR/manifest.json" \
+                  --skip "${SKIP[@]}"
+            - name: Run tests
+              run: |
+                eval $(opam env)
+                set +e
+                make test
+                TEST_RESULT=$?
+                cat _build/default/test/tests.log
+                exit $TEST_RESULT
+
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
deleted file mode 100644
index c01dc056..00000000
--- a/.github/workflows/main.yml
+++ /dev/null
@@ -1,67 +0,0 @@
-name: Build and Package TLA Proof Manager
-on:
-    push:
-    schedule:
-        - cron: '42 5 5 * *'
-jobs:
-    test:
-        name: Build TLAPS installer and test it
-        runs-on: ${{ matrix.operating-system }}
-        strategy:
-            matrix:
-                operating-system: [
-                    macos-latest,
-                    ubuntu-latest]
-                ocaml-compiler: [
-                    '0',
-                    '1',
-                    '2',
-                    ]
-        steps:
-            - name: Install deps
-              if: matrix.operating-system == 'ubuntu-latest'
-              run: |
-                sudo apt-get update
-                sudo apt-get install --yes time
-            - name: Set up Python
-              uses: actions/setup-python@v2
-              with:
-                python-version: '3.10'
-            - uses: actions/checkout@v2
-            - name: Get OCaml version
-              run: |
-                INDEX=${{ matrix.ocaml-compiler }}
-                OCAML_VERSION=\
-                `python .github/workflows/ocaml_versions.py $INDEX`
-                echo "OCAML_VERSION=$OCAML_VERSION" \
-                >> $GITHUB_ENV
-                echo "OCAML_VERSION = $OCAML_VERSION"
-            - uses: ocaml/setup-ocaml@v2
-              with:
-                ocaml-compiler: ${{ env.OCAML_VERSION }}
-            # - uses: actions/cache@v3
-            #   id: cache
-            #   with:
-            #     path: _build_cache
-            #     key: ${{ runner.os }}_build_cache
-            - name: Build installer of TLAPS
-              run: |
-                eval $(opam env)
-                opam install ./ --deps-only --yes
-                make
-                make release
-            - name: Run a subset of `tlapm` tests
-              run: |
-                eval $(opam env)
-                make test-inline test-fast-basic
-            - name: Run all `tlapm` tests
-              if: >-
-                matrix.operating-system == 'ubuntu-latest' &&
-                matrix.ocaml-compiler == '2'
-              run: |
-                eval $(opam env)
-                make test
-            - name: Print Test Results
-              if: matrix.operating-system == 'ubuntu-latest'
-              run: |
-                cat _build/default/test/tests.log
diff --git a/.github/workflows/ocaml_versions.py b/.github/workflows/ocaml_versions.py
index d7229ea9..339e6e2c 100644
--- a/.github/workflows/ocaml_versions.py
+++ b/.github/workflows/ocaml_versions.py
@@ -3,9 +3,8 @@
 
 
 OCAML_VERSIONS = [
-    '4.08.1',
-    '4.13.0',
-    '4.14.0',
+    '4.13.1',
+    '5.1.0',
     ]
 
 
diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml
deleted file mode 100644
index baafc9af..00000000
--- a/.github/workflows/pr.yml
+++ /dev/null
@@ -1,68 +0,0 @@
-name: Build on PR
-on:
-    pull_request:
-    push:
-        paths:
-            - '.github/workflows/pr.yml'
-    schedule:
-        - cron: '42 5 20 * *'
-jobs:
-    test:
-        name: Build and Test
-        runs-on: ${{ matrix.operating-system }}
-        strategy:
-            fail-fast: false
-            matrix:
-                operating-system: [
-                    macos-latest,
-                    ubuntu-latest]
-                ocaml-compiler: [
-                    '0',
-                    '1',
-                    '2',
-                    ]
-        steps:
-            - name: Install deps
-              if: matrix.operating-system == 'ubuntu-latest'
-              run: |
-                sudo apt-get update
-                sudo apt-get install --yes time
-            - name: Set up Python
-              uses: actions/setup-python@v2
-              with:
-                python-version: '3.10'
-            - uses: actions/checkout@v2
-            - name: Get OCaml version
-              run: |
-                INDEX=${{ matrix.ocaml-compiler }}
-                OCAML_VERSION=\
-                `python .github/workflows/ocaml_versions.py $INDEX`
-                echo "OCAML_VERSION=$OCAML_VERSION" \
-                >> $GITHUB_ENV
-                echo "OCAML_VERSION = $OCAML_VERSION"
-            - uses: ocaml/setup-ocaml@v2
-              with:
-                ocaml-compiler: ${{ env.OCAML_VERSION }}
-            # - uses: actions/cache@v3
-            #   id: cache
-            #   with:
-            #     path: _build_cache
-            #     key: ${{ runner.os }}_build_cache
-            - name: Build installer of TLAPS
-              run: |
-                eval $(opam env)
-                opam install ./ --deps-only --yes
-                make
-                make release
-            - name: Run a subset of `tlapm` tests
-              run: |
-                eval $(opam env)
-                make test-inline test-fast-basic
-            - name: Run all `tlapm` tests
-              run: |
-                eval $(opam env)
-                make test
-            - name: Print Test Results
-              if: matrix.operating-system == 'ubuntu-latest'
-              run: |
-                cat _build/default/test/tests.log