diff --git a/.github/workflows/cppverify-ci.yml b/.github/workflows/cppverify-ci.yml
index bc27cd732a..4ac61a2609 100644
--- a/.github/workflows/cppverify-ci.yml
+++ b/.github/workflows/cppverify-ci.yml
@@ -3,7 +3,8 @@ name: CppVerify CI
 # Linux runs every Clang and clang-tools-extra test in a release and an
 # assertions build, with the oldest and the newest cvc5 the release supports.
 # macOS and Windows build a fresh clone the way setup.sh and setup.ps1 do for
-# a user, then verify a program with the result.
+# a user, then verify a program with the result; macOS then runs the Verify
+# tests, with the newest cvc5 and the pinned Lean.
 
 on:
   # The book, the language reference, the website scripts, and DESIGN.md are
@@ -68,7 +69,8 @@ jobs:
             "https://github.com/cvc5/cvc5/releases/download/cvc5-${{ matrix.cvc5 }}/${{ matrix.cvc5-archive }}"
           unzip -q "$RUNNER_TEMP/cvc5.zip" -d "$RUNNER_TEMP/cvc5"
           dirname "$(find "$RUNNER_TEMP/cvc5" -name cvc5 -type f)" >> "$GITHUB_PATH"
-          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+          # elan v4.2.4.
+          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/227caca133724d5516bee25c2aeb3e609478f2d8/elan-init.sh \
             | sh -s -- -y --default-toolchain none
           # From its GitHub release: elan's own source, releases.lean-lang.org, may be down.
           version="${LEAN_TOOLCHAIN##*:v}"
@@ -142,8 +144,29 @@ jobs:
         with:
           submodules: recursive
 
-      - name: Install build tools
-        run: brew install ninja
+      - name: Install build tools, cvc5, and Lean
+        env:
+          CVC5_VERSION: "1.4.2"
+        run: |
+          set -o pipefail
+          brew install ninja
+          curl -sSfL -o "$RUNNER_TEMP/cvc5.zip" \
+            "https://github.com/cvc5/cvc5/releases/download/cvc5-$CVC5_VERSION/cvc5-macOS-arm64-static.zip"
+          unzip -q "$RUNNER_TEMP/cvc5.zip" -d "$RUNNER_TEMP/cvc5"
+          dirname "$(find "$RUNNER_TEMP/cvc5" -name cvc5 -type f)" >> "$GITHUB_PATH"
+          # elan v4.2.4.
+          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/227caca133724d5516bee25c2aeb3e609478f2d8/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          # From its GitHub release, as on Linux.
+          version="${LEAN_TOOLCHAIN##*:v}"
+          curl -sSfL -o "$RUNNER_TEMP/lean.zip" \
+            "https://github.com/leanprover/lean4/releases/download/v$version/lean-$version-darwin_aarch64.zip"
+          unzip -q "$RUNNER_TEMP/lean.zip" -d "$RUNNER_TEMP/lean"
+          mkdir -p "$HOME/.elan/toolchains"
+          mv "$RUNNER_TEMP/lean/lean-$version-darwin_aarch64" \
+            "$HOME/.elan/toolchains/leanprover--lean4---v$version"
+          "$HOME/.elan/bin/elan" default "$LEAN_TOOLCHAIN"
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
       - name: Build with setup.sh
         run: ./setup.sh
@@ -153,6 +176,8 @@ jobs:
 
       - name: Test the verifier
         run: |
+          cvc5 --version | head -1
+          lean --version
           ninja -C build FileCheck not count split-file llvm-config \
             cpp-verify-archive-fuzzer
           build/bin/llvm-lit -sv --no-progress-bar clang/test/Verify
@@ -169,10 +194,10 @@ jobs:
         with:
           submodules: recursive
 
-      - uses: ilammy/msvc-dev-cmd@v1
+      - uses: ilammy/msvc-dev-cmd@0b201ec74fa43914dc39ae48a89fd1d8cb592756 # v1.13.0
 
       - name: Install Ninja
