From 3a04e9e21c78ac473c78b80d148cbde539abc054 Mon Sep 17 00:00:00 2001
From: Pantazis Deligiannis <pdeligia@microsoft.com>
Date: Mon, 4 Mar 2024 12:17:18 -0800
Subject: [PATCH] update the project to net8.0 (#497)

---
 .config/dotnet-tools.json                     |  6 +-
 .github/workflows/codeql-analysis.yml         |  4 +-
 .github/workflows/test-coyote.yml             |  8 +-
 .github/workflows/test-performance.yml        |  4 +-
 Common/build.props                            |  6 +-
 History.md                                    |  3 +
 Samples/CloudMessaging/run-mock.cmd           |  2 +-
 Samples/CloudMessaging/run-nondeterminism.cmd |  2 +-
 Samples/CloudMessaging/run.cmd                |  2 +-
 Samples/Common/TestDriver/rewrite.coyote.json |  2 +-
 Samples/Common/build.props                    |  2 +-
 Samples/README.md                             |  4 +-
 Samples/Scripts/run-tests.ps1                 |  2 +-
 .../ImageGallery/design.dgml                  | 18 ++--
 .../ImageGalleryAspNet/ImageGallery/readme.md |  2 +-
 .../ImageGalleryAspNet/rewrite.coyote.json    |  2 +-
 .../PetImages.Tests/PetImages.Tests.csproj    |  4 +-
 .../PetImages.Tests/rewrite.coyote.json       |  2 +-
 Scripts/CI/azure-nuget-sign-publish.yml       |  8 +-
 Scripts/common.psm1                           |  2 +-
 Scripts/gen-docs.ps1                          |  2 +-
 Scripts/run-benchmark-history.ps1             |  2 +-
 Scripts/run-benchmarks.ps1                    |  2 +-
 Scripts/run-tests.ps1                         | 18 ++--
 Source/Test/Rewriting/RewritingOptions.cs     |  6 +-
 .../Rewriting/Types/Threading/Interlocked.cs  |  4 +-
 Source/Test/Test.csproj                       |  6 +-
 Tests/compare-rewriting-diff-logs.ps1         |  2 +-
 Tests/get-rewriting-diff-logs.ps1             |  2 +-
 Tools/CLI/Coyote.CLI.csproj                   |  6 +-
 Tools/Coyote/Coyote.csproj                    |  6 +-
 docs/assets/images/RaftMocking.dgml           |  8 +-
 docs/assets/images/RaftMocking.svg            | 82 +++++++++----------
 docs/assets/images/cloudmessaging.dgml        |  8 +-
 docs/assets/images/cloudmessaging.svg         | 74 ++++++++---------
 docs/assets/images/core.dgml                  |  4 +-
 docs/concepts/binary-rewriting.md             |  4 +-
 docs/get-started/build-source.md              |  2 +-
 docs/get-started/install.md                   |  2 +-
 docs/get-started/using-coyote.md              |  2 +-
 docs/how-to/coverage.md                       |  6 +-
 docs/how-to/liveness-checking.md              |  4 +-
 docs/how-to/unit-testing.md                   |  2 +-
 .../actors/failover-robot-navigator.md        | 14 ++--
 docs/samples/actors/failure-detector.md       | 20 ++---
 docs/samples/tasks/bounded-buffer.md          |  6 +-
 docs/tutorials/actors/hello-world.md          | 14 ++--
 docs/tutorials/actors/raft-azure.md           |  4 +-
 docs/tutorials/actors/raft-mocking.md         | 14 ++--
 docs/tutorials/actors/test-failover.md        | 10 +--
 docs/tutorials/first-concurrency-unit-test.md |  4 +-
 docs/tutorials/mocks/mock-dependencies.md     |  2 +-
 .../mocks/optimistic-concurrency-control.md   |  2 +-
 docs/tutorials/test-concurrent-operations.md  |  2 +-
 docs/tutorials/test-failover.md               | 10 +--
 docs/tutorials/testing-aspnet-service.md      |  4 +-
 global.json                                   |  2 +-
 57 files changed, 228 insertions(+), 219 deletions(-)

diff --git a/.config/dotnet-tools.json b/.config/dotnet-tools.json
index fd3a04477..1a3d42bac 100644
--- a/.config/dotnet-tools.json
+++ b/.config/dotnet-tools.json
@@ -3,19 +3,19 @@
   "isRoot": true,
   "tools": {
     "dotnet-counters": {
-      "version": "6.0.351802",
+      "version": "8.0.510501",
       "commands": [
         "dotnet-counters"
       ]
     },
     "dotnet-dump": {
-      "version": "6.0.351802",
+      "version": "8.0.510501",
       "commands": [
         "dotnet-dump"
       ]
     },
     "dotnet-ilverify": {
-      "version": "7.0.0",
+      "version": "8.0.0",
       "commands": [
         "ilverify"
       ]
diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml
index 34b3d7c97..3c5c097b8 100644
--- a/.github/workflows/codeql-analysis.yml
+++ b/.github/workflows/codeql-analysis.yml
@@ -26,10 +26,10 @@ jobs:
       uses: NuGet/setup-nuget@v1
       with:
         nuget-version: '6.x'
-    - name: Setup .NET 7.0 SDK
+    - name: Setup .NET 8.0 SDK
       uses: actions/setup-dotnet@v1
       with:
-        dotnet-version: '7.0.x'
+        dotnet-version: '8.0.x'
     - name: Set environment variables
       run: echo "COYOTE_CLI_TELEMETRY_OPTOUT=1" >> $GITHUB_ENV
     # Initializes the CodeQL tools for scanning.
diff --git a/.github/workflows/test-coyote.yml b/.github/workflows/test-coyote.yml
index a48f02906..d7c46ac47 100644
--- a/.github/workflows/test-coyote.yml
+++ b/.github/workflows/test-coyote.yml
@@ -30,10 +30,10 @@ jobs:
         uses: NuGet/setup-nuget@v1
         with:
           nuget-version: '6.x'
-      - name: Setup .NET 7.0 SDK
+      - name: Setup .NET 8.0 SDK
         uses: actions/setup-dotnet@v1
         with:
-          dotnet-version: '7.0.x'
+          dotnet-version: '8.0.x'
       - name: Setup .NET 6.0 SDK
         uses: actions/setup-dotnet@v1
         with:
@@ -81,10 +81,10 @@ jobs:
       COYOTE_CLI_TELEMETRY_OPTOUT: 1
     steps:
       - uses: actions/checkout@v2
-      - name: Setup .NET 7.0 SDK
+      - name: Setup .NET 8.0 SDK
         uses: actions/setup-dotnet@v1
         with:
-          dotnet-version: '7.0.x'
+          dotnet-version: '8.0.x'
       - name: Download Coyote binaries
         uses: actions/download-artifact@v3
         with:
diff --git a/.github/workflows/test-performance.yml b/.github/workflows/test-performance.yml
index 271f0f38b..3482ef588 100644
--- a/.github/workflows/test-performance.yml
+++ b/.github/workflows/test-performance.yml
@@ -23,10 +23,10 @@ jobs:
         uses: NuGet/setup-nuget@v1
         with:
           nuget-version: '6.x'
-      - name: Setup .NET 7.0 SDK
+      - name: Setup .NET 8.0 SDK
         uses: actions/setup-dotnet@v1
         with:
-          dotnet-version: '7.0.x'
+          dotnet-version: '8.0.x'
       - name: Setup Powershell
         run: ./Scripts/install-pwsh.cmd
       - name: Build Coyote projects
diff --git a/Common/build.props b/Common/build.props
index a146c2cb6..b74642a73 100644
--- a/Common/build.props
+++ b/Common/build.props
@@ -16,10 +16,10 @@
     <PackageLicenseFile>LICENSE</PackageLicenseFile>
     <PackageOutputPath>$(MSBuildThisFileDirectory)/../bin/nuget</PackageOutputPath>
   </PropertyGroup>
-  <PropertyGroup Condition="'$(TargetFramework)' == 'net7.0' or '$(TargetFramework)' == 'net6.0'">
+  <PropertyGroup Condition="'$(TargetFramework)' == 'net8.0' or '$(TargetFramework)' == 'net6.0'">
     <LangVersion>10.0</LangVersion>
   </PropertyGroup>
-  <PropertyGroup Condition="'$(TargetFramework)' != 'net7.0' and '$(TargetFramework)' != 'net6.0'">
+  <PropertyGroup Condition="'$(TargetFramework)' != 'net8.0' and '$(TargetFramework)' != 'net6.0'">
     <LangVersion>8.0</LangVersion>
   </PropertyGroup>
   <PropertyGroup>
@@ -48,7 +48,7 @@
     <Net6Installed>false</Net6Installed>
     <Net6Installed Condition="$(GlobalVersion.StartsWith('6.0'))">true</Net6Installed>
     <Net6Installed Condition="'$(BUILD_NET6)'=='yes'">true</Net6Installed>
-    <TargetFrameworks>net7.0</TargetFrameworks>
+    <TargetFrameworks>net8.0</TargetFrameworks>
     <TargetFrameworks Condition="'$(NetStandard2Supported)'">$(TargetFrameworks);netstandard2.0</TargetFrameworks>
     <TargetFrameworks Condition="'$(NetCore31Installed)' and '$(NetCore31Supported)'">$(TargetFrameworks);netcoreapp3.1</TargetFrameworks>
     <TargetFrameworks Condition="'$(Net6Installed)' and '$(Net6Supported)'">$(TargetFrameworks);net6.0</TargetFrameworks>
diff --git a/History.md b/History.md
index b18271310..38a923c96 100644
--- a/History.md
+++ b/History.md
@@ -1,3 +1,6 @@
+## vNext
+- Added support for the `net8.0` target framework.
+
 ## v1.7.10
 - Fixed an issue with `Actor` not halting as expected in certain scenarios after explicitly raising
   a `HaltEvent` event.
diff --git a/Samples/CloudMessaging/run-mock.cmd b/Samples/CloudMessaging/run-mock.cmd
index 8baeb9389..54bad474d 100644
--- a/Samples/CloudMessaging/run-mock.cmd
+++ b/Samples/CloudMessaging/run-mock.cmd
@@ -1,2 +1,2 @@
 cd %~dp0
-dotnet ..\..\bin\net7.0\coyote.dll test /../bin/net7.0/Raft.Mocking.dll -i 1000 -ms 500 -graph-bug
+dotnet ..\..\bin\net8.0\coyote.dll test /../bin/net8.0/Raft.Mocking.dll -i 1000 -ms 500 -graph-bug
diff --git a/Samples/CloudMessaging/run-nondeterminism.cmd b/Samples/CloudMessaging/run-nondeterminism.cmd
index 6917ef129..3c201ef3c 100644
--- a/Samples/CloudMessaging/run-nondeterminism.cmd
+++ b/Samples/CloudMessaging/run-nondeterminism.cmd
@@ -1,2 +1,2 @@
 cd %~dp0
-dotnet ..\..\bin\net7.0\coyote.dll test ../bin/net7.0/Raft.Nondeterminism.dll -i 1000 -ms 500 -graph-bug
+dotnet ..\..\bin\net8.0\coyote.dll test ../bin/net8.0/Raft.Nondeterminism.dll -i 1000 -ms 500 -graph-bug
diff --git a/Samples/CloudMessaging/run.cmd b/Samples/CloudMessaging/run.cmd
index 15eb9ba91..087d83c94 100644
--- a/Samples/CloudMessaging/run.cmd
+++ b/Samples/CloudMessaging/run.cmd
@@ -1 +1 @@
-dotnet %~dp0\..\bin\net7.0\Raft.Azure.dll --connection-string %CONNECTION_STRING% --topic-name rafttopic --num-requests 5 --local-cluster-size 5 
+dotnet %~dp0\..\bin\net8.0\Raft.Azure.dll --connection-string %CONNECTION_STRING% --topic-name rafttopic --num-requests 5 --local-cluster-size 5 
diff --git a/Samples/Common/TestDriver/rewrite.coyote.json b/Samples/Common/TestDriver/rewrite.coyote.json
index 9a1028ab7..a4aa0a6f4 100644
--- a/Samples/Common/TestDriver/rewrite.coyote.json
+++ b/Samples/Common/TestDriver/rewrite.coyote.json
@@ -1,5 +1,5 @@
 {
-  "AssembliesPath": "../bin/net7.0",
+  "AssembliesPath": "../bin/net8.0",
   "Assemblies": [
     "AccountManager.dll",
     "AccountManager.ETags.dll",
diff --git a/Samples/Common/build.props b/Samples/Common/build.props
index cc18b0450..8d6beaccf 100644
--- a/Samples/Common/build.props
+++ b/Samples/Common/build.props
@@ -5,7 +5,7 @@
     <Company>Microsoft Corporation</Company>
     <Copyright>Copyright © Microsoft Corporation.</Copyright>
     <LangVersion>10.0</LangVersion>
-    <TargetFrameworks>net7.0</TargetFrameworks>
+    <TargetFrameworks>net8.0</TargetFrameworks>
     <UseLocalCoyote>False</UseLocalCoyote>
     <UseLocalNugetPackages>False</UseLocalNugetPackages>
     <UseNugetPackages>True</UseNugetPackages>
diff --git a/Samples/README.md b/Samples/README.md
index 7636cbacc..875331663 100644
--- a/Samples/README.md
+++ b/Samples/README.md
@@ -35,8 +35,8 @@ to build reliable applications and services:
 
 To build and run the samples, you will need to:
 
-- Install the [.NET 7.0 SDK](https://dotnet.microsoft.com/download/dotnet).
-- Install the [.NET 7.0 version of the coyote
+- Install the [.NET 8.0 SDK](https://dotnet.microsoft.com/download/dotnet).
+- Install the [.NET 8.0 version of the coyote
   tool](https://microsoft.github.io/coyote/get-started/install/).
 
 Once you are ready, build the samples by running the following script from the root of the
diff --git a/Samples/Scripts/run-tests.ps1 b/Samples/Scripts/run-tests.ps1
index 760099863..0d9e3cec0 100644
--- a/Samples/Scripts/run-tests.ps1
+++ b/Samples/Scripts/run-tests.ps1
@@ -7,7 +7,7 @@ CheckPSVersion
 
 Write-Comment -prefix "." -text "Testing the Coyote samples" -color "yellow"
 
-$framework = "net7.0"
+$framework = "net8.0"
 $tests = "$PSScriptRoot/../Common/bin/$framework/TestDriver.dll"
 if (-not (Test-Path $tests)) {
     Write-Error "tests for the Coyote samples not found."
diff --git a/Samples/WebApps/ImageGalleryAspNet/ImageGallery/design.dgml b/Samples/WebApps/ImageGalleryAspNet/ImageGallery/design.dgml
index b6d3d0596..713be1a95 100644
--- a/Samples/WebApps/ImageGalleryAspNet/ImageGallery/design.dgml
+++ b/Samples/WebApps/ImageGalleryAspNet/ImageGallery/design.dgml
@@ -617,7 +617,7 @@
     <Alias n="93" Id="(@1 @21 @44 Member=(Name=Create OverloadingParameters=[@43]))" />
     <Alias n="94" Id="(@1 @21 @44 Member=(Name=Update OverloadingParameters=[@43]))" />
     <Alias n="95" Id="(@1 @21 @67 Member=(Name=Store OverloadingParameters=[@76]))" />
-    <Alias n="96" Uri="Assembly=file:///C:/Program Files/dotnet/packs/Microsoft.NETCore.App.Ref/7.0.100/ref/net7.0/System.Runtime.dll" />
+    <Alias n="96" Uri="Assembly=file:///C:/Program Files/dotnet/packs/Microsoft.NETCore.App.Ref/8.0.200/ref/net8.0/System.Runtime.dll" />
     <Alias n="97" Id="(@96 Namespace=System Type=String)" />
     <Alias n="98" Id="OverloadingParameters=[@97]" />
     <Alias n="99" Id="(@1 @21 @44 Member=(Name=Get @98))" />
@@ -869,13 +869,13 @@
     </Style>
   </Styles>
   <Paths>
-    <Path Id="a5b18c87-5523-45ca-ad7c-ba9f9cd970f0.OutputPath" Value="C:\git\microsoft\CoyoteSamples\ImageGalleryAspNet\bin\net7.0\ImageGalleryClient.dll" />
-    <Path Id="a5b18c87-5523-45ca-ad7c-ba9f9cd970f0.OutputPathUri" Value="file:///C:/git/microsoft/CoyoteSamples/ImageGalleryAspNet/bin/net7.0/ImageGalleryClient.dll" />
-    <Path Id="b61697f0-7146-4c6a-8b6f-22f47731b799.OutputPath" Value="C:\git\microsoft\CoyoteSamples\ImageGalleryAspNet\bin\net7.0\ImageGalleryTests.dll" />
-    <Path Id="b61697f0-7146-4c6a-8b6f-22f47731b799.OutputPathUri" Value="file:///C:/git/microsoft/CoyoteSamples/ImageGalleryAspNet/bin/net7.0/ImageGalleryTests.dll" />
-    <Path Id="c1ca4fb9-7c59-425f-b437-04cc48ba1988.OutputPath" Value="C:\git\microsoft\CoyoteSamples\ImageGalleryAspNet\ImageGallery\bin\Debug\net7.0\ImageGallery.dll" />
-    <Path Id="c1ca4fb9-7c59-425f-b437-04cc48ba1988.OutputPathUri" Value="file:///C:/git/microsoft/CoyoteSamples/ImageGalleryAspNet/ImageGallery/bin/Debug/net7.0/ImageGallery.dll" />
-    <Path Id="e140c75e-8fc0-4c25-a744-2172d419a56a.OutputPath" Value="C:\git\microsoft\CoyoteSamples\ImageGalleryAspNet\bin\net7.0\ImageGalleryService.dll" />
-    <Path Id="e140c75e-8fc0-4c25-a744-2172d419a56a.OutputPathUri" Value="file:///C:/git/microsoft/CoyoteSamples/ImageGalleryAspNet/bin/net7.0/ImageGalleryService.dll" />
+    <Path Id="a5b18c87-5523-45ca-ad7c-ba9f9cd970f0.OutputPath" Value="C:\git\microsoft\CoyoteSamples\ImageGalleryAspNet\bin\net8.0\ImageGalleryClient.dll" />
+    <Path Id="a5b18c87-5523-45ca-ad7c-ba9f9cd970f0.OutputPathUri" Value="file:///C:/git/microsoft/CoyoteSamples/ImageGalleryAspNet/bin/net8.0/ImageGalleryClient.dll" />
+    <Path Id="b61697f0-7146-4c6a-8b6f-22f47731b799.OutputPath" Value="C:\git\microsoft\CoyoteSamples\ImageGalleryAspNet\bin\net8.0\ImageGalleryTests.dll" />
+    <Path Id="b61697f0-7146-4c6a-8b6f-22f47731b799.OutputPathUri" Value="file:///C:/git/microsoft/CoyoteSamples/ImageGalleryAspNet/bin/net8.0/ImageGalleryTests.dll" />
+    <Path Id="c1ca4fb9-7c59-425f-b437-04cc48ba1988.OutputPath" Value="C:\git\microsoft\CoyoteSamples\ImageGalleryAspNet\ImageGallery\bin\Debug\net8.0\ImageGallery.dll" />
+    <Path Id="c1ca4fb9-7c59-425f-b437-04cc48ba1988.OutputPathUri" Value="file:///C:/git/microsoft/CoyoteSamples/ImageGalleryAspNet/ImageGallery/bin/Debug/net8.0/ImageGallery.dll" />
+    <Path Id="e140c75e-8fc0-4c25-a744-2172d419a56a.OutputPath" Value="C:\git\microsoft\CoyoteSamples\ImageGalleryAspNet\bin\net8.0\ImageGalleryService.dll" />
+    <Path Id="e140c75e-8fc0-4c25-a744-2172d419a56a.OutputPathUri" Value="file:///C:/git/microsoft/CoyoteSamples/ImageGalleryAspNet/bin/net8.0/ImageGalleryService.dll" />
   </Paths>
 </DirectedGraph>
\ No newline at end of file
diff --git a/Samples/WebApps/ImageGalleryAspNet/ImageGallery/readme.md b/Samples/WebApps/ImageGalleryAspNet/ImageGallery/readme.md
index 5c4be451c..959629b83 100644
--- a/Samples/WebApps/ImageGalleryAspNet/ImageGallery/readme.md
+++ b/Samples/WebApps/ImageGalleryAspNet/ImageGallery/readme.md
@@ -8,7 +8,7 @@ This is a web client front end that uses the ImageGalleryService middle tier.
 
 The app depends on the following:
 
-- [.NET 7.0 SDK](https://dotnet.microsoft.com/download/dotnet) must be installed.
+- [.NET 8.0 SDK](https://dotnet.microsoft.com/download/dotnet) must be installed.
 - [Azure Storage Emulator](https://docs.microsoft.com/en-us/azure/storage/common/storage-use-emulator) must be hnstalled running.
 - [Azure Cosmos Emulator](https://docs.microsoft.com/en-us/azure/cosmos-db/local-emulator?tabs=cli%2Cssl-netstd21) must be installed and running.
 - Open Azure Cosmos Data Explorer from taskbar tray and copy the `Primary Connection String` from there into `~/ImageGalleryAspNet/ImageGalleryService/appsettings.json`.
diff --git a/Samples/WebApps/ImageGalleryAspNet/rewrite.coyote.json b/Samples/WebApps/ImageGalleryAspNet/rewrite.coyote.json
index 14ce638a7..6beb421ac 100644
--- a/Samples/WebApps/ImageGalleryAspNet/rewrite.coyote.json
+++ b/Samples/WebApps/ImageGalleryAspNet/rewrite.coyote.json
@@ -1,5 +1,5 @@
 {
-  "AssembliesPath": "./bin/net7.0",
+  "AssembliesPath": "./bin/net8.0",
   "OutputPath": "./bin/coyote",
   "Assemblies": [
       "ImageGalleryService.dll",
diff --git a/Samples/WebApps/PetImagesAspNet/PetImages.Tests/PetImages.Tests.csproj b/Samples/WebApps/PetImagesAspNet/PetImages.Tests/PetImages.Tests.csproj
index 02b075ac4..7609f2872 100644
--- a/Samples/WebApps/PetImagesAspNet/PetImages.Tests/PetImages.Tests.csproj
+++ b/Samples/WebApps/PetImagesAspNet/PetImages.Tests/PetImages.Tests.csproj
@@ -10,8 +10,8 @@
     <ProjectReference Include="..\PetImages\PetImages.csproj" />
   </ItemGroup>
   <ItemGroup>
-    <PackageReference Include="Microsoft.AspNetCore.TestHost" Version="7.0.1" />
-    <PackageReference Include="Microsoft.AspNetCore.Mvc.Testing" Version="7.0.1" />
+    <PackageReference Include="Microsoft.AspNetCore.TestHost" Version="8.0.2" />
+    <PackageReference Include="Microsoft.AspNetCore.Mvc.Testing" Version="8.0.2" />
     <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.4.0" />
     <PackageReference Include="xunit" Version="2.4.2" />
     <PackageReference Include="xunit.runner.visualstudio" Version="2.4.5" />
diff --git a/Samples/WebApps/PetImagesAspNet/PetImages.Tests/rewrite.coyote.json b/Samples/WebApps/PetImagesAspNet/PetImages.Tests/rewrite.coyote.json
index b7cc8ff97..2cef38260 100644
--- a/Samples/WebApps/PetImagesAspNet/PetImages.Tests/rewrite.coyote.json
+++ b/Samples/WebApps/PetImagesAspNet/PetImages.Tests/rewrite.coyote.json
@@ -1,5 +1,5 @@
 {
-  "AssembliesPath": "./bin/net7.0",
+  "AssembliesPath": "./bin/net8.0",
   "Assemblies": [
     "PetImages.dll",
     "PetImages.Tests.dll"
diff --git a/Scripts/CI/azure-nuget-sign-publish.yml b/Scripts/CI/azure-nuget-sign-publish.yml
index 205f322f9..b37427ee3 100644
--- a/Scripts/CI/azure-nuget-sign-publish.yml
+++ b/Scripts/CI/azure-nuget-sign-publish.yml
@@ -8,9 +8,9 @@ steps:
     versionSpec: 6.x
 
 - task: UseDotNet@2
-  displayName: 'Install .NET 7.0 SDK'
+  displayName: 'Install .NET 8.0 SDK'
   inputs:
-    version: 7.0.x
+    version: 8.0.x
 
 - task: UseDotNet@2
   displayName: 'Install .NET 6.0 SDK'
@@ -39,10 +39,10 @@ steps:
     pwsh: true
 
 - task: EsrpCodeSigning@2
-  displayName: 'ESRP CodeSigning .NET 7.0'
+  displayName: 'ESRP CodeSigning .NET 8.0'
   inputs:
     ConnectedServiceName: CoyoteNugetSign
-    FolderPath: bin\net7.0
+    FolderPath: bin\net8.0
     signConfigType: inlineSignParams
     inlineOperation: |
      [
diff --git a/Scripts/common.psm1 b/Scripts/common.psm1
index fe1876210..985234ae6 100644
--- a/Scripts/common.psm1
+++ b/Scripts/common.psm1
@@ -23,7 +23,7 @@ function Invoke-CoyoteTool([String]$cmd, [String]$dotnet, [String]$framework, [S
         $command = "$coyote $cmd $target"
     }
 
-    if ($command -eq "rewrite" -and $framework -ne "netcoreapp3.1" -and $framework -ne "net6.0" -and $framework -ne "net7.0" -and $IsWindows) {
+    if ($command -eq "rewrite" -and $framework -ne "netcoreapp3.1" -and $framework -ne "net6.0" -and $framework -ne "net8.0" -and $IsWindows) {
         # NOTE: Mono.Cecil cannot sign assemblies on unix platforms.
         $command = "$command -snk $key"
     }
diff --git a/Scripts/gen-docs.ps1 b/Scripts/gen-docs.ps1
index abba4e023..271f8f3fa 100644
--- a/Scripts/gen-docs.ps1
+++ b/Scripts/gen-docs.ps1
@@ -3,7 +3,7 @@
 
 $root_dir = "$PSScriptRoot\.."
 $packages_path = "$root_dir\packages"
-$framework = "net7.0"
+$framework = "net8.0"
 
 Import-Module $PSScriptRoot\common.psm1 -Force
 
diff --git a/Scripts/run-benchmark-history.ps1 b/Scripts/run-benchmark-history.ps1
index 758c5fe30..d4717ad32 100644
--- a/Scripts/run-benchmark-history.ps1
+++ b/Scripts/run-benchmark-history.ps1
@@ -41,7 +41,7 @@ function RestoreBenchmark() {
     Invoke-Expression "sed -i 's/\\Performance.Tests.csproj/\\Microsoft.Coyote.Performance.Tests.csproj/' $RootDir\Coyote.sln"
 }
 
-$benchmarks_dir = "$RootDir/Tools/BenchmarkRunner/bin/net7.0"
+$benchmarks_dir = "$RootDir/Tools/BenchmarkRunner/bin/net8.0"
 $benchmark_runner = "BenchmarkRunner.exe"
 $index = 0
 
diff --git a/Scripts/run-benchmarks.ps1 b/Scripts/run-benchmarks.ps1
index c59c2c935..f3e2cc786 100644
--- a/Scripts/run-benchmarks.ps1
+++ b/Scripts/run-benchmarks.ps1
@@ -30,7 +30,7 @@ if ($local -eq ""){
 }
 
 $current_dir = (Get-Item -Path "./").FullName
-$benchmarks_dir = "$PSScriptRoot/../Tools/BenchmarkRunner/bin/net7.0"
+$benchmarks_dir = "$PSScriptRoot/../Tools/BenchmarkRunner/bin/net8.0"
 $benchmark_runner = "BenchmarkRunner.exe"
 $artifacts_dir = "$current_dir/benchmark_$commit"
 
diff --git a/Scripts/run-tests.ps1 b/Scripts/run-tests.ps1
index bfdba5788..c53649532 100644
--- a/Scripts/run-tests.ps1
+++ b/Scripts/run-tests.ps1
@@ -2,8 +2,8 @@
 # Licensed under the MIT License.
 
 param(
-    [ValidateSet("net7.0", "net6.0", "netcoreapp3.1", "net462")]
-    [string]$framework = "net7.0",
+    [ValidateSet("net8.0", "net6.0", "netcoreapp3.1", "net462")]
+    [string]$framework = "net8.0",
     [ValidateSet("all", "runtime", "rewriting", "testing", "actors", "actors-testing", "tools")]
     [string]$test = "all",
     [string]$filter = "",
@@ -32,8 +32,14 @@ $dotnet_runtime_path = FindDotNetRuntimePath -dotnet $dotnet -runtime "NETCore"
 $aspnet_runtime_path = FindDotNetRuntimePath -dotnet $dotnet -runtime "AspNetCore"
 $runtime_version = FindDotNetRuntimeVersion -dotnet_runtime_path $dotnet_runtime_path
 
+# NOTE: we do some hacks to get around a known issue with dotnet tool
+# command being available after locally being restored.
+# Example: https://github.com/dotnet/sdk/issues/11820
 # Restore the local ilverify tool.
+&dotnet nuget locals all --clear
 &dotnet tool restore
+&dotnet tool install dotnet-ilverify --version 8.0.0
+&dotnet tool list
 $ilverify = "dotnet ilverify"
 
 [System.Environment]::SetEnvironmentVariable('COYOTE_CLI_TELEMETRY_OPTOUT', '1')
@@ -53,12 +59,12 @@ foreach ($kvp in $targets.GetEnumerator()) {
         }
 
         $target = "$PSScriptRoot/../Tests/$($kvp.Value)/$($kvp.Value).csproj"
-        if ($f -eq "net7.0") {
+        if ($f -eq "net8.0") {
             $AssemblyName = GetAssemblyName($target)
-            $command = [IO.Path]::Combine($PSScriptRoot, "..", "Tests", $($kvp.Value), "bin", "net7.0", "$AssemblyName.dll")
+            $command = [IO.Path]::Combine($PSScriptRoot, "..", "Tests", $($kvp.Value), "bin", "net8.0", "$AssemblyName.dll")
             $command = $command + ' -r "' + [IO.Path]::Combine( `
-                $PSScriptRoot, "..", "Tests", $($kvp.Value), "bin", "net7.0", "*.dll") + '"'
-            $command = $command + ' -r "' + [IO.Path]::Combine($PSScriptRoot, "..", "bin", "net7.0", "*.dll") + '"'
+                $PSScriptRoot, "..", "Tests", $($kvp.Value), "bin", "net8.0", "*.dll") + '"'
+            $command = $command + ' -r "' + [IO.Path]::Combine($PSScriptRoot, "..", "bin", "net8.0", "*.dll") + '"'
             $command = $command + ' -r "' + [IO.Path]::Combine($dotnet_runtime_path, $runtime_version, "*.dll") + '"'
             $command = $command + ' -r "' + [IO.Path]::Combine($aspnet_runtime_path, $runtime_version, "*.dll") + '"'
             Invoke-ToolCommand -tool $ilverify -cmd $command -error_msg "found corrupted assembly rewriting"
diff --git a/Source/Test/Rewriting/RewritingOptions.cs b/Source/Test/Rewriting/RewritingOptions.cs
index 21042884a..1b2666929 100644
--- a/Source/Test/Rewriting/RewritingOptions.cs
+++ b/Source/Test/Rewriting/RewritingOptions.cs
@@ -308,7 +308,7 @@ private static bool TryResolveTargetFramework(Assembly assembly, out string reso
             {
                 if (tokens[0] == ".NETCoreApp")
                 {
-                    resolvedTargetFramework = tokens[1] is "v7.0" ? "net7.0" :
+                    resolvedTargetFramework = tokens[1] is "v8.0" ? "net8.0" :
                         tokens[1] is "v6.0" ? "net6.0" :
                         tokens[1] is "v3.1" ? "netcoreapp3.1" :
                         resolvedTargetFramework;
@@ -331,10 +331,10 @@ private static bool TryResolveTargetFramework(Assembly assembly, out string reso
         /// {
         ///     // The directory with the assemblies to rewrite. This path is relative
         ///     // to this configuration file.
-        ///     "AssembliesPath": "./bin/net7.0",
+        ///     "AssembliesPath": "./bin/net8.0",
         ///     // The output directory where rewritten assemblies are placed. This path
         ///     // is relative to this configuration file.
-        ///     "OutputPath": "./bin/net7.0/RewrittenBinaries",
+        ///     "OutputPath": "./bin/net8.0/RewrittenBinaries",
         ///     // The assemblies to rewrite. The paths are relative to 'AssembliesPath'.
         ///     "Assemblies": [
         ///         "Example.exe"
diff --git a/Source/Test/Rewriting/Types/Threading/Interlocked.cs b/Source/Test/Rewriting/Types/Threading/Interlocked.cs
index 1b6bc8b68..3e3d009c1 100644
--- a/Source/Test/Rewriting/Types/Threading/Interlocked.cs
+++ b/Source/Test/Rewriting/Types/Threading/Interlocked.cs
@@ -241,7 +241,7 @@ public static IntPtr Exchange(ref IntPtr location1, IntPtr value)
             return SystemInterlocked.Exchange(ref location1, value);
         }
 
-#if NET7_0_OR_GREATER
+#if NET8_0_OR_GREATER
         /// <summary>
         /// Sets a platform-specific handle or pointer to a specified value and returns the
         /// original value, as an atomic operation.
@@ -346,7 +346,7 @@ public static IntPtr CompareExchange(ref IntPtr location1, IntPtr value, IntPtr
             return SystemInterlocked.CompareExchange(ref location1, value, comparand);
         }
 
-#if NET7_0_OR_GREATER
+#if NET8_0_OR_GREATER
         /// <summary>
         /// Compares two platform-specific handles or pointers for equality and, if they
         /// are equal, replaces the first one.
diff --git a/Source/Test/Test.csproj b/Source/Test/Test.csproj
index bec9d421b..c76b6d102 100644
--- a/Source/Test/Test.csproj
+++ b/Source/Test/Test.csproj
@@ -19,8 +19,8 @@
     <PackageReference Include="Mono.Cecil" Version="0.11.4" />
     <PackageReference Include="xunit.abstractions" Version="2.0.3" />
   </ItemGroup>
-  <ItemGroup Condition="'$(TargetFramework)' == 'net7.0'">
-    <PackageReference Include="Microsoft.Extensions.DependencyModel" Version="7.0.0" />
+  <ItemGroup Condition="'$(TargetFramework)' == 'net8.0'">
+    <PackageReference Include="Microsoft.Extensions.DependencyModel" Version="8.0.0" />
   </ItemGroup>
   <ItemGroup Condition="'$(TargetFramework)' == 'net6.0'">
     <PackageReference Include="Microsoft.Extensions.DependencyModel" Version="6.0.0" />
@@ -30,7 +30,7 @@
     <PackageReference Include="System.Text.Json" Version="6.0.0" />
   </ItemGroup>
   <ItemGroup Condition="'$(TargetFramework)' == 'netstandard2.0'">
-    <PackageReference Include="System.Text.Json" Version="7.0.1" />
+    <PackageReference Include="System.Text.Json" Version="8.0.2" />
   </ItemGroup>
   <ItemGroup>
     <ProjectReference Include="..\..\Source\Core\Core.csproj" />
diff --git a/Tests/compare-rewriting-diff-logs.ps1 b/Tests/compare-rewriting-diff-logs.ps1
index 91a891910..abc94e1d0 100644
--- a/Tests/compare-rewriting-diff-logs.ps1
+++ b/Tests/compare-rewriting-diff-logs.ps1
@@ -3,7 +3,7 @@
 
 Import-Module $PSScriptRoot/../Scripts/common.psm1 -Force
 
-$framework = "net7.0"
+$framework = "net8.0"
 $targets = [ordered]@{
     "rewriting" = "Tests.Rewriting"
     "rewriting-helpers" = "Tests.Rewriting.Helpers"
diff --git a/Tests/get-rewriting-diff-logs.ps1 b/Tests/get-rewriting-diff-logs.ps1
index 319c20069..8def4195e 100644
--- a/Tests/get-rewriting-diff-logs.ps1
+++ b/Tests/get-rewriting-diff-logs.ps1
@@ -3,7 +3,7 @@
 
 Import-Module $PSScriptRoot/../Scripts/common.psm1 -Force
 
-$framework = "net7.0"
+$framework = "net8.0"
 $targets = [ordered]@{
     "rewriting" = "Tests.Rewriting"
     "rewriting-helpers" = "Tests.Rewriting.Helpers"
diff --git a/Tools/CLI/Coyote.CLI.csproj b/Tools/CLI/Coyote.CLI.csproj
index 38da737bf..177f48c83 100644
--- a/Tools/CLI/Coyote.CLI.csproj
+++ b/Tools/CLI/Coyote.CLI.csproj
@@ -20,13 +20,13 @@
   <ItemGroup>
     <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
   </ItemGroup>
-  <ItemGroup Condition="'$(TargetFramework)' == 'net7.0'">
+  <ItemGroup Condition="'$(TargetFramework)' == 'net8.0'">
     <FrameworkReference Include="Microsoft.AspNetCore.App" />
-    <PackageReference Include="System.Configuration.ConfigurationManager" Version="7.0.0" />
+    <PackageReference Include="System.Configuration.ConfigurationManager" Version="8.0.0" />
   </ItemGroup>
   <ItemGroup Condition="'$(TargetFramework)' == 'net6.0'">
     <FrameworkReference Include="Microsoft.AspNetCore.App" />
-    <PackageReference Include="System.Configuration.ConfigurationManager" Version="7.0.0" />
+    <PackageReference Include="System.Configuration.ConfigurationManager" Version="8.0.0" />
   </ItemGroup>
   <ItemGroup Condition="'$(TargetFramework)' == 'netcoreapp3.1'">
     <FrameworkReference Include="Microsoft.AspNetCore.App" />
diff --git a/Tools/Coyote/Coyote.csproj b/Tools/Coyote/Coyote.csproj
index 8c43ef371..45d873e78 100644
--- a/Tools/Coyote/Coyote.csproj
+++ b/Tools/Coyote/Coyote.csproj
@@ -22,17 +22,17 @@
       <PrivateAssets>all</PrivateAssets>
     </PackageReference>
   </ItemGroup>
-  <ItemGroup Condition="'$(TargetFramework)' == 'net7.0'">
+  <ItemGroup Condition="'$(TargetFramework)' == 'net8.0'">
     <FrameworkReference Include="Microsoft.AspNetCore.App" />
     <FrameworkReference Include="Microsoft.NETCore.App" />
-    <PackageReference Include="System.Configuration.ConfigurationManager" Version="7.0.0" >
+    <PackageReference Include="System.Configuration.ConfigurationManager" Version="8.0.0" >
       <PrivateAssets>all</PrivateAssets>
     </PackageReference>
   </ItemGroup>
   <ItemGroup Condition="'$(TargetFramework)' == 'net6.0'">
     <FrameworkReference Include="Microsoft.AspNetCore.App" />
     <FrameworkReference Include="Microsoft.NETCore.App" />
-    <PackageReference Include="System.Configuration.ConfigurationManager" Version="7.0.0" >
+    <PackageReference Include="System.Configuration.ConfigurationManager" Version="8.0.0" >
       <PrivateAssets>all</PrivateAssets>
     </PackageReference>
   </ItemGroup>
diff --git a/docs/assets/images/RaftMocking.dgml b/docs/assets/images/RaftMocking.dgml
index aedc01735..81ada9053 100644
--- a/docs/assets/images/RaftMocking.dgml
+++ b/docs/assets/images/RaftMocking.dgml
@@ -432,9 +432,9 @@
     </Style>
   </Styles>
   <Paths>
-    <Path Id="64ea33e6-a1c1-4e8b-9ce0-e581e344ee49.OutputPath" Value="D:\git\microsoft\CoyoteSamples\bin\net7.0\Raft.dll" />
-    <Path Id="64ea33e6-a1c1-4e8b-9ce0-e581e344ee49.OutputPathUri" Value="file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll" />
-    <Path Id="adc6f234-56dd-47d9-8e55-e4aa8a71170d.OutputPath" Value="D:\git\microsoft\CoyoteSamples\bin\net7.0\Raft.Mocking.dll" />
-    <Path Id="adc6f234-56dd-47d9-8e55-e4aa8a71170d.OutputPathUri" Value="file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll" />
+    <Path Id="64ea33e6-a1c1-4e8b-9ce0-e581e344ee49.OutputPath" Value="D:\git\microsoft\CoyoteSamples\bin\net8.0\Raft.dll" />
+    <Path Id="64ea33e6-a1c1-4e8b-9ce0-e581e344ee49.OutputPathUri" Value="file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll" />
+    <Path Id="adc6f234-56dd-47d9-8e55-e4aa8a71170d.OutputPath" Value="D:\git\microsoft\CoyoteSamples\bin\net8.0\Raft.Mocking.dll" />
+    <Path Id="adc6f234-56dd-47d9-8e55-e4aa8a71170d.OutputPathUri" Value="file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll" />
   </Paths>
 </DirectedGraph>
\ No newline at end of file
diff --git a/docs/assets/images/RaftMocking.svg b/docs/assets/images/RaftMocking.svg
index 2e8ac3f83..d579fa497 100644
--- a/docs/assets/images/RaftMocking.svg
+++ b/docs/assets/images/RaftMocking.svg
@@ -8,74 +8,74 @@
   </defs>
   <rect width="1184.9437333333331" height="773.47879784008285" fill="#1E1E1E" />
   <g transform="translate(487.044981487557,192.344743585442)">
-    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll)" />
-    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll)">
+    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll)" />
+    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll)">
       <path d="M 108.227021107097,137.655956414558 L 107.652090356671,187.134111791473" stroke-dasharray="2,0" fill="none" stroke="#00A600" stroke-width="3.713132377351049" />
       <path d="M 107.547518401173,196.133504254641 L 111.663439446468,186.180655720232 C 108.985333684548,187.149603933029 106.318847028795,187.118619649918 103.663979479208,186.0877028709 z" fill="#00A600" stroke="#00A600" stroke-width="1" stroke-linejoin="round" />
     </g>
-    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll)">
+    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll)">
       <rect x="-189.173558456323" y="-172.344743585442" rx="5" ry="5" width="598.403333333333" height="310.0007" fill="#094167" stroke="#094167" stroke-width="1" />
       <use x="56.826441543676992" y="-167.344743585442" xlink:href="#CodeSchema_Assembly" />
       <text x="76.826441543676992" y="-154.394743585442" fill="#FFFFFF">Raft.Mocking.dll</text>
       <rect x="-184.173558456323" y="-144.38474358544198" width="588.403333333333" height="277.0407" fill="#1E1E1E" stroke="#094167" stroke-width="1" />
-      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
+      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
         <path d="M 73.866441543677,-23.0403355086654 L 94.9405894341168,-25.762345065691" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="1" />
         <path d="M 103.866441542077,-26.9152388798929 L 93.4364308380315,-29.6012911343175 C 94.7697903505313,-27.0846935261295 95.1113885177022,-24.4399966052524 94.4612253395443,-21.6672003716863 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
       </g>
-      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
+      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
         <rect x="103.866441542077" y="-115.344644586843" rx="5" ry="5" width="285.363333333333" height="140.0003" fill="#0E619A" stroke="#0E619A" stroke-width="1" />
         <use x="122.866441542077" y="-109.344644586843" xlink:href="#CodeSchema_Namespace" />
         <text x="139.86644154207698" y="-97.394644586843" fill="#FFFFFF">Microsoft‎.Coyote‎.Samples‎.CloudMessaging</text>
         <rect x="108.866441542077" y="-87.384644586843" width="275.363333333333" height="107.0403" fill="#1E1E1E" stroke="#0E619A" stroke-width="1" />
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=MockClient)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=MockClient)">
           <rect x="159.374774881092" y="-75.3445445868431" rx="5" ry="5" width="120.69" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="179.374774881092" y="-70.3445445868431" xlink:href="#CodeSchema_Class" />
           <text x="200.374774881092" y="-57.3945445868431" fill="#FFFFFF">MockClient</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=MockClusterManager)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=MockClusterManager)">
           <rect x="159.374774875411" y="-20.3444445868431" rx="5" ry="5" width="174.346666666666" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="178.374774875411" y="-15.3444445868431" xlink:href="#CodeSchema_Class" />
           <text x="199.374774875411" y="-2.3944445868430986" fill="#FFFFFF">MockClusterManager</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
       </g>
-      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking)">
+      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking)">
         <rect x="-169.173558456323" y="-132.344643585443" rx="5" ry="5" width="243.04" height="250.0005" fill="#0E619A" stroke="#0E619A" stroke-width="1" />
         <use x="-150.173558456323" y="-126.34464358544301" xlink:href="#CodeSchema_Namespace" />
         <text x="-133.173558456323" y="-114.394643585443" fill="#FFFFFF">Microsoft‎.Coyote‎.Samples‎.Mocking</text>
         <rect x="-164.173558456323" y="-104.384643585443" width="233.04" height="217.04049999999998" fill="#1E1E1E" stroke="#0E619A" stroke-width="1" />
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=MockServerHost)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=SafetyMonitor)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=MockServerHost)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=SafetyMonitor)">
           <path d="M -47.653558456323,42.655606414557 L -47.653558456323,63.655606414557" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="1.5" />
           <path d="M -47.653558456323,72.655606414557 L -43.653558456323,62.655606414557 C -46.3202251229897,63.655606414557 -48.9868917896563,63.655606414557 -51.653558456323,62.655606414557 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=Program)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=RaftTestScenario)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=Program)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=RaftTestScenario)">
           <path d="M -47.653558456323,-67.344393585443 L -47.653558456323,-46.344393585443" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="1.792481250360578" />
           <path d="M -47.653558456323,-37.344393585443 L -43.653558456323,-47.344393585443 C -46.3202251229897,-46.344393585443 -48.9868917896563,-46.344393585443 -51.653558456323,-47.344393585443 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=RaftTestScenario)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=MockServerHost)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=RaftTestScenario)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=MockServerHost)">
           <path d="M -47.653558456323,-12.344393585443 L -47.653558456323,8.65560641455698" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="1" />
           <path d="M -47.653558456323,17.655606414557 L -43.653558456323,7.65560641455698 C -46.3202251229897,8.65560641455698 -48.9868917896563,8.65560641455698 -51.653558456323,7.65560641455698 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=MockServerHost)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=MockServerHost)">
           <rect x="-121.675225122989" y="17.6556564145567" rx="5" ry="5" width="148.043333333333" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-102.675225122989" y="22.6556564145567" xlink:href="#CodeSchema_Class" />
           <text x="-81.675225122989" y="35.6056564145567" fill="#FFFFFF">MockServerHost</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=Program)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=Program)">
           <rect x="-100.956891789656" y="-92.3445435854426" rx="5" ry="5" width="106.606666666667" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-80.956891789656" y="-87.3445435854426" xlink:href="#CodeSchema_Class" />
           <text x="-59.956891789656" y="-74.394543585442591" fill="#FFFFFF">Program</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=RaftTestScenario)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=RaftTestScenario)">
           <rect x="-121.583558456323" y="-37.3444435854426" rx="5" ry="5" width="147.86" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-101.583558456323" y="-32.3444435854426" xlink:href="#CodeSchema_Class" />
           <text x="-80.583558456323" y="-19.394443585442595" fill="#FFFFFF">RaftTestScenario</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=SafetyMonitor)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Mocking.dll Namespace=Microsoft.Coyote.Samples.Mocking Type=SafetyMonitor)">
           <rect x="-115.733558456323" y="72.6557564145576" rx="5" ry="5" width="136.16" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-96.733558456323" y="77.6557564145576" xlink:href="#CodeSchema_Class" />
           <text x="-75.733558456323" y="90.6057564145576" fill="#FFFFFF">SafetyMonitor</text>
@@ -83,133 +83,133 @@
         </g>
       </g>
     </g>
-    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll)">
+    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll)">
       <rect x="-467.0449814875567" y="196.13350425464103" rx="5" ry="5" width="1144.9437333333331" height="365.00054999999986" fill="#094167" stroke="#094167" stroke-width="1" />
       <use x="76.9550185124433" y="201.13350425464103" xlink:href="#CodeSchema_Assembly" />
       <text x="96.9550185124433" y="214.083504254641" fill="#FFFFFF">Raft.dll</text>
       <rect x="-462.0449814875567" y="224.09350425464103" width="1134.9437333333331" height="332.04054999999988" fill="#1E1E1E" stroke="#094167" stroke-width="1" />
-      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
+      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
         <rect x="-447.04498148755664" y="236.13360425464092" rx="5" ry="5" width="1104.9437333333328" height="305.00035" fill="#0E619A" stroke="#0E619A" stroke-width="1" />
         <use x="-18.04498148755664" y="242.13360425464092" xlink:href="#CodeSchema_Namespace" />
         <text x="-1.0449814875566403" y="254.0836042546409" fill="#FFFFFF">Microsoft‎.Coyote‎.Samples‎.CloudMessaging</text>
         <rect x="-442.04498148755664" y="264.09360425464092" width="1094.9437333333328" height="272.04035000000005" fill="#1E1E1E" stroke="#0E619A" stroke-width="1" />
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
           <path d="M 331.917262517409,356.133741959559 L 259.371660137095,382.833908100003" fill="none" stroke="#A0A0A0" stroke-width="1.5" />
           <path d="M 250.405763396648,386.133776385788 L 261.171917720316,386.433644821876 C 259.832188101851,384.085184157256 258.911132172339,381.58263204275 258.408749931779,378.925988478357 z" fill="#A0A0A0" stroke="#A0A0A0" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterClientEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterClientEvent)">
           <path d="M -216.111093845686,466.133868189067 L -320.728177129853,493.690758326495" stroke-dasharray="2,2" fill="none" stroke="#00AEEF" stroke-width="1.5" />
           <path d="M -330.003339467189,496.133902615297 L -319.314312686544,497.454775994035 C -320.388552148989,494.980111904902 -321.067802110718,492.401404748088 -321.352062571729,489.718654523594 z" fill="#00AEEF" stroke="#00AEEF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterServerEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterServerEvent)">
           <path d="M -168.655991503393,466.133868189067 L -168.655991503393,487.133892287428" stroke-dasharray="2,2" fill="none" stroke="#00AEEF" stroke-width="1.792481250360578" />
           <path d="M -168.655991503393,496.133902615297 L -164.655991503393,486.133902615297 C -167.322658170059,487.133892287428 -169.989324836726,487.133892287428 -172.655991503393,486.133902615297 z" fill="#00AEEF" stroke="#00AEEF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)">
           <path d="M 196.280798892089,300.631905335175 L 307.279848058691,328.775613905011" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="3.4770981551934379" />
           <path d="M 316.580213958211,331.133713271034 L 307.870026240532,324.798681311936 C 307.607544250878,327.483177065779 306.952151866504,330.068050744243 305.90384908741,332.553302347328 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesResponseEvent)">
           <path d="M 98.6221728518094,294.323948548535 L -217.437562312856,330.052210286192" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="3.4036774610288019" />
           <path d="M -227.004765707155,331.133713271034 L -216.61874379146,333.985124985732 C -217.287792536812,331.377105297868 -217.5873320889,328.727315274517 -217.517362447722,326.035754915681 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientRequestEvent)">
           <path d="M 100.308361978574,299.776136023636 L -27.2482258276019,328.990087644834" stroke-dasharray="2,2" fill="none" stroke="#00AEEF" stroke-width="2.292481250360578" />
           <path d="M -36.6079171818358,331.133713271034 L -25.9673098275031,332.80028914117 C -26.9505629458092,330.289770139362 -27.5458887093947,327.690405150307 -27.7532871182597,325.002194174007 z" fill="#00AEEF" stroke="#00AEEF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientResponseEvent)">
           <path d="M 142.26072519969,301.133678844805 L 130.496533828348,323.08542659793" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="1" />
           <path d="M 126.183365432891,331.133713271034 L 134.432559899219,324.209062329888 C 131.671744026932,323.715235114007 129.321323629765,322.455618081853 127.381298707717,320.430211233427 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=IServerManager)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=IServerManager)">
           <path d="M 199.297077353237,294.796173018176 L 511.705246662844,333.042407546691" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="3.5849625007211561" />
           <path d="M 521.260531776702,334.212203062151 L 511.820704650245,329.02667861205 C 511.867268915662,331.718955028703 511.543224410026,334.365860064679 510.848571133336,336.96739371998 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
           <path d="M 177.076965168303,301.133678844805 L 181.316628225312,303.018489033232 C 208.280797494303,315.005842810473 221.270267002335,328.187878127886 220.285036749409,342.56459498547 L 217.914766994359,377.152141443005" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="3.6239637567217926" />
           <path d="M 217.299259395926,386.133776385788 L 221.973591933214,376.430652387259 C 219.244980444181,377.243300401382 216.584553544538,377.060982484628 213.992311234287,375.883698636999 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteRequestEvent)">
           <path d="M 101.14753012221,300.378919451811 L 90.4024801375436,303.018489033232 C 41.6048593333939,315.005842810473 17.2060489313189,323.095279691334 17.2060489313189,327.286799675817 L 17.2060489313189,336.088991643229 C 17.2060489313189,341.007782991711 25.7369007299075,355.210053426159 42.7986043270847,378.695802946572" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="2.9036774610288019" />
           <path d="M 48.2244869889268,386.133776385788 L 45.56263359515,375.697563638338 C 43.875784946618,377.910016912921 41.7214237075515,379.481588980222 39.0995498779505,380.41227984024 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteResponseEvent)">
           <path d="M 177.076965168303,301.133678844805 L 181.316628225312,303.018489033232 C 208.280797494303,315.005842810473 222.727749339872,325.191039683575 224.657483762021,333.57407965254 L 229.288846375177,353.693375578054 C 231.209349068538,362.036311608091 259.257746269446,372.164202974692 313.434037977901,384.077049677857" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="2.4036774610288019" />
           <path d="M 322.816059489004,386.133776385788 L 313.904558642815,380.085210219466 C 313.719551291447,382.774644239613 313.148524664355,385.3794551161 312.191478761542,387.899642848927 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)">
           <rect x="233.93865184577624" y="331.13385425464094" rx="5" ry="5" width="229.45000000000005" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="253.93865184577624" y="336.13385425464094" xlink:href="#CodeSchema_Class" />
           <text x="274.93865184577623" y="349.08385425464093" fill="#FFFFFF">AppendLogEntriesRequestEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesResponseEvent)">
           <rect x="-427.0449814875563" y="331.13385425464094" rx="5" ry="5" width="237.493333333333" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-408.0449814875563" y="336.13385425464094" xlink:href="#CodeSchema_Class" />
           <text x="-387.0449814875563" y="349.08385425464093" fill="#FFFFFF">AppendLogEntriesResponseEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientRequestEvent)">
           <rect x="-159.55154815422384" y="331.13385425464094" rx="5" ry="5" width="162.7233333333329" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-140.55154815422384" y="336.13385425464094" xlink:href="#CodeSchema_Class" />
           <text x="-119.55154815422384" y="349.08385425464093" fill="#FFFFFF">ClientRequestEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientResponseEvent)">
           <rect x="33.171885179108983" y="331.133804254641" rx="5" ry="5" width="170.76666666666694" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="53.171885179108983" y="336.133804254641" xlink:href="#CodeSchema_Class" />
           <text x="74.171885179108983" y="349.083804254641" fill="#FFFFFF">ClientResponseEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)">
           <rect x="-223.0549814875564" y="441.13385425464094" rx="5" ry="5" width="145.03333333333296" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-204.0549814875564" y="446.13385425464094" xlink:href="#CodeSchema_Class" />
           <text x="-183.0549814875564" y="459.08385425464093" fill="#FFFFFF">ClusterManager</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=IServerManager)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=IServerManager)">
           <rect x="493.38875184577626" y="331.13385425464094" rx="5" ry="5" width="144.51" height="25" fill="#1382CE" stroke="#1382CE" stroke-width="1" />
           <use x="512.38875184577626" y="339.13385425464094" xlink:href="#CodeSchema_Interface" />
           <text x="533.38875184577626" y="349.08385425464093" fill="#FFFFFF">IServerManager</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#1382CE" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
           <rect x="168.73084067607397" y="386.13385425464094" rx="5" ry="5" width="80.74666666666667" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="188.73084067607397" y="391.13385425464094" xlink:href="#CodeSchema_Class" />
           <text x="209.73084067607397" y="404.08385425464093" fill="#FFFFFF">Log</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=NotifyJoinedServiceEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=NotifyJoinedServiceEvent)">
           <rect x="-37.709981487556433" y="441.13400425464096" rx="5" ry="5" width="194.14333333333298" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-18.709981487556433" y="446.13400425464096" xlink:href="#CodeSchema_Class" />
           <text x="2.2900185124435666" y="459.08400425464094" fill="#FFFFFF">NotifyJoinedServiceEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterClientEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterClientEvent)">
           <rect x="-427.04498148755647" y="496.13385425464094" rx="5" ry="5" width="163.01333333333298" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-408.04498148755647" y="501.13385425464094" xlink:href="#CodeSchema_Class" />
           <text x="-387.04498148755647" y="514.083854254641" fill="#FFFFFF">RegisterClientEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterServerEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterServerEvent)">
           <rect x="-233.36664815422307" y="496.13385425464094" rx="5" ry="5" width="165.65666666666698" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-213.36664815422307" y="501.13385425464094" xlink:href="#CodeSchema_Class" />
           <text x="-192.36664815422307" y="514.083854254641" fill="#FFFFFF">RegisterServerEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)">
           <rect x="99.071984162007709" y="276.13370425464092" rx="5" ry="5" width="94.019999999999982" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="118.07198416200771" y="281.13370425464092" xlink:href="#CodeSchema_Class" />
           <text x="139.07198416200771" y="294.08370425464091" fill="#FFFFFF">Server</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteRequestEvent)">
           <rect x="-17.67925932392572" y="386.133904254641" rx="5" ry="5" width="156.41000000000003" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="2.32074067607428" y="391.133904254641" xlink:href="#CodeSchema_Class" />
           <text x="23.32074067607428" y="404.08390425464097" fill="#FFFFFF">VoteRequestEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteResponseEvent)">
           <rect x="279.47760734274073" y="386.13385425464094" rx="5" ry="5" width="164.45333333333292" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="298.47760734274073" y="391.13385425464094" xlink:href="#CodeSchema_Class" />
           <text x="319.47760734274073" y="404.08385425464093" fill="#FFFFFF">VoteResponseEvent</text>
diff --git a/docs/assets/images/cloudmessaging.dgml b/docs/assets/images/cloudmessaging.dgml
index 17c25fdbe..249e0aa13 100644
--- a/docs/assets/images/cloudmessaging.dgml
+++ b/docs/assets/images/cloudmessaging.dgml
@@ -413,9 +413,9 @@
     </Style>
   </Styles>
   <Paths>
-    <Path Id="64ea33e6-a1c1-4e8b-9ce0-e581e344ee49.OutputPath" Value="D:\git\microsoft\CoyoteSamples\bin\net7.0\Raft.dll" />
-    <Path Id="64ea33e6-a1c1-4e8b-9ce0-e581e344ee49.OutputPathUri" Value="file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll" />
-    <Path Id="9513779f-4e37-4a20-9e33-8beb11477695.OutputPath" Value="D:\git\microsoft\CoyoteSamples\bin\net7.0\Raft.Azure.dll" />
-    <Path Id="9513779f-4e37-4a20-9e33-8beb11477695.OutputPathUri" Value="file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll" />
+    <Path Id="64ea33e6-a1c1-4e8b-9ce0-e581e344ee49.OutputPath" Value="D:\git\microsoft\CoyoteSamples\bin\net8.0\Raft.dll" />
+    <Path Id="64ea33e6-a1c1-4e8b-9ce0-e581e344ee49.OutputPathUri" Value="file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll" />
+    <Path Id="9513779f-4e37-4a20-9e33-8beb11477695.OutputPath" Value="D:\git\microsoft\CoyoteSamples\bin\net8.0\Raft.Azure.dll" />
+    <Path Id="9513779f-4e37-4a20-9e33-8beb11477695.OutputPathUri" Value="file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll" />
   </Paths>
 </DirectedGraph>
\ No newline at end of file
diff --git a/docs/assets/images/cloudmessaging.svg b/docs/assets/images/cloudmessaging.svg
index d942d3071..63692575a 100644
--- a/docs/assets/images/cloudmessaging.svg
+++ b/docs/assets/images/cloudmessaging.svg
@@ -8,52 +8,52 @@
   </defs>
   <rect width="1184.943733333334" height="654.554072069219" fill="#1E1E1E" />
   <g transform="translate(522.074416244198,194.584024338219)">
-    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll)" />
-    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll)">
+    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll)" />
+    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll)">
       <path d="M 74.4422867232811,25.416175661781 L 73.7353936597412,65.9708646376465" stroke-dasharray="2,0" fill="none" stroke="#00A600" stroke-width="3.836212670985748" />
       <path d="M 73.5785419743832,74.9694977310002 L 77.7522141107159,65.0407283763218 C 75.0685244883862,65.9941019243662 72.4022628310962,65.9476273509268 69.753429138846,64.9013046560036 z" fill="#00A600" stroke="#00A600" stroke-width="1" stroke-linejoin="round" />
     </g>
-    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll)">
+    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll)">
       <rect x="-235.28131870585378" y="-174.58402433821891" rx="5" ry="5" width="622.93333333333339" height="200.00040000000007" fill="#094167" stroke="#094167" stroke-width="1" />
       <use x="30.718681294146222" y="-169.58402433821891" xlink:href="#CodeSchema_Assembly" />
       <text x="50.718681294146222" y="-156.63402433821892" fill="#FFFFFF">Raft.Azure.dll</text>
       <rect x="-230.28131870585378" y="-146.6240243382189" width="612.93333333333339" height="167.04040000000006" fill="#1E1E1E" stroke="#094167" stroke-width="1" />
-      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
+      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
         <rect x="-215.28131870585375" y="-134.58392433821891" rx="5" ry="5" width="582.93333333333339" height="140.00020000000009" fill="#0E619A" stroke="#0E619A" stroke-width="1" />
         <use x="-47.281318705853749" y="-128.58392433821891" xlink:href="#CodeSchema_Namespace" />
         <text x="-30.281318705853749" y="-116.6339243382189" fill="#FFFFFF">Microsoft‎.Coyote‎.Samples‎.CloudMessaging</text>
         <rect x="-210.28131870585375" y="-106.6239243382189" width="572.93333333333339" height="107.04020000000008" fill="#1E1E1E" stroke="#0E619A" stroke-width="1" />
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Program)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureClusterManager)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Program)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureClusterManager)">
           <path d="M 53.9135287077871,-69.583820766798 L -51.5018508769543,-41.8742802528154" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="1.5" />
           <path d="M -60.2153622801482,-39.5838421953235 L -49.5270122096152,-38.2575040899604 C -51.1628851386956,-40.5847532053811 -51.8408166152129,-43.1638073002496 -51.560806639167,-45.994666374566 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Program)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureMessageReceiver)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Program)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureMessageReceiver)">
           <path d="M 101.467233286094,-69.583820766798 L 101.467233286094,-48.5838357667658" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="2.4036774610288019" />
           <path d="M 101.467233286094,-39.5838421953235 L 105.467233286094,-49.5838421953235 C 102.800566619427,-48.5838357667658 100.13389995276,-48.5838357667658 97.4672332860935,-49.5838421953235 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Program)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureServer)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Program)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureServer)">
           <path d="M 143.332695689961,-69.583820766798 L 235.177044127443,-42.1613711027668" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="2.1609640474436809" />
           <path d="M 243.809805459244,-39.5838421953235 L 235.372174058809,-46.2775987154243 C 235.558504352722,-43.4389727129364 234.795583902164,-40.8837694925972 233.083412707135,-38.6119890544068 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureClusterManager)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureClusterManager)">
           <rect x="-195.28131870585375" y="-39.583824338218818" rx="5" ry="5" width="175.44" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-175.28131870585375" y="-34.583824338218818" xlink:href="#CodeSchema_Class" />
           <text x="-154.28131870585375" y="-21.633824338218815" fill="#FFFFFF">AzureClusterManager</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureMessageReceiver)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureMessageReceiver)">
           <rect x="10.377014627479696" y="-39.583824338218818" rx="5" ry="5" width="182.123333333333" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="29.377014627479696" y="-34.583824338218818" xlink:href="#CodeSchema_Class" />
           <text x="50.377014627479696" y="-21.633824338218815" fill="#FFFFFF">AzureMessageReceiver</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureServer)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AzureServer)">
           <rect x="223.22534796081266" y="-39.583824338219017" rx="5" ry="5" width="124.42666666666696" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="243.22534796081266" y="-34.583824338219017" xlink:href="#CodeSchema_Class" />
           <text x="264.22534796081266" y="-21.633824338219014" fill="#FFFFFF">AzureServer</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Program)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.Azure.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Program)">
           <rect x="48.13534796081268" y="-94.583824338219017" rx="5" ry="5" width="106.60666666666697" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="68.13534796081268" y="-89.583824338219017" xlink:href="#CodeSchema_Class" />
           <text x="89.13534796081268" y="-76.633824338219014" fill="#FFFFFF">Program</text>
@@ -61,133 +61,133 @@
         </g>
       </g>
     </g>
-    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll)">
+    <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll)">
       <rect x="-502.07441624419789" y="74.96949773100016" rx="5" ry="5" width="1144.943733333334" height="365.00055" fill="#094167" stroke="#094167" stroke-width="1" />
       <use x="41.925583755802108" y="79.96949773100016" xlink:href="#CodeSchema_Assembly" />
       <text x="61.925583755802108" y="92.919497731000163" fill="#FFFFFF">Raft.dll</text>
       <rect x="-497.07441624419789" y="102.92949773100017" width="1134.943733333334" height="332.04055" fill="#1E1E1E" stroke="#094167" stroke-width="1" />
-      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
+      <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging)">
         <rect x="-482.07441624419789" y="114.96959773100014" rx="5" ry="5" width="1104.943733333334" height="305.00035" fill="#0E619A" stroke="#0E619A" stroke-width="1" />
         <use x="-53.074416244197892" y="120.96959773100014" xlink:href="#CodeSchema_Namespace" />
         <text x="-36.074416244197892" y="132.91959773100012" fill="#FFFFFF">Microsoft‎.Coyote‎.Samples‎.CloudMessaging</text>
         <rect x="-477.07441624419789" y="142.92959773100014" width="1094.943733333334" height="272.04035000000005" fill="#1E1E1E" stroke="#0E619A" stroke-width="1" />
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterClientEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterClientEvent)">
           <path d="M -251.140528602327,344.969861665426 L -355.757611886495,372.526751802855" stroke-dasharray="2,2" fill="none" stroke="#00AEEF" stroke-width="1.5" />
           <path d="M -365.03277422383,374.969896091656 L -354.343747443186,376.290769470395 C -355.417986905631,373.816105381262 -356.097236867359,371.237398224448 -356.381497328371,368.554647999953 z" fill="#00AEEF" stroke="#00AEEF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterServerEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterServerEvent)">
           <path d="M -203.685426260034,344.969861665426 L -203.685426260034,365.969885763787" stroke-dasharray="2,2" fill="none" stroke="#00AEEF" stroke-width="1.792481250360578" />
           <path d="M -203.685426260034,374.969896091656 L -199.685426260034,364.969896091656 C -202.352092926701,365.969885763787 -205.018759593368,365.969885763787 -207.685426260034,364.969896091656 z" fill="#00AEEF" stroke="#00AEEF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientRequestEvent)">
           <path d="M 54.6511168499186,179.026279736195 L -64.8417155880862,207.727896572328" stroke-dasharray="2,2" fill="none" stroke="#00AEEF" stroke-width="2.1609640474436809" />
           <path d="M -74.1749963275075,209.969706747394 L -63.5173443880586,211.52355845768 C -64.5303122472249,209.024355494577 -65.1531189289474,206.431437650079 -65.385764433226,203.744804924188 z" fill="#00AEEF" stroke="#00AEEF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientResponseEvent)">
           <path d="M 153.10200728486,173.672092451466 L 449.753579250761,210.224636424702" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="1" />
           <path d="M 459.307815285112,211.401881603152 L 449.87204289981,206.208982654322 C 449.916635571992,208.901310911503 449.59052292953,211.547961937902 448.893704972424,214.148935733518 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=IServerManager)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=IServerManager)">
           <path d="M 95.4083948951286,179.969672321164 L 82.3952314253365,202.082395122541" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="3.713132377351049" />
           <path d="M 77.7536105614864,209.969706747394 L 86.2728061067182,203.380070394597 C 83.5443480426802,202.758641214967 81.2461148079929,201.406149030114 79.3781064026564,199.322593840036 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
           <path d="M 124.335820256369,179.969672321164 L 127.588435761307,181.854482509591 C 148.275003033941,193.841836286832 159.061341069779,207.023871604245 159.94744986882,221.40058846183 L 162.079037057781,255.984632211444" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="3.54373142062517" />
           <path d="M 162.632835926587,264.969769862148 L 166.010077254103,254.742637272036 C 163.409845002737,255.90260787713 160.748229112825,256.066656545757 158.025229584367,255.234783277918 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteRequestEvent)">
           <path d="M 116.642740165036,179.969672321164 L 123.119226559451,185.803012348486 C 150.25878859319,210.247484843933 164.118029773382,223.727177087001 164.696950100027,226.24208907769 L 165.565330589994,230.014457063724 C 166.139030352899,232.506690185243 200.48682907853,243.297080967527 268.608726766888,262.385629410576" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="2.9036774610288019" />
           <path d="M 277.839973427084,264.969769862148 L 269.288452609281,258.422137335602 C 268.968154835788,261.101655407309 268.249298697989,263.669603413843 267.131884195884,266.125981355203 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteResponseEvent)">
           <path d="M 56.6288057008078,179.852512943632 L 49.1699146521608,181.854482509591 C 4.50771433383965,193.841836286832 -16.1728996405756,207.023871604245 -12.8719272710848,221.40058846183 L -4.88872842001468,256.169794820662" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="2.5" />
           <path d="M -2.86820629720273,264.969769862148 L -1.20747423282129,254.328248870751 C -3.58920959045729,255.871418230757 -6.18824724957206,256.468171410567 -9.00458721016558,256.118508410184 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)">
           <path d="M 148.158955796458,179.954928102269 L 248.043319141178,207.42711050179" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="3.4770981551934379" />
           <path d="M 257.287783361072,209.969706747394 L 248.706596619214,203.46100226022 C 248.396908772262,206.141516417109 247.689729510094,208.712704586472 246.58505883271,211.174566768308 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesResponseEvent)">
           <path d="M 52.4271027834322,173.293595316887 L -255.007922768899,208.863181080106" stroke-dasharray="2,0" fill="none" stroke="#FF00FF" stroke-width="3.4036774610288019" />
           <path d="M -264.571844852826,209.969706747394 L -254.178385458564,212.793888366876 C -254.854681143816,210.187679015974 -255.161164393982,207.538683144237 -255.097835209062,204.846900751666 z" fill="#FF00FF" stroke="#FF00FF" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)-&gt;(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
           <path d="M 271.06931044083,234.969735435918 L 203.946415573145,261.465800534078" fill="none" stroke="#A0A0A0" stroke-width="1.5" />
           <path d="M 195.06975543677,264.969769862148 L 205.839973906079,265.018699642012 C 204.435973918876,262.706006325027 203.456857227414,260.225594743129 202.902623831694,257.577464896319 z" fill="#A0A0A0" stroke="#A0A0A0" stroke-width="1" stroke-linejoin="round" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientRequestEvent)">
           <rect x="-194.58098291086421" y="209.96979773099997" rx="5" ry="5" width="162.72333333333307" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-175.58098291086421" y="214.96979773099997" xlink:href="#CodeSchema_Class" />
           <text x="-154.58098291086421" y="227.91979773099996" fill="#FFFFFF">ClientRequestEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClientResponseEvent)">
           <rect x="432.10265042246863" y="209.96984773099993" rx="5" ry="5" width="170.76666666666711" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="452.10265042246863" y="214.96984773099993" xlink:href="#CodeSchema_Class" />
           <text x="473.10265042246863" y="227.91984773099992" fill="#FFFFFF">ClientResponseEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=ClusterManager)">
           <rect x="-258.084416244198" y="319.96984773100007" rx="5" ry="5" width="145.03333333333296" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-239.084416244198" y="324.96984773100007" xlink:href="#CodeSchema_Class" />
           <text x="-218.084416244198" y="337.91984773100006" fill="#FFFFFF">ClusterManager</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=IServerManager)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=IServerManager)">
           <rect x="-1.8575495775312447" y="209.969797731" rx="5" ry="5" width="144.51" height="25" fill="#1382CE" stroke="#1382CE" stroke-width="1" />
           <use x="17.142450422468755" y="217.969797731" xlink:href="#CodeSchema_Interface" />
           <text x="38.142450422468755" y="227.919797731" fill="#FFFFFF">IServerManager</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#1382CE" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Log)">
           <rect x="116.88198493083348" y="264.969897731" rx="5" ry="5" width="80.74666666666667" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="136.88198493083348" y="269.969897731" xlink:href="#CodeSchema_Class" />
           <text x="157.88198493083348" y="282.919897731" fill="#FFFFFF">Log</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=NotifyJoinedServiceEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=NotifyJoinedServiceEvent)">
           <rect x="-72.739416244197969" y="319.96999773100003" rx="5" ry="5" width="194.14333333333298" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-53.739416244197969" y="324.96999773100003" xlink:href="#CodeSchema_Class" />
           <text x="-32.739416244197969" y="337.919997731" fill="#FFFFFF">NotifyJoinedServiceEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterClientEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterClientEvent)">
           <rect x="-462.074416244198" y="374.96984773100019" rx="5" ry="5" width="163.01333333333298" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-443.074416244198" y="379.96984773100019" xlink:href="#CodeSchema_Class" />
           <text x="-422.074416244198" y="392.91984773100017" fill="#FFFFFF">RegisterClientEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterServerEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=RegisterServerEvent)">
           <rect x="-268.39608291086495" y="374.96984773100007" rx="5" ry="5" width="165.65666666666698" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-248.39608291086495" y="379.96984773100007" xlink:href="#CodeSchema_Class" />
           <text x="-227.39608291086495" y="392.91984773100006" fill="#FFFFFF">RegisterServerEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=Server)">
           <rect x="53.614995118542765" y="154.969697731" rx="5" ry="5" width="94.019999999999982" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="72.614995118542765" y="159.969697731" xlink:href="#CodeSchema_Class" />
           <text x="93.614995118542765" y="172.91969773099999" fill="#FFFFFF">Server</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteRequestEvent)">
           <rect x="227.6287515974999" y="264.96989773099995" rx="5" ry="5" width="156.41000000000008" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="247.6287515974999" y="269.96989773099995" xlink:href="#CodeSchema_Class" />
           <text x="268.6287515974999" y="282.91989773099994" fill="#FFFFFF">VoteRequestEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=VoteResponseEvent)">
           <rect x="-77.571448402499385" y="264.96989773099995" rx="5" ry="5" width="164.45333333333309" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-58.571448402499385" y="269.96989773099995" xlink:href="#CodeSchema_Class" />
           <text x="-37.571448402499385" y="282.91989773099994" fill="#FFFFFF">VoteResponseEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesRequestEvent)">
           <rect x="172.65255042246884" y="209.96979773099997" rx="5" ry="5" width="229.45000000000005" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="192.65255042246884" y="214.96979773099997" xlink:href="#CodeSchema_Class" />
           <text x="213.65255042246884" y="227.91979773099996" fill="#FFFFFF">AppendLogEntriesRequestEvent</text>
           <rect x="INF" y="INF" width="-INF" height="-INF" fill="#1E1E1E" stroke="#0E70C0" stroke-width="1" />
         </g>
-        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net7.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesResponseEvent)">
+        <g id="(Assembly=file:///D:/git/microsoft/CoyoteSamples/bin/net8.0/Raft.dll Namespace=Microsoft.Coyote.Samples.CloudMessaging Type=AppendLogEntriesResponseEvent)">
           <rect x="-462.07441624419795" y="209.96984773100016" rx="5" ry="5" width="237.493333333333" height="25" fill="#0E70C0" stroke="#0E70C0" stroke-width="1" />
           <use x="-443.07441624419795" y="214.96984773100016" xlink:href="#CodeSchema_Class" />
           <text x="-422.07441624419795" y="227.91984773100015" fill="#FFFFFF">AppendLogEntriesResponseEvent</text>
diff --git a/docs/assets/images/core.dgml b/docs/assets/images/core.dgml
index 4746b3610..f93dbaf89 100644
--- a/docs/assets/images/core.dgml
+++ b/docs/assets/images/core.dgml
@@ -1884,7 +1884,7 @@
     </Style>
   </Styles>
   <Paths>
-    <Path Id="e75db9c9-7842-4ae4-a29d-624f6b49f607.OutputPath" Value="C:\git\coyote\bin\net7.0\Microsoft.Coyote.dll" />
-    <Path Id="e75db9c9-7842-4ae4-a29d-624f6b49f607.OutputPathUri" Value="file:///C:/git/coyote/bin/net7.0/Microsoft.Coyote.dll" />
+    <Path Id="e75db9c9-7842-4ae4-a29d-624f6b49f607.OutputPath" Value="C:\git\coyote\bin\net8.0\Microsoft.Coyote.dll" />
+    <Path Id="e75db9c9-7842-4ae4-a29d-624f6b49f607.OutputPathUri" Value="file:///C:/git/coyote/bin/net8.0/Microsoft.Coyote.dll" />
   </Paths>
 </DirectedGraph>
\ No newline at end of file
diff --git a/docs/concepts/binary-rewriting.md b/docs/concepts/binary-rewriting.md
index 4db863576..31a82f46b 100644
--- a/docs/concepts/binary-rewriting.md
+++ b/docs/concepts/binary-rewriting.md
@@ -33,8 +33,8 @@ file, which looks like this example:
 
 ```json
 {
-  "AssembliesPath": "bin/net7.0",
-  "OutputPath": "bin/net7.0/rewritten",
+  "AssembliesPath": "bin/net8.0",
+  "OutputPath": "bin/net8.0/rewritten",
   "Assemblies": [
     "BoundedBuffer.dll",
     "MyOtherLibrary.dll",
diff --git a/docs/get-started/build-source.md b/docs/get-started/build-source.md
index 921ab8644..feb7493ae 100644
--- a/docs/get-started/build-source.md
+++ b/docs/get-started/build-source.md
@@ -8,7 +8,7 @@ the github repo</a>
 
 ### Prerequisites
 
-- [.NET 7.0 SDK](https://dotnet.microsoft.com/download/dotnet)
+- [.NET 8.0 SDK](https://dotnet.microsoft.com/download/dotnet)
 
 **Optional:**
 
diff --git a/docs/get-started/install.md b/docs/get-started/install.md
index eb189ccfe..d093290ad 100644
--- a/docs/get-started/install.md
+++ b/docs/get-started/install.md
@@ -10,7 +10,7 @@ frameworks supported by Coyote:
 
 | Target Framework      | Operating System      |
 | :-------------------: | :-------------------: |
-| .NET 7.0              | Linux, macOS, Windows |
+| .NET 8.0              | Linux, macOS, Windows |
 | .NET 6.0              | Linux, macOS, Windows |
 | .NET Core 3.1         | Linux, macOS, Windows |
 | .NET Standard 2.0     | Linux, macOS, Windows |
diff --git a/docs/get-started/using-coyote.md b/docs/get-started/using-coyote.md
index b2731704d..30c8abde1 100644
--- a/docs/get-started/using-coyote.md
+++ b/docs/get-started/using-coyote.md
@@ -216,7 +216,7 @@ explore Coyote further!
 **Format of the executable (.exe) or library (.dll) is invalid.**
 
 If you are using a .NET Core target platform then on Windows you will get executable program with
-`.exe` file extension, like `coyote\Samples\bin\net7.0\BoundedBuffer.exe` These are not
+`.exe` file extension, like `coyote\Samples\bin\net8.0\BoundedBuffer.exe` These are not
 rewritable assemblies. You must instead rewrite and test the associated library, in this case
 `BoundedBuffer.dll`.
 
diff --git a/docs/how-to/coverage.md b/docs/how-to/coverage.md
index 1d2a69fc9..9634b7a70 100644
--- a/docs/how-to/coverage.md
+++ b/docs/how-to/coverage.md
@@ -89,14 +89,14 @@ Then run `coyote` with one of the coverage flags, as well as the other options y
 some minimal examples:
 
 ```plain
-coyote test ./bin/net7.0/Monitors.exe -i 10 --coverage
+coyote test ./bin/net8.0/Monitors.exe -i 10 --coverage
 ```
 
-This will create the directory `./bin/net7.0/Output/Monitors.exe/CoyoteOutput/`, then it
+This will create the directory `./bin/net8.0/Output/Monitors.exe/CoyoteOutput/`, then it
 generates coverage files for code coverage which you can load into Visual Studio to see the results.
 
 ```plain
-coyote test ./bin/net7.0/Monitors.exe -i 10 -coverage activity  -o "/Coyote_Coverage/Monitors"
+coyote test ./bin/net8.0/Monitors.exe -i 10 -coverage activity  -o "/Coyote_Coverage/Monitors"
 ```
 
 This will create the directory `/Coyote_Coverage/Monitors/CoyoteOutput`, then it generates only
diff --git a/docs/how-to/liveness-checking.md b/docs/how-to/liveness-checking.md
index fa7e91b32..a2c3b7473 100644
--- a/docs/how-to/liveness-checking.md
+++ b/docs/how-to/liveness-checking.md
@@ -29,7 +29,7 @@ the [coyote tool](../get-started/using-coyote.md) as follows, setting N steps as
 From the [samples](https://github.com/microsoft/coyote/tree/main/Samples) directory:
 
 ```plain
-coyote test ./Samples/bin/net7.0/CoffeeMachineActors.dll -i 10 -ms 200 -s portfolio
+coyote test ./Samples/bin/net8.0/CoffeeMachineActors.dll -i 10 -ms 200 -s portfolio
 ```
 
 The `coyote test` tool will produce output, ending with something like the following:
@@ -52,7 +52,7 @@ averaging 457 steps. Going by this output, let's decide to increase the bound to
 `coyote test`.
 
 ```plain
-coyote test ./Samples/bin/net7.0/CoffeeMachineActors.dll -i 10 -ms 1000 -s portfolio
+coyote test ./Samples/bin/net8.0/CoffeeMachineActors.dll -i 10 -ms 1000 -s portfolio
 ```
 
 This time the output will be something like:
diff --git a/docs/how-to/unit-testing.md b/docs/how-to/unit-testing.md
index b3691fc07..ca21ee32d 100644
--- a/docs/how-to/unit-testing.md
+++ b/docs/how-to/unit-testing.md
@@ -16,7 +16,7 @@ a complete example using xUnit. The project simply includes xUnit and the Coyote
 ```xml
 <Project Sdk="Microsoft.NET.Sdk">
   <PropertyGroup>
-    <TargetFramework>net7.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
   </PropertyGroup>
   <ItemGroup>
     <PackageReference Include="Microsoft.Coyote" Version="1.4.1" />
diff --git a/docs/samples/actors/failover-robot-navigator.md b/docs/samples/actors/failover-robot-navigator.md
index 1a16d6ea3..5aaacfe59 100644
--- a/docs/samples/actors/failover-robot-navigator.md
+++ b/docs/samples/actors/failover-robot-navigator.md
@@ -110,7 +110,7 @@ before coding and pushing to production.
 To run the `DrinksServingRobotActors` example, you will need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -124,7 +124,7 @@ You can build the sample by following the instructions
 Now you can run the `DrinksServingRobotActors` application:
 
 ```plain
-./Samples/bin/net7.0/DrinksServingRobotActors.exe
+./Samples/bin/net8.0/DrinksServingRobotActors.exe
 ```
 
 When you run the executable like this without using `coyote test` (this is called running in
@@ -238,13 +238,13 @@ You can now use `coyote test` to test the code and see if any bugs can be found.
 `CoyoteSamples` folder enter this command:
 
 ```plain
-coyote test ./Samples/bin/net7.0/DrinksServingRobotActors.dll -i 1000 -ms 2000 -s prioritization -sv 10
+coyote test ./Samples/bin/net8.0/DrinksServingRobotActors.dll -i 1000 -ms 2000 -s prioritization -sv 10
 ```
 
 Chances are this will find a bug quickly, and you will see output from the test like this:
 
 ```plain
-. Testing .\Samples\bin\net7.0\DrinksServingRobotActors.exe
+. Testing .\Samples\bin\net8.0\DrinksServingRobotActors.exe
 Starting TestingProcessScheduler in process 26236
 ... Created '1' testing task.
 ... Task 0 is using 'prioritization' strategy (seed:324932188).
@@ -275,7 +275,7 @@ Starting TestingProcessScheduler in process 26236
 ```
 
 Notice that a log file is produced
-`.bin\net7.0\Output\DrinksServingRobot.exe\CoyoteOutput\DrinksServingRobot_0_1.txt`. This log can be
+`.bin\net8.0\Output\DrinksServingRobot.exe\CoyoteOutput\DrinksServingRobot_0_1.txt`. This log can be
 pretty big, it contains the test iteration that failed, and towards the end of this file you will
 see something like this:
 
@@ -471,7 +471,7 @@ liveness bug in hot state 'Busy' at the end of program execution.
 If you add to the coyote test command line `--actor-graph`, and test again:
 
 ```plain
-coyote test .\Samples\bin\net7.0\DrinksServingRobotActors.dll -i 1000 -ms 2000 -s prioritization -sv 10 --actor-graph
+coyote test .\Samples\bin\net8.0\DrinksServingRobotActors.dll -i 1000 -ms 2000 -s prioritization -sv 10 --actor-graph
 ```
 
 you'll see in the output of the tester that a DGML diagram has been produced:
@@ -640,7 +640,7 @@ After you perform this fix and rebuild the sample, try running coyote test again
 command line which previously reported the liveness bug:
 
 ```plain
-coyote test ./Samples/bin/net7.0/DrinksServingRobotActors.dll -i 1000 -ms 2000 -s prioritization -sv 10
+coyote test ./Samples/bin/net8.0/DrinksServingRobotActors.dll -i 1000 -ms 2000 -s prioritization -sv 10
 ```
 
 And now no bug will be found -- you should get result similar to this:
diff --git a/docs/samples/actors/failure-detector.md b/docs/samples/actors/failure-detector.md
index 1b5bd80ba..666851845 100644
--- a/docs/samples/actors/failure-detector.md
+++ b/docs/samples/actors/failure-detector.md
@@ -11,7 +11,7 @@ late at night scratching your head. Read further to learn how to find this bug u
 You will also need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -26,7 +26,7 @@ Let's see if Coyote can find the bug in this sample. Type `coyote -?` to see the
 sure you have installed it correctly. Now you are ready to run a `coyote` test as follows:
 
 ```plain
-coyote test ./Samples/bin/net7.0/Monitors.dll --iterations 1000 -ms 200
+coyote test ./Samples/bin/net8.0/Monitors.dll --iterations 1000 -ms 200
 ```
 
 This also runs perfectly up to 1000 iterations. So this is indeed a hard bug to find. It can be
@@ -35,7 +35,7 @@ points `--strategy prioritization` (or with the default `random` exploration str
 much larger number of iterations, typically more than 100,000 of them).
 
 ```plain
-coyote test ./Samples/bin/net7.0/Monitors.dll --iterations 1000 -ms 200 -s prioritization -sv 10
+coyote test ./Samples/bin/net8.0/Monitors.dll --iterations 1000 -ms 200 -s prioritization -sv 10
 ```
 
 Even then you might need to run it a few times to catch the bug. Set `--iterations` to a bigger
@@ -48,8 +48,8 @@ strategy, you will see a bug report:
 ```plain
 ... Task 0 found a bug.
 ... Emitting task 0 traces:
-..... Writing .\Samples\bin\net7.0\Output\Monitors.exe\CoyoteOutput\Monitors_0_0.txt
-..... Writing .\Samples\bin\net7.0\Output\Monitors.exe\CoyoteOutput\Monitors_0_0.trace
+..... Writing .\Samples\bin\net8.0\Output\Monitors.exe\CoyoteOutput\Monitors_0_0.txt
+..... Writing .\Samples\bin\net8.0\Output\Monitors.exe\CoyoteOutput\Monitors_0_0.trace
 ```
 
 The `*.txt` file is the text log of the iteration that found the bug. The `*.trace` contains the
@@ -59,10 +59,10 @@ Finding a hard to find bug is one thing, but if you can't reproduce this bug whi
 is no point. So the `*.trace` can be used with the `coyote replay` command as follows:
 
 ```plain
-coyote replay ./Samples/bin/net7.0/Monitors.dll 
-    .\Samples\bin\net7.0\Output\Monitors.exe\CoyoteOutput\Monitors_0_0.trace
+coyote replay ./Samples/bin/net8.0/Monitors.dll 
+    .\Samples\bin\net8.0\Output\Monitors.exe\CoyoteOutput\Monitors_0_0.trace
     
-. Reproducing trace in ./Samples/bin/net7.0/Monitors.exe
+. Reproducing trace in ./Samples/bin/net8.0/Monitors.exe
 ... Reproduced 1 bug.
 ... Elapsed 0.1724228 sec.
 ```
@@ -74,14 +74,14 @@ tool can help you with that also. If you run the following command line it will
 diagram of the state machines that are being tested:
 
 ```plain
-coyote test ./Samples/bin/net7.0/Monitors.dll --iterations 10 --max-steps 20 --actor-graph
+coyote test ./Samples/bin/net8.0/Monitors.dll --iterations 10 --max-steps 20 --actor-graph
 ```
 
 You will see the following output:
 
 ```plain
 ... Emitting graph:
-..... Writing .\Samples\bin\net7.0\Output\Monitors.exe\CoyoteOutput\Monitors_0_1.dgml
+..... Writing .\Samples\bin\net8.0\Output\Monitors.exe\CoyoteOutput\Monitors_0_1.dgml
 ```
 
 Open the DGML diagram using Visual Studio 2022 and you will see the following:
diff --git a/docs/samples/tasks/bounded-buffer.md b/docs/samples/tasks/bounded-buffer.md
index 102878ef1..0905315b8 100644
--- a/docs/samples/tasks/bounded-buffer.md
+++ b/docs/samples/tasks/bounded-buffer.md
@@ -10,7 +10,7 @@ article](https://cloudblogs.microsoft.com/opensource/2020/07/14/extreme-programm
 To run the `BoundedBuffer` example, you will need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -25,13 +25,13 @@ Now you can run the `BoundedBuffer` application in a mode that should trigger th
 the time:
 
 ```plain
-./Samples/bin/net7.0/BoundedBuffer.exe -m
+./Samples/bin/net8.0/BoundedBuffer.exe -m
 ```
 
 And you can run it with a fix for the deadlock as follows:
 
 ```plain
-./Samples/bin/net7.0/BoundedBuffer.exe -f
+./Samples/bin/net8.0/BoundedBuffer.exe -f
 ```
 
 ### Can you find the deadlock bug in BoundedBuffer class?
diff --git a/docs/tutorials/actors/hello-world.md b/docs/tutorials/actors/hello-world.md
index 3c35733f5..5f024dc4b 100644
--- a/docs/tutorials/actors/hello-world.md
+++ b/docs/tutorials/actors/hello-world.md
@@ -10,7 +10,7 @@ model](../../concepts/actors/overview.md).
 To run the Hello World Actors  example, you will need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -24,7 +24,7 @@ You can build the sample by following the instructions
 Now you can run the HelloWorldActors application:
 
 ```plain
-"./Samples/bin/net7.0/HelloWorldActors.exe"
+"./Samples/bin/net8.0/HelloWorldActors.exe"
 ```
 
 Press the ENTER key to terminate the program when it is done. Note that a bug has been inserted into
@@ -59,13 +59,13 @@ find the `coyote` test tool and setup your environment to use it.
 Enter the following from the command line:
 
 ```plain
-coyote test ./Samples/bin/net7.0/HelloWorldActors.dll --iterations 30
+coyote test ./Samples/bin/net8.0/HelloWorldActors.dll --iterations 30
 ```
 
 The result is:
 
 ```plain
-. Testing .\Samples\bin\net7.0\HelloWorldActors.dll
+. Testing .\Samples\bin\net8.0\HelloWorldActors.dll
 Starting TestingProcessScheduler in process 16432
 ... Created '1' testing task.
 ... Task 0 is using 'random' strategy (seed:308255541).
@@ -73,8 +73,8 @@ Starting TestingProcessScheduler in process 16432
 ..... Iteration #2
 ... Task 0 found a bug.
 ... Emitting task 0 traces:
-..... Writing .\Samples\bin\net7.0\Output\HelloWorldActors.exe\CoyoteOutput\HelloWorldActors_0_2.txt
-..... Writing .\Samples\bin\net7.0\Output\HelloWorldActors.exe\CoyoteOutput\HelloWorldActors_0_2.trace
+..... Writing .\Samples\bin\net8.0\Output\HelloWorldActors.exe\CoyoteOutput\HelloWorldActors_0_2.txt
+..... Writing .\Samples\bin\net8.0\Output\HelloWorldActors.exe\CoyoteOutput\HelloWorldActors_0_2.trace
 ... Elapsed 0.0906639 sec.
 ... Testing statistics:
 ..... Found 1 bug.
@@ -240,7 +240,7 @@ tool has ways of interrupting and restarting this `Execute` method based on `--i
 So now you know what happened when you ran the following command line:
 
 ```plain
-coyote test ./Samples/bin/net7.0/HelloWorldActors.exe --iterations 30
+coyote test ./Samples/bin/net8.0/HelloWorldActors.exe --iterations 30
 ```
 
 A special coyote `TestingEngine` was created, it invoked the `Execute` method 30 times, and during
diff --git a/docs/tutorials/actors/raft-azure.md b/docs/tutorials/actors/raft-azure.md
index b8a59414f..a20a09a83 100644
--- a/docs/tutorials/actors/raft-azure.md
+++ b/docs/tutorials/actors/raft-azure.md
@@ -31,7 +31,7 @@ is called the `Azure CLI`.
 You will also need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -64,7 +64,7 @@ You can build the sample by following the instructions
 Now you can run the Raft.Azure application:
 
 ```plain
-"./Samples/bin/net7.0/Raft.Azure.exe" --connection-string "%CONNECTION_STRING%" --topic-name rafttopic --num-requests 5 --local-cluster-size 5
+"./Samples/bin/net8.0/Raft.Azure.exe" --connection-string "%CONNECTION_STRING%" --topic-name rafttopic --num-requests 5 --local-cluster-size 5
 ```
 
 Note: you don't want to try and run Raft.Azure client using the `coyote test` tool until you
diff --git a/docs/tutorials/actors/raft-mocking.md b/docs/tutorials/actors/raft-mocking.md
index b8eaef301..e854df5c7 100644
--- a/docs/tutorials/actors/raft-mocking.md
+++ b/docs/tutorials/actors/raft-mocking.md
@@ -19,7 +19,7 @@ you achieve a high level of confidence that the code is rock solid.
 You will also need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -33,12 +33,12 @@ You can build the sample by following the instructions
 Now you can run `coyote test` tool on the Raft.Mocking application:
 
 ```plain
-coyote test ./Samples/bin/net7.0/Raft.Mocking.dll -i 1000 -ms 200 --coverage activity
+coyote test ./Samples/bin/net8.0/Raft.Mocking.dll -i 1000 -ms 200 --coverage activity
 ```
 
 You should see the test succeed with output like this, including a coverage report and graph:
 ```plain
-. Testing ./Samples/bin/net7.0/Raft.Mocking.dll
+. Testing ./Samples/bin/net8.0/Raft.Mocking.dll
 Starting TestingProcessScheduler in process 34068
 ... Created '1' testing task.
 ... Task 0 is using 'random' strategy (seed:1388735316).
@@ -49,9 +49,9 @@ Starting TestingProcessScheduler in process 34068
 ..... Iteration #900
 ..... Iteration #1000
 ... Emitting coverage reports:
-..... Writing .\Samples\bin\net7.0\Output\Raft.Mocking.dll\CoyoteOutput\Raft.Mocking.dgml
-..... Writing .\Samples\bin\net7.0\Output\Raft.Mocking.dll\CoyoteOutput\Raft.Mocking.coverage.txt
-..... Writing .\Samples\bin\net7.0\Output\Raft.Mocking.dll\CoyoteOutput\Raft.Mocking.coverage.ser
+..... Writing .\Samples\bin\net8.0\Output\Raft.Mocking.dll\CoyoteOutput\Raft.Mocking.dgml
+..... Writing .\Samples\bin\net8.0\Output\Raft.Mocking.dll\CoyoteOutput\Raft.Mocking.coverage.txt
+..... Writing .\Samples\bin\net8.0\Output\Raft.Mocking.dll\CoyoteOutput\Raft.Mocking.coverage.ser
 ... Testing statistics:
 ..... Found 0 bugs.
 ... Exploration statistics:
@@ -127,7 +127,7 @@ async operations. The last option is interesting because it allows you to test m
 scheduling strategies at once:
 
 ```plain
-coyote test ./Samples/bin/net7.0/Raft.Mocking.dll -i 1000 -ms 200 --coverage activity -s portfolio
+coyote test ./Samples/bin/net8.0/Raft.Mocking.dll -i 1000 -ms 200 --coverage activity -s portfolio
 ```
 
 When you use this the test will print the chosen strategies at the top of the test output:
diff --git a/docs/tutorials/actors/test-failover.md b/docs/tutorials/actors/test-failover.md
index a7da6c643..fb22c0744 100644
--- a/docs/tutorials/actors/test-failover.md
+++ b/docs/tutorials/actors/test-failover.md
@@ -64,7 +64,7 @@ it happens after failover just to prove the usefulness of this testing methodolo
 To run the `CoffeeMachine` example, you will need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -78,7 +78,7 @@ You can build the sample by following the instructions
 Now you can run the `CoffeeMachine` application:
 
 ```plain
-./Samples/bin/net7.0/CoffeeMachineActors.exe
+./Samples/bin/net8.0/CoffeeMachineActors.exe
 ```
 
 ## The coffee machine
@@ -189,15 +189,15 @@ You can now use [coyote test](../../get-started/using-coyote.md) to exercise the
 can be found. From the [samples](https://github.com/microsoft/coyote/tree/main/Samples) directory:
 
 ```plain
-coyote test ./Samples/bin/net7.0/CoffeeMachineActors.dll -i 100 -ms 2000 -s prioritization -sv 10 --actor-graph
+coyote test ./Samples/bin/net8.0/CoffeeMachineActors.dll -i 100 -ms 2000 -s prioritization -sv 10 --actor-graph
 ```
 
 Chances are this will find a bug quickly, one of the safety assertions will fire and you will see
 that a test output log and a DGML diagram are produced, like this:
 
 ```plain
-.\Samples\bin\net7.0\Output\CoffeeMachineActors.exe\CoyoteOutput\CoffeeMachine_0_0.txt
-.\Samples\bin\net7.0\Output\CoffeeMachineActors.exe\CoyoteOutput\CoffeeMachine_0_0.dgml
+.\Samples\bin\net8.0\Output\CoffeeMachineActors.exe\CoyoteOutput\CoffeeMachine_0_0.txt
+.\Samples\bin\net8.0\Output\CoffeeMachineActors.exe\CoyoteOutput\CoffeeMachine_0_0.dgml
 ```
 
 This log can be pretty big, a couple thousand lines where each line represents one async operation.
diff --git a/docs/tutorials/first-concurrency-unit-test.md b/docs/tutorials/first-concurrency-unit-test.md
index dc90882aa..5dfedf9d5 100644
--- a/docs/tutorials/first-concurrency-unit-test.md
+++ b/docs/tutorials/first-concurrency-unit-test.md
@@ -17,7 +17,7 @@ you in writing correct concurrent code.
 To run the code in this tutorial, you will need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -410,7 +410,7 @@ You can build the sample by following the instructions
 You can now run the tests (without Coyote) like this:
 
 ```plain
-cd .\Samples\bin\net7.0
+cd .\Samples\bin\net8.0
 .\AccountManager.exe
 ```
 
diff --git a/docs/tutorials/mocks/mock-dependencies.md b/docs/tutorials/mocks/mock-dependencies.md
index 0d7122a94..3cd98f4cc 100644
--- a/docs/tutorials/mocks/mock-dependencies.md
+++ b/docs/tutorials/mocks/mock-dependencies.md
@@ -24,7 +24,7 @@ means that using locks in your code will not help you in writing correct concurr
 To run the code in this tutorial, you will need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 - Go through the [write your first concurrency unit test](../first-concurrency-unit-test.md) tutorial.
diff --git a/docs/tutorials/mocks/optimistic-concurrency-control.md b/docs/tutorials/mocks/optimistic-concurrency-control.md
index 714530d11..44287b059 100644
--- a/docs/tutorials/mocks/optimistic-concurrency-control.md
+++ b/docs/tutorials/mocks/optimistic-concurrency-control.md
@@ -27,7 +27,7 @@ trivial.
 To run the code in this tutorial, you will need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 - Go through the [mocking dependencies for testing](mock-dependencies.md) tutorial.
diff --git a/docs/tutorials/test-concurrent-operations.md b/docs/tutorials/test-concurrent-operations.md
index 511a23bd5..fd10f43f8 100644
--- a/docs/tutorials/test-concurrent-operations.md
+++ b/docs/tutorials/test-concurrent-operations.md
@@ -14,7 +14,7 @@ In this follow-up tutorial, you will write a few more tests that exercise the co
 To run the code in this tutorial, you will need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 - Go through the [write your first concurrency unit test](first-concurrency-unit-test.md) tutorial.
diff --git a/docs/tutorials/test-failover.md b/docs/tutorials/test-failover.md
index 49c849cc5..30c7bd7cb 100644
--- a/docs/tutorials/test-failover.md
+++ b/docs/tutorials/test-failover.md
@@ -60,7 +60,7 @@ it happens after failover just to prove the usefulness of this testing methodolo
 To run the `CoffeeMachine` example, you will need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -74,7 +74,7 @@ You can build the sample by following the instructions
 Now you can run the `CoffeeMachine` application:
 
 ```plain
-./Samples/bin/net7.0/CoffeeMachineTasks.exe
+./Samples/bin/net8.0/CoffeeMachineTasks.exe
 ```
 
 ## The Coffee Machine
@@ -182,20 +182,20 @@ You can now use [coyote test](../get-started/using-coyote.md) to exercise the co
 bugs can be found. First you need to rewrite the assembly, from the `Samples` directory:
 
 ```plain
-coyote rewrite ./Samples/bin/net7.0/CoffeeMachineTasks.dll
+coyote rewrite ./Samples/bin/net8.0/CoffeeMachineTasks.dll
 ```
 
 Then you can run the test:
 
 ```plain
-coyote test ./Samples/bin/net7.0/CoffeeMachineTasks.dll -i 1000 -ms 500 -s fair-prioritization -sv 10
+coyote test ./Samples/bin/net8.0/CoffeeMachineTasks.dll -i 1000 -ms 500 -s fair-prioritization -sv 10
 ```
 
 Chances are this will find a bug quickly, one of the safety assertions will fire and you will see
 that a test output log is produced, like this:
 
 ```plain
-.\Samples\bin\net7.0\Output\CoffeeMachineTasks.exe\CoyoteOutput\CoffeeMachine_0_0.txt
+.\Samples\bin\net8.0\Output\CoffeeMachineTasks.exe\CoyoteOutput\CoffeeMachine_0_0.txt
 ```
 
 This log contains only the one test iteration that failed, and towards the end you will see
diff --git a/docs/tutorials/testing-aspnet-service.md b/docs/tutorials/testing-aspnet-service.md
index a1610a3b4..6d376e82c 100644
--- a/docs/tutorials/testing-aspnet-service.md
+++ b/docs/tutorials/testing-aspnet-service.md
@@ -12,7 +12,7 @@ Coyote and you can run the web front end using the Azure storage emulators.
 You will also need to:
 
 - Install [Visual Studio 2022](https://visualstudio.microsoft.com/downloads/).
-- Install the [.NET 7.0 version of the coyote tool](../get-started/install.md).
+- Install the [.NET 8.0 version of the coyote tool](../get-started/install.md).
 - Be familiar with the `coyote` tool. See [using Coyote](../get-started/using-coyote.md).
 - Clone the [Coyote git repo](http://github.com/microsoft/coyote).
 
@@ -155,7 +155,7 @@ Just run them from inside Visual Studio, or run the following:
 
 ```
 cd Samples/WebApps/ImageGalleryAspNet/
-dotnet test bin/net7.0/ImageGalleryTests.dll
+dotnet test bin/net8.0/ImageGalleryTests.dll
 ```
 
 The tests may or may not trigger the bug! Most likely you will see this output:
diff --git a/global.json b/global.json
index 06ce1b485..e72335a83 100644
--- a/global.json
+++ b/global.json
@@ -1,5 +1,5 @@
 {
   "sdk": {
-    "version": "7.0.400"
+    "version": "8.0.201"
   }
 }