diff --git a/.github/workflows/dafny_interop_library_go_tests.yml b/.github/workflows/dafny_interop_library_go_tests.yml
index f00bd7625..9bc434325 100644
--- a/.github/workflows/dafny_interop_library_go_tests.yml
+++ b/.github/workflows/dafny_interop_library_go_tests.yml
@@ -23,7 +23,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        library: [TestVectors]
+        library: [AwsEncryptionSDK, TestVectors]
         go-version: ["1.23"]
         os: [
             # Sed script doesn't work properly on windows
@@ -97,8 +97,32 @@ jobs:
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_go CORES=$CORES
 
+      - name: Unzip .NET Retry Flag Manifests
+        if: matrix.library == 'TestVectors'
+        shell: bash
+        working-directory: TestVectors/dafny/TestVectors/test/
+        run: |
+          unzip invalid-Net-4.0.0.zip -d invalid-Net-4.0.0
+          unzip v4-Net-4.0.1.zip -d v4-Net-4.0.1
+          unzip valid-Net-4.0.0.zip -d valid-Net-4.0.0
+
+      # TODO: Remove this after Go polymorph does not generate unwanted duplicate code.
+      - name: Purge polymorph code in Go
+        if: matrix.library == 'TestVectors'
+        working-directory: ./${{ matrix.library }}
+        shell: bash
+        run: |
+          make purge_polymorph_code
+
       - name: Test Go
         working-directory: ${{ matrix.library }}
         shell: bash
         run: |
           make test_go
+
+      - name: Test Examples for Go
+        if: matrix.library == 'AwsEncryptionSDK'
+        working-directory: ${{ matrix.library }}/runtimes/go/examples
+        shell: bash
+        run: |
+          go run main.go
diff --git a/.github/workflows/dafny_interop_test_net.yml b/.github/workflows/dafny_interop_test_net.yml
index c2a0cc9ac..b709d31d7 100644
--- a/.github/workflows/dafny_interop_test_net.yml
+++ b/.github/workflows/dafny_interop_test_net.yml
@@ -34,7 +34,12 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [windows-latest, ubuntu-22.04, macos-15]
+        os: [
+            windows-latest,
+            ubuntu-22.04,
+            # TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
+            # macos-15,
+          ]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
diff --git a/.github/workflows/dafny_interop_test_vector_net.yml b/.github/workflows/dafny_interop_test_vector_net.yml
index d45f8a61e..81aadd5f5 100644
--- a/.github/workflows/dafny_interop_test_vector_net.yml
+++ b/.github/workflows/dafny_interop_test_vector_net.yml
@@ -33,7 +33,12 @@ jobs:
   decrypt_python_vectors:
     strategy:
       matrix:
-        os: [windows-latest, ubuntu-22.04, macos-15]
+        os: [
+            windows-latest,
+            ubuntu-22.04,
+            # TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
+            # macos-15,
+          ]
     runs-on: ${{matrix.os}}
     permissions:
       id-token: write
@@ -140,7 +145,11 @@ jobs:
   generate_vectors:
     strategy:
       matrix:
-        os: [ubuntu-22.04, macos-15]
+        os: [
+            ubuntu-22.04,
+            # TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
+            # macos-15,
+          ]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
@@ -242,7 +251,11 @@ jobs:
     needs: generate_vectors
     strategy:
       matrix:
-        os: [ubuntu-22.04, macos-15]
+        os: [
+            ubuntu-22.04,
+            # TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
+            # macos-15,
+          ]
     runs-on: ${{ matrix.os }}
     permissions:
       id-token: write
diff --git a/AwsEncryptionSDK/runtimes/net/ESDK.csproj b/AwsEncryptionSDK/runtimes/net/ESDK.csproj
index 2dcdef83b..24f8b5ddd 100644
--- a/AwsEncryptionSDK/runtimes/net/ESDK.csproj
+++ b/AwsEncryptionSDK/runtimes/net/ESDK.csproj
@@ -28,9 +28,33 @@
       
   </PropertyGroup>
 
+  <PropertyGroup>
+    <!-- This is somewhat brittle,
+         but having the value in a properties file
+         that can be shared is worth it.
+         See: https://learn.microsoft.com/en-us/visualstudio/msbuild/property-functions?view=vs-2022
+         for more details on property functions
+         
+         This takes a properties file (a=b)
+         1. Loads the file
+         2. Splits on `dafnyVersion=` and takes everything to the right of that
+           e.g. the version + any trailing data
+         3. Splits on newline and takes the second element.
+           This SHOULD be the value of `dafnyVersion` and not contain any trailing data
+     -->
+    <projectProperties>
+      $([System.IO.File]::ReadAllText('$(MSBuildProjectDirectory)/../../../project.properties'))
+    </projectProperties>
+    <dropBeforeDafnyVersionProperty>
+      $([System.Text.RegularExpressions.Regex]::Split("$(projectProperties)", "dafnyVersion=")[1])
+    </dropBeforeDafnyVersionProperty>
+    <DafnyVersion>
+      $([System.Text.RegularExpressions.Regex]::Split("$(dropBeforeDafnyVersionProperty)", "\n")[1])
+    </DafnyVersion>
+  </PropertyGroup>
+
   <ItemGroup>
-      <!-- TODO: manually upgraded to match the latest from MPL, is that reasonable? -->
-      <PackageReference Include="DafnyRuntime" Version="4.9.0" />
+      <PackageReference Include="DafnyRuntime" Version="$(DafnyVersion)" />
       <PackageReference Include="BouncyCastle.Cryptography" Version="2.6.2" />
       <ProjectReference Include="../../../mpl/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj" />
       <!--
diff --git a/mpl b/mpl
index 03c999c72..c7fbf370e 160000
--- a/mpl
+++ b/mpl
@@ -1 +1 @@
-Subproject commit 03c999c72426158b06988cc31155454808d6baa1
+Subproject commit c7fbf370ef505a99bf40288a15ee7c91163b4535