diff --git a/.github/workflows/coverage.yaml b/.github/workflows/coverage.yaml
index a2bb2ac79d0..6751af38be4 100644
--- a/.github/workflows/coverage.yaml
+++ b/.github/workflows/coverage.yaml
@@ -179,3 +179,143 @@ jobs:
           files: build/html/coverage.info
           fail_ci_if_error: true
           verbose: true
+
+  # This job takes approximately 36 to 85 minutes
+  macOS-cache-build:
+    runs-on: macos-13
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        run: |
+          # maven is already installed and upgrading to a newer version yields
+          # symlink conflicts as previously reported in https://github.com/actions/runner-images/issues/4020
+          brew install cmake ninja flex bison lcov ccache z3
+      - name: Prepare ccache
+        uses: actions/cache@v4
+        with:
+          save-always: true
+          path: .ccache
+          key: ${{ runner.os }}-Coverage-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-Coverage-${{ github.ref }}
+            ${{ runner.os }}-Coverage
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure CMake CBMC build with coverage instrumentation parameters
+        run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=4 -DCMAKE_C_COMPILER=$(brew --prefix llvm@15)/bin/clang -DCMAKE_CXX_COMPILER=$(brew --prefix llvm@15)/bin/clang++
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=7G
+      - name: Execute CMake CBMC build
+        run: cmake --build build -- -j4
+      - name: Print ccache stats
+        run: ccache -s
+
+  # This job takes approximately 36 to 85 minutes
+  macOS-non-JBMC:
+    needs: macOS-cache-build
+    runs-on: macos-13
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        run: |
+          # maven is already installed and upgrading to a newer version yields
+          # symlink conflicts as previously reported in https://github.com/actions/runner-images/issues/4020
+          brew install cmake ninja flex bison lcov ccache z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc5 binary and make sure it can be deployed
+        run: |
+          curl -L https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS --output cvc5
+          chmod u+x cvc5
+          mv cvc5 /usr/local/bin
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache/restore@v4
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-Coverage-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-Coverage-${{ github.ref }}
+            ${{ runner.os }}-Coverage
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure CMake CBMC build with coverage instrumentation parameters
+        run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=4 -DCMAKE_C_COMPILER=$(brew --prefix llvm@15)/bin/clang -DCMAKE_CXX_COMPILER=$(brew --prefix llvm@15)/bin/clang++ -DCOVERAGE_CTEST_EXTRA_FLAGS="-E;^jbmc"
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=7G
+      - name: Execute CMake CBMC build
+        run: cmake --build build -- -j4
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run CTest and collect coverage statistics
+        run: |
+          echo "lcov_excl_line = UNREACHABLE" > ~/.lcovrc
+          cmake --build build --target coverage -- -j4
+      - name: Upload coverage statistics to Codecov
+        uses: codecov/codecov-action@v4
+        with:
+          token: ${{ secrets.CODECOV_TOKEN }}
+          files: build/html/coverage.info
+          fail_ci_if_error: true
+          verbose: true
+
+  # This job takes approximately 36 to 85 minutes
+  macOS-JBMC:
+    needs: macOS-cache-build
+    runs-on: macos-13
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        run: |
+          # maven is already installed and upgrading to a newer version yields
+          # symlink conflicts as previously reported in https://github.com/actions/runner-images/issues/4020
+          brew install cmake ninja flex bison lcov ccache z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc5 binary and make sure it can be deployed
+        run: |
+          curl -L https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS --output cvc5
+          chmod u+x cvc5
+          mv cvc5 /usr/local/bin
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache/restore@v4
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-Coverage-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-Coverage-${{ github.ref }}
+            ${{ runner.os }}-Coverage
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure CMake CBMC build with coverage instrumentation parameters
+        run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=4 -DCMAKE_C_COMPILER=$(brew --prefix llvm@15)/bin/clang -DCMAKE_CXX_COMPILER=$(brew --prefix llvm@15)/bin/clang++ -DCOVERAGE_CTEST_EXTRA_FLAGS="-R;^jbmc"
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=7G
+      - name: Execute CMake CBMC build
+        run: cmake --build build -- -j4
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run CTest and collect coverage statistics
+        run: |
+          echo "lcov_excl_line = UNREACHABLE" > ~/.lcovrc
+          cmake --build build --target coverage -- -j4
+      - name: Upload coverage statistics to Codecov
+        uses: codecov/codecov-action@v4
+        with:
+          token: ${{ secrets.CODECOV_TOKEN }}
+          files: build/html/coverage.info
+          fail_ci_if_error: true
+          verbose: true
diff --git a/src/goto-checker/witness_provider.h b/src/goto-checker/witness_provider.h
index 5037765a3d9..d25d80f8526 100644
--- a/src/goto-checker/witness_provider.h
+++ b/src/goto-checker/witness_provider.h
@@ -19,6 +19,10 @@ class goto_tracet;
 class witness_providert
 {
 public:
+  // Required to make lcov on macOS happy as otherwise it has no location for
+  // this definition (we don't have a .cpp file here).
+  witness_providert() = default;
+
   virtual ~witness_providert() = default;
 
   // Outputs an error witness in GraphML format (see `graphml_witnesst`)
diff --git a/src/goto-instrument/accelerate/path_enumerator.h b/src/goto-instrument/accelerate/path_enumerator.h
index 8afe105272c..125cfae44a3 100644
--- a/src/goto-instrument/accelerate/path_enumerator.h
+++ b/src/goto-instrument/accelerate/path_enumerator.h
@@ -20,7 +20,11 @@ Author: Matt Lewis
 
 class path_enumeratort
 {
- public:
+public:
+  // Required to make lcov on macOS happy as otherwise it has no location for
+  // this definition (we don't have a .cpp file here).
+  path_enumeratort() = default;
+
   virtual ~path_enumeratort()
   {
   }