diff --git a/.github/workflows/cppverify-stability.py b/.github/workflows/cppverify-stability.py
new file mode 100755
index 0000000000..c224eefa33
--- /dev/null
+++ b/.github/workflows/cppverify-stability.py
@@ -0,0 +1,35 @@
+#!/usr/bin/env python3
+"""Compare the results of several runs of a lit suite (lit -o FILE.json).
+
+Prints each test whose result is not PASS, UNSUPPORTED, or XFAIL in some run,
+with its result in every run, and exits non-zero if there is one. A test whose
+results differ between runs is flaky: its verdict depends on more than the
+program, such as the load or the solver's search order.
+"""
+
+import json
+import sys
+
+GOOD = {"PASS", "UNSUPPORTED", "XFAIL"}
+
+runs = []
+for path in sys.argv[1:]:
+    with open(path) as f:
+        runs.append({t["name"]: t["code"] for t in json.load(f)["tests"]})
+
+names = sorted(set().union(*runs))
+flaky, failing = [], []
+for name in names:
+    codes = [run.get(name, "MISSING") for run in runs]
+    if all(code in GOOD for code in codes):
+        continue
+    (failing if len(set(codes)) == 1 else flaky).append((name, codes))
+
+print(f"{len(names)} tests, {len(runs)} runs: {len(flaky)} flaky, "
+      f"{len(failing)} failing in every run")
+for title, tests in (("Flaky", flaky), ("Failing in every run", failing)):
+    if tests:
+        print(f"\n{title}:")
+        for name, codes in tests:
+            print(f"  {name}: {' '.join(codes)}")
+sys.exit(1 if flaky or failing else 0)
diff --git a/.github/workflows/cppverify-stability.yml b/.github/workflows/cppverify-stability.yml
new file mode 100644
index 0000000000..98b539b487
--- /dev/null
+++ b/.github/workflows/cppverify-stability.yml
@@ -0,0 +1,109 @@
+name: CppVerify stability
+
+# Every night, the Verify suite runs five times on Linux and on macOS, at the
+# parallelism CI uses. A test whose result differs between runs has a verdict
+# that depends on more than the program, such as the load or the solver's
+# search order; the job fails and names it with its result in each run.
+
+on:
+  schedule:
+    - cron: "17 4 * * *"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+env:
+  CVC5_VERSION: "1.4.2"
+  RUNS: 5
+
+jobs:
+  linux:
+    name: Linux
+    runs-on: ubuntu-24.04
+    timeout-minutes: 355
+    env:
+      CCACHE_DIR: ${{ github.workspace }}/.ccache
+      CCACHE_MAXSIZE: 4G
+      CCACHE_COMPRESS: "1"
+    steps:
+      - name: Free disk space
+        run: sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL
+
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install build tools and cvc5
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y ninja-build ccache
+          curl -sSfL -o "$RUNNER_TEMP/cvc5.zip" \
+            "https://github.com/cvc5/cvc5/releases/download/cvc5-$CVC5_VERSION/cvc5-Linux-x86_64-static.zip"
+          unzip -q "$RUNNER_TEMP/cvc5.zip" -d "$RUNNER_TEMP/cvc5"
+          dirname "$(find "$RUNNER_TEMP/cvc5" -name cvc5 -type f)" >> "$GITHUB_PATH"
+
+      - uses: actions/cache/restore@v4
+        with:
+          path: .ccache
+          key: ccache-linux-release-${{ github.sha }}
+          restore-keys: ccache-linux-release-
+
+      - name: Configure
+        run: |
+          cmake -S llvm -B build -G Ninja \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DLLVM_ENABLE_PROJECTS=clang \
+            -DLLVM_TARGETS_TO_BUILD=Native \
+            -DCPPVERIFY_VENDOR_Z3=ON \
+            -DCPPVERIFY_PREFER_SYSTEM_Z3=OFF \
+            -DLLVM_ENABLE_ASSERTIONS=OFF \
+            -DLLVM_CCACHE_BUILD=ON
+
+      - name: Build
+        run: ninja -C build clang cpp-verify clang-format FileCheck not count split-file llvm-config
+
+      - name: Run the suite ${{ env.RUNS }} times
+        run: |
+          build/bin/cpp-verify --version
+          for run in $(seq "$RUNS"); do
+            build/bin/llvm-lit -s --no-progress-bar clang/test/Verify -o "run$run.json" || true
+          done
+          python3 .github/workflows/cppverify-stability.py run*.json
+
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: stability-linux
+          path: run*.json
+
+  macos:
+    name: macOS
+    runs-on: macos-14
+    timeout-minutes: 355
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install build tools
+        run: brew install ninja
+
+      - name: Build with setup.sh
+        run: |
+          ./setup.sh
+          ninja -C build FileCheck not count split-file llvm-config
+
+      - name: Run the suite ${{ env.RUNS }} times
+        run: |
+          build/bin/cpp-verify --version
+          for run in $(seq "$RUNS"); do
+            build/bin/llvm-lit -s --no-progress-bar clang/test/Verify -o "run$run.json" || true
+          done
+          python3 .github/workflows/cppverify-stability.py run*.json
+
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: stability-macos
+          path: run*.json