diff --git a/.github/workflows/daily-soak-test-build.yml b/.github/workflows/daily-soak-test-build.yml
new file mode 100644
index 00000000000..98f9025f244
--- /dev/null
+++ b/.github/workflows/daily-soak-test-build.yml
@@ -0,0 +1,23 @@
+
+# Scheduled daily build
+#
+# The purpose of this build is to run tests that may have non-deterministic failures
+# many times over, in the hopes of more aggressively revealing
+# flaky tests that occasionally slow down unrelated development.
+
+name: Daily soak test workflow
+
+on:
+  schedule:
+    # Chosen to be hopefully outside of business hours for most contributors'
+    # time zones, and not on the hour to avoid heavy scheduled-job times:
+    # https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#schedule
+    - cron: "30 3 * * *"
+  workflow_dispatch:
+
+jobs:
+  daily-soak-build-for-master:
+    if: github.repository_owner == 'dafny-lang' || github.event_name == 'workflow_dispatch'
+    uses: ./.github/workflows/xunit-tests-reusable.yml
+    with:
+        soak_test: true
diff --git a/.github/workflows/xunit-tests-reusable.yml b/.github/workflows/xunit-tests-reusable.yml
index b4f7c95c86c..07934ea3bd4 100644
--- a/.github/workflows/xunit-tests-reusable.yml
+++ b/.github/workflows/xunit-tests-reusable.yml
@@ -2,7 +2,17 @@ name: Run XUnit tests
 
 on:
   workflow_dispatch:
+    inputs:
+      soak_test:
+        required: false
+        type: boolean
+        default: false
   workflow_call:
+    inputs:
+      soak_test:
+        required: false
+        type: boolean
+        default: false
 
 ## In the matrix:
 ##  os - name of the Github actions runner
@@ -15,13 +25,32 @@ defaults:
     working-directory: dafny
 
 jobs:
+  populate-matrix-dimensions:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Populate iterations (normal mode)
+        id: populate-iterations-normal
+        if: "!inputs.soak_test"
+        working-directory: .
+        run: echo "iterations=[1]" >> $GITHUB_OUTPUT
+      - name: Populate iterations (soak test mode)
+        id: populate-iterations-soak
+        if: inputs.soak_test
+        working-directory: .
+        run: echo "iterations=[`seq -s , 1 5`]" >> $GITHUB_OUTPUT
+    outputs:
+      iterations: ${{ steps.populate-iterations-normal.outputs.iterations }} ${{ steps.populate-iterations-soak.outputs.iterations }}
+  
   build:
+    needs: populate-matrix-dimensions
     runs-on: ${{matrix.os}}
     timeout-minutes: 60
-    name: ${{matrix.suffix}}
+    name: ${{matrix.suffix}} (${{matrix.iteration}})
     strategy:
       fail-fast: false
       matrix:
+        os: [ubuntu-20.04, windows-2019, macos-11]
+        iteration: ${{ fromJson(needs.populate-matrix-dimensions.outputs.iterations) }}
         include:
           - os: macos-11
             suffix: osx
@@ -66,27 +95,34 @@ jobs:
     - name: Build
       run: dotnet build --no-restore ${{env.solutionPath}}
     - name: Run DafnyCore Tests
+      if: "!inputs.soak_test"
       run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyCore.Test/coverlet.runsettings Source/DafnyCore.Test
-    - name: Run DafnyLanguageServer Tests
+    - name: Run DafnyLanguageServer Tests (soak test - iteration ${{matrix.iteration}})
+      if: inputs.soak_test
       run: |
-        ## Run twice to catch unstable code (Issue #2673)
         dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyLanguageServer.Test/coverlet.runsettings Source/DafnyLanguageServer.Test
-        ## On the second run, collect test coverage data
+    - name: Run DafnyLanguageServer Tests
+      if: "!inputs.soak_test"
+      run: |
         ##  Note that, for some mysterious reason, --collect doesn't work with the DafnyLanguageServer.Test package
         dotnet coverage collect -o DafnyLanguageServer.Test.coverage dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx Source/DafnyLanguageServer.Test
-
     - name: Run DafnyDriver Tests
+      if: "!inputs.soak_test"
       run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyDriver.Test/coverlet.runsettings Source/DafnyDriver.Test
     - name: Run DafnyPipeline Tests
+      if: "!inputs.soak_test"
       run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyPipeline.Test/coverlet.runsettings Source/DafnyPipeline.Test
     - name: Run DafnyTestGeneration Tests
+      if: "!inputs.soak_test"
       run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyTestGeneration.Test/coverlet.runsettings Source/DafnyTestGeneration.Test
     - name: Run AutoExtern Tests
+      if: "!inputs.soak_test"
       run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/AutoExtern.Test/coverlet.runsettings Source/AutoExtern.Test
     - name: Run DafnyRuntime Tests
+      if: "!inputs.soak_test"
       run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyRuntime.Tests/coverlet.runsettings Source/DafnyRuntime.Tests
     - uses: actions/upload-artifact@v4
-      if: always()
+      if: always() && !inputs.soak_test
       with:
         name: unit-test-results-${{ matrix.os }}
         path: |