diff --git a/.github/workflows/pull.yml b/.github/workflows/pull.yml
index ad9a6d9ca..03f6e18c3 100644
--- a/.github/workflows/pull.yml
+++ b/.github/workflows/pull.yml
@@ -8,20 +8,20 @@ jobs:
   pr-ci-codegen:
     uses: ./.github/workflows/library_codegen.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
   pr-ci-verification:
     uses: ./.github/workflows/library_dafny_verification.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
   # pr-ci-java:
   #   uses: ./.github/workflows/library_java_tests.yml
   #   with:
-  #     dafny: '4.2.0'
+  #     dafny: '4.9.0'
   pr-ci-net:
     uses: ./.github/workflows/library_net_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
   pr-test-vectors:
     uses: ./.github/workflows/library_interop_tests.yml
     with:
-      dafny: '4.2.0'
+      dafny: '4.9.0'
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy
index 695b3379d..1a89973e7 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/AwsEncryptionSdkOperations.dfy
@@ -17,7 +17,7 @@ include "Serialize/EncryptionContext.dfy"
 
 module AwsEncryptionSdkOperations refines AbstractAwsCryptographyEncryptionSdkOperations {
 
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MPL = AwsCryptographyMaterialProvidersTypes
   import MaterialProviders
   import EncryptDecryptHelpers
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy
index 6a3762abe..5825b02cf 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/EncryptDecrypt.dfy
@@ -15,7 +15,7 @@ module EncryptDecryptHelpers {
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
   import MaterialProviders
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MessageBody
   import SerializableTypes
   import opened SerializeFunctions
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy
index cf46c3714..ab851b1a8 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/Index.dfy
@@ -7,7 +7,7 @@ module
   {:extern "software.amazon.cryptography.encryptionsdk.internaldafny" }
   EncryptionSdk refines AbstractAwsCryptographyEncryptionSdkService {
   import Operations = AwsEncryptionSdkOperations
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import MaterialProviders
   import AwsCryptographyMaterialProvidersTypes
 
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy
index 2607f528c..2456f756e 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/KeyDerivation.dfy
@@ -12,7 +12,7 @@ module KeyDerivation {
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
   import AwsCryptographyPrimitivesTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import HeaderTypes
   import SerializableTypes
 
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
index ca62a4d66..794c22838 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy
@@ -22,7 +22,7 @@ module MessageBody {
   import opened UInt = StandardLibrary.UInt
   import Types = AwsCryptographyEncryptionSdkTypes
   import MPL = AwsCryptographyMaterialProvidersTypes
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   import Streams
   import UTF8
   import SerializableTypes
diff --git a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy
index b7edf42a6..f73045a5a 100644
--- a/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy
+++ b/AwsEncryptionSDK/dafny/AwsEncryptionSdk/test/Fixtures.dfy
@@ -9,7 +9,7 @@ module Fixtures {
   import primitivesTypes = AwsCryptographyPrimitivesTypes
   import mplTypes = AwsCryptographyMaterialProvidersTypes
   import opened UInt = StandardLibrary.UInt
-  import Aws.Cryptography.Primitives
+  import Primitives = AtomicPrimitives
   
   // The following are test resources that exist in tests accounts:
 
@@ -20,7 +20,7 @@ module Fixtures {
   
   const branchKeyStoreName := "KeyStoreDdbTable"
   const logicalKeyStoreName := branchKeyStoreName
-  const branchKeyId := "75789115-1deb-4fe3-a2ec-be9e885d1945"
+  const branchKeyId := "3f43a9af-08c5-4317-b694-3d3e883dcaef"
   
   // UTF-8 encoded "aws-crypto-"
   const RESERVED_ENCRYPTION_CONTEXT: UTF8.ValidUTF8Bytes :=
diff --git a/AwsEncryptionSDK/runtimes/net/CHANGELOG.md b/AwsEncryptionSDK/runtimes/net/CHANGELOG.md
index bf9b9eb6a..741db3da1 100644
--- a/AwsEncryptionSDK/runtimes/net/CHANGELOG.md
+++ b/AwsEncryptionSDK/runtimes/net/CHANGELOG.md
@@ -1,5 +1,9 @@
 # Changelog
 
+## 4.1.1
+
+Update .csproj files to prevent use of AWS-SDK-NET V4
+
 ## 4.1.0
 
 ### Notes
diff --git a/AwsEncryptionSDK/runtimes/net/ESDK.csproj b/AwsEncryptionSDK/runtimes/net/ESDK.csproj
index d0332e517..9e8ac6774 100644
--- a/AwsEncryptionSDK/runtimes/net/ESDK.csproj
+++ b/AwsEncryptionSDK/runtimes/net/ESDK.csproj
@@ -8,7 +8,7 @@
       <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
       <IsPackable>true</IsPackable>
       
-      <Version>4.1.0</Version>
+      <Version>4.1.1</Version>
 
       <AssemblyName>AWS.Cryptography.EncryptionSDK</AssemblyName>
       <PackageId>AWS.Cryptography.EncryptionSDK</PackageId>
@@ -29,11 +29,8 @@
   </PropertyGroup>
 
   <ItemGroup>
-      <!-- TODO: manually upgraded to match the latest from MPL, is that reasonable? -->
-      <PackageReference Include="AWSSDK.Core" Version="3.7.300.2" />
-      <PackageReference Include="DafnyRuntime" Version="4.2.0" />
-      <PackageReference Include="BouncyCastle.Cryptography" Version="2.2.1" />
-      <PackageReference Include="AWS.Cryptography.MaterialProviders" Version="1.3.0" />
+      <PackageReference Include="DafnyRuntime" Version="[4.2.0,4.8.0]" />
+      <PackageReference Include="AWS.Cryptography.MaterialProviders" Version="[1.7.6]" />
       <!--
         System.Collections.Immutable can be removed once dafny.msbuild is updated with
         https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned
diff --git a/SharedMakefileV2.mk b/SharedMakefileV2.mk
index 94138dfc6..66d54cf49 100644
--- a/SharedMakefileV2.mk
+++ b/SharedMakefileV2.mk
@@ -6,9 +6,19 @@
 # that are shared by all libraries in this repo.
 PROJECT_ROOT := $(abspath $(dir $(abspath $(lastword $(MAKEFILE_LIST)))))
 
-SMITHY_DAFNY_ROOT := $(PROJECT_ROOT)/smithy-dafny
+SMITHY_DAFNY_ROOT := $(PROJECT_ROOT)/mpl/smithy-dafny
 GRADLEW := ./runtimes/java/gradlew
 
 VERIFY_TIMEOUT := 150
 
 include $(SMITHY_DAFNY_ROOT)/SmithyDafnyMakefile.mk
+
+verify:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+verify_single:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+verify_service:DAFNY_OPTIONS=--allow-deprecation --allow-external-contracts
+
+transpile_implementation_net: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-module-names --allow-external-contracts
+transpile_test_net: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-module-names --allow-external-contracts
+
+transpile_implementation_java: DAFNY_OPTIONS=--allow-warnings --compile-suffix --legacy-data-constructors --legacy-module-names --allow-external-contracts
+transpile_test_java: DAFNY_OPTIONS=--allow-warnings --include-test-runner --compile-suffix --legacy-data-constructors --legacy-module-names --allow-external-contracts
diff --git a/libraries b/libraries
index 05beef6e2..fabf44d71 160000
--- a/libraries
+++ b/libraries
@@ -1 +1 @@
-Subproject commit 05beef6e25a5583abdd4c70c6b09404dfe2fb4cb
+Subproject commit fabf44d71c6d5065b0021cb4e5e96b5128c87d39
diff --git a/mpl b/mpl
index 6d0f00dfa..df37a708c 160000
--- a/mpl
+++ b/mpl
@@ -1 +1 @@
-Subproject commit 6d0f00dfa8c31d490d89399cc104e7d4eac5b9b4
+Subproject commit df37a708cae023ae88a7d0dd0f3ecb59753be5f5