-        run: choco install ninja --no-progress -y
+        run: choco install ninja --version 1.13.2 --allow-downgrade --no-progress -y
 
       - name: Build with setup.ps1
         shell: pwsh
diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp
index 459e978d75..674d0453cf 100644
--- a/clang/lib/Verify/Driver/Verifier.cpp
+++ b/clang/lib/Verify/Driver/Verifier.cpp
@@ -2643,7 +2643,8 @@ class LeanProject {
   // kernel rejected it. A goal with an error is elaborated with sorryAx. A
   // goal that takes longer than Limit, or stops Lean, is not proved, and the
   // goals after it start again in a new process; heartbeats bound no kernel
-  // check. Goals Lean cannot start on are left out.
+  // check. A goal's time starts when Lean has loaded the project's modules or
+  // finished the goal before. Goals Lean cannot start on are left out.
   std::map<std::string, LeanTrial>
   tryLeanGoals(const std::vector<const LeanProjectGoal *> &Goals,
                const std::string &Lean,
@@ -2751,8 +2752,9 @@ class LeanProject {
       bool TimedOut = false;
       while (true) {
         ChildPoll Poll = pollChild(Process, "Lean");
+        const bool WasStarted = Started;
         readReport();
-        if (Axioms.size() != Finished) {
+        if (Started != WasStarted || Axioms.size() != Finished) {
           Finished = Axioms.size();
           Progress = std::chrono::steady_clock::now();
         }
diff --git a/clang/test/Verify/suite/Inputs/lean_automation_slow_user.lean b/clang/test/Verify/suite/Inputs/lean_automation_slow_user.lean
new file mode 100644
index 0000000000..4c891a047d
--- /dev/null
+++ b/clang/test/Verify/suite/Inputs/lean_automation_slow_user.lean
@@ -0,0 +1,4 @@
+import CppVerify.Specs
+
+/- Loading this module takes 4 s, longer than the test gives one goal. -/
+initialize IO.sleep 4000
diff --git a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py
index 903c52aad2..ee28dd51a1 100644
--- a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py
+++ b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py
@@ -93,14 +93,41 @@ def fail(message):
     raise AssertionError(message)
 
 
-def run(command, expected_codes, timeout=180):
-    process = subprocess.run(
-        [str(argument) for argument in command],
-        stdout=subprocess.PIPE,
-        stderr=subprocess.STDOUT,
-        text=True,
-        timeout=timeout,
+# A guard against a hang, not a budget. cpp-verify gives each lake step of a
+# Lean build or certification 300 seconds, so a command that runs Lean gets
+# more than that.
+TIMEOUT = 180
+LEAN_TIMEOUT = 900
+
+
+def runs_lean(command):
+    return pathlib.Path(str(command[0])).name == "lake" or any(
+        str(argument).startswith(("--backend=lean", "--lean-"))
+        for argument in command
     )
+
+
+def run(command, expected_codes):
+    timeout = LEAN_TIMEOUT if runs_lean(command) else TIMEOUT
+    try:
+        process = subprocess.run(
+            [str(argument) for argument in command],
+            stdout=subprocess.PIPE,
+            stderr=subprocess.STDOUT,
+            text=True,
+            timeout=timeout,
+        )
+    except subprocess.TimeoutExpired as error:
+        output = error.output or ""
+        if isinstance(output, bytes):
+            output = output.decode(errors="replace")
+        fail(
+            "command timed out after {} seconds:\n{}\n{}".format(
+                timeout,
+                " ".join(str(argument) for argument in command),
+                output[-8000:],
+            )
+        )
     if process.returncode not in expected_codes:
         fail(
             "command returned {} instead of {}:\n{}\n{}".format(
diff --git a/clang/test/Verify/suite/lean_automation.test b/clang/test/Verify/suite/lean_automation.test
index 1ae7aeb4ef..a33499fb11 100644
--- a/clang/test/Verify/suite/lean_automation.test
+++ b/clang/test/Verify/suite/lean_automation.test
@@ -22,14 +22,14 @@
 # RUN: not test -e %t/p/.cppverify/automation
 #
 # An edited proof is the user's, kept as it is; it may use cppverify_auto.
-# RUN: sed -i 's/^  cppverify_auto_grind$/  cppverify_auto/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_postcondition_506f384e.lean
+# RUN: sed -i.orig 's/^  cppverify_auto_grind$/  cppverify_auto/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_postcondition_506f384e.lean
 # RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EDITED
 # RUN: grep -qx '  cppverify_auto' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_postcondition_506f384e.lean
 #
 # A stub that no revision of cppverify_auto tried, as before automation, and
 # one an earlier revision tried, are tried.
-# RUN: sed -i -e '/^   automation:/d' -e '/^import CppVerify.Goals\./d' -e '/^import CppVerify.Auto$/d' -e 's/^  cppverify_auto_grind$/  sorry/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean
-# RUN: sed -i 's/cppverify_auto 3 did not prove it/cppverify_auto 2 did not prove it/' %t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean
+# RUN: sed -i.orig -e '/^   automation:/d' -e '/^import CppVerify.Goals\./d' -e '/^import CppVerify.Auto$/d' -e 's/^  cppverify_auto_grind$/  sorry/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean
+# RUN: sed -i.orig 's/cppverify_auto 3 did not prove it/cppverify_auto 2 did not prove it/' %t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean
 # RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EDITED
 # RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean --check-prefix=TRIED
 # RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean --check-prefix=STUB
@@ -41,6 +41,11 @@
 # RUN: %cpp-verify --backend=lean --lean-project=%t/u --lean-auto-timeout=3000 --jobs=2 %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT
 # RUN: FileCheck %s --input-file=%t/u/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_overflow_fd7a6390.lean --check-prefix=HONEST
 #
+# A goal's time starts once Lean has loaded the project's modules, however
+# long that takes: here longer than the limit for one goal.
+# RUN: mkdir -p %t/load/CppVerify && cp %S/Inputs/lean_automation_slow_user.lean %t/load/CppVerify/User.lean
+# RUN: %cpp-verify --backend=lean --lean-project=%t/load --lean-auto-timeout=3000 --jobs=1 %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT
+#
 # Without automation every new goal gets a stub.
 # RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t/q %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=PLAIN --implicit-check-not=cppverify_auto
 # RUN: not grep -r -l 'automation:' %t/q/CppVerify/Proofs
diff --git a/clang/test/Verify/suite/lean_contract_certify.test b/clang/test/Verify/suite/lean_contract_certify.test
index 9823942ef9..926ca701a3 100644
--- a/clang/test/Verify/suite/lean_contract_certify.test
+++ b/clang/test/Verify/suite/lean_contract_certify.test
@@ -11,7 +11,7 @@
 # RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_contract_certify.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED
 #
 # The check's proof left a stub: the contract establishes nothing.
-# RUN: sed -i 's/^  omega$/  sorry/' %t/p/CppVerify/Proofs/cppverify_sensor_contract_eb6f5c/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean
+# RUN: sed -i.orig 's/^  omega$/  sorry/' %t/p/CppVerify/Proofs/cppverify_sensor_contract_eb6f5c/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean
 # RUN: not %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_contract_certify.cpp -- 2>&1 | FileCheck %s --check-prefix=STUB
 
 # EXPORT: Trusted: sensor (contract assumed, not verified)
diff --git a/clang/test/Verify/suite/lean_readable.cpp b/clang/test/Verify/suite/lean_readable.cpp
index 16bd3f0f2b..e9a66230cf 100644
--- a/clang/test/Verify/suite/lean_readable.cpp
+++ b/clang/test/Verify/suite/lean_readable.cpp
@@ -21,7 +21,7 @@
 //
 // A readable form that says less than its goal does not build: here the
 // definition of b is replaced by the conclusion it should lead to.
-// RUN: sed -i 's/(h_b_1 : b_1 = __local_call_2_1)/(h_b_1 : b_1 = x_0 + (BitVec.ofInt 32 (2)))/' %t/p/CppVerify/Goals/cppverify_twice_edf933.lean
+// RUN: sed -i.orig 's/(h_b_1 : b_1 = __local_call_2_1)/(h_b_1 : b_1 = x_0 + (BitVec.ofInt 32 (2)))/' %t/p/CppVerify/Goals/cppverify_twice_edf933.lean
 // RUN: cd %t/p && not lake build CppVerify.Generated 2>&1 | FileCheck %s --check-prefix=BRIDGE
 
 int next(int x)
diff --git a/clang/test/Verify/suite/lean_refutation.test b/clang/test/Verify/suite/lean_refutation.test
index d668d941d4..4c61bf4236 100644
--- a/clang/test/Verify/suite/lean_refutation.test
+++ b/clang/test/Verify/suite/lean_refutation.test
@@ -22,7 +22,7 @@
 #
 # A failure that is gone takes its refutation with it, as does a module of
 # no failure.
-# RUN: sed -i 's/return x + 2;/return x + 1;/' %t/r.cpp
+# RUN: sed -i.orig 's/return x + 2;/return x + 1;/' %t/r.cpp
 # RUN: not %cpp-verify --lean-fallback=%t/p %t/r.cpp -- 2>&1 | FileCheck %s --check-prefix=FIXED
 # RUN: not test -e %t/p/CppVerify/Refutations/cppverify_add_one_fc20c3
 # RUN: not test -e %t/p/CppVerify/Refutations/cppverify_fake_000000
diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
index 8801739d90..9ebfe68210 100644
--- a/docs/ARCHITECTURE.md
+++ b/docs/ARCHITECTURE.md
@@ -2483,8 +2483,9 @@ replay both drive it.
   proved each goal, then the axioms of its theorem or that the kernel
   rejected it (its messages, written by a thread of its own, are buffered and
   lost when it is stopped). A goal that takes longer than
-  `--lean-auto-timeout`, or stops Lean, is not proved, and the goals after it
-  start again in a new process. Each goal then gets the step that proved it
+  `--lean-auto-timeout`, counted from when Lean has loaded the project's
+  modules or finished the goal before, or stops Lean, is not proved, and the
+  goals after it start again in a new process. Each goal then gets the step that proved it
   (an automatic proof, pristine like a stub) or a stub whose header records
   the attempt. An export's `LeanAutomatic` counts its goals with automatic
   proofs. Without the toolchain nothing is tried.
diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
index 8d7f19bb6a..926cfb3c42 100644
--- a/website/source/language/tooling.rst
+++ b/website/source/language/tooling.rst
@@ -679,7 +679,8 @@ Backends
        on it. Requires ``--lean-project`` or ``--lean-fallback``.
    * - ``--lean-auto-timeout=N``
      - Milliseconds of wall-clock time ``cppverify_auto`` may spend on one
-       new goal, its kernel check included (default 20000; ``0`` disables). A
+       new goal, its kernel check included, counted once Lean has loaded the
+       project's modules (default 20000; ``0`` disables). A
        goal that takes longer gets a stub, as in ``automation:
        cppverify_auto 3 did not prove it within 20 s``. Requires
        ``--lean-project`` or ``--lean-fallback``.
diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst
index 773c07003b..ab311d905c 100644
--- a/website/source/release-notes.rst
+++ b/website/source/release-notes.rst
@@ -1029,6 +1029,11 @@ misbehaves on an input its precondition admits, when a counterexample does not
 reproduce, or when two backends decide differently
 (:doc:`book/part-ii/ch17-backends-modular-calls`).
 
+**cvc5 and Lean on macOS.** macOS CI installed neither, so the 36 tests that
+need cvc5 or Lean and run outside Linux, the backend fidelity gate among them,
+ran only on Linux. They now run on macOS too, with cvc5 1.4.2 and the pinned
+Lean.
+
 **Sanitizers every night.** The verifier's own code is now built with
 AddressSanitizer and UndefinedBehaviorSanitizer (``-DCPPVERIFY_SANITIZER``),
 and every Verify test program runs through that build every night; a report