diff --git a/AwsCryptographicMaterialProviders/Makefile b/AwsCryptographicMaterialProviders/Makefile
index e9edc486d..073b42e4e 100644
--- a/AwsCryptographicMaterialProviders/Makefile
+++ b/AwsCryptographicMaterialProviders/Makefile
@@ -12,7 +12,7 @@ PROJECT_SERVICES := \
 SERVICE_NAMESPACE_AwsCryptographicMaterialProviders=aws.cryptography.materialProviders
 SERVICE_NAMESPACE_AwsCryptographyKeyStore=aws.cryptography.keyStore
 
-MAX_RESOURCE_COUNT=50000000
+MAX_RESOURCE_COUNT=60000000
 # Order is important
 # In java they MUST be built
 # in the order they depend on each other
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsArnParsing.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsArnParsing.dfy
index 6aca5ca66..26c4b3baf 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsArnParsing.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AwsArnParsing.dfy
@@ -230,6 +230,13 @@ module AwsArnParsing {
   {}
 
   function method ParseAwsKmsArn(identifier: string): (result: Result<AwsKmsArn, string>)
+    ensures result.Success? ==>
+      && "arn" <= identifier
+      && |Split(identifier, ':')| == 6
+      && |Split(identifier, ':')[1]| > 0
+      && Split(identifier, ':')[2] == "kms"
+      && |Split(identifier, ':')[3]| > 0
+      && |Split(identifier, ':')[4]| > 0
   {
     var components := Split(identifier, ':');
 
@@ -252,6 +259,13 @@ module AwsArnParsing {
   }
 
   function method ParseAmazonDynamodbTableArn(identifier: string): (result: Result<AmazonDynamodbTableArn, string>)
+    ensures result.Success? ==>
+      && "arn" <= identifier
+      && |Split(identifier, ':')| == 6
+      && |Split(identifier, ':')[1]| > 0
+      && Split(identifier, ':')[2] == "dynamodb"
+      && |Split(identifier, ':')[3]| > 0
+      && |Split(identifier, ':')[4]| > 0
   {
     var components := Split(identifier, ':');
 
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy
index ddcbdd5c3..52c4b7406 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy
@@ -182,7 +182,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
       assert (head.Ptr? <==> tail.Ptr?);
     }
 
-    method remove(toRemove: CacheEntry)
+    method {:vcs_split_on_every_assert} remove(toRemove: CacheEntry)
       requires Invariant()
       requires toRemove in Items
       modifies this, Items
@@ -280,6 +280,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
 
     ghost predicate ValidState()
       reads this`Modifies, Modifies - {History}
+      ensures ValidState() ==> History in Modifies
     {
       && History in Modifies
       && this in Modifies
@@ -297,7 +298,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
       // The cache is a cache of Cells, these Cells MUST be unique.
       // The actual value that the Cell contains MAY be a duplicate.
       // See the uniqueness comment on the DoublyLinkedList.Invariant.
-      && (forall k <- cache.Keys(), k' <- cache.Keys() | k != k' :: cache.Select(k) != cache.Select(k'))
+      && MutableMapIsInjective(cache)
       // Given that cache.Values and queue.Items are unique
       // they MUST contain exactly the same elements.
       && multiset(cache.Values()) == multiset(queue.Items)
@@ -410,7 +411,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
     ghost predicate PutCacheEntryEnsuresPublicly(input: Types.PutCacheEntryInput, output: Result<(), Types.Error>)
     {true}
 
-    method PutCacheEntry'(input: Types.PutCacheEntryInput)
+    method {:vcs_split_on_every_assert} PutCacheEntry'(input: Types.PutCacheEntryInput)
       returns (output: Result<(), Types.Error>)
       requires ValidState()
       modifies Modifies - {History}
@@ -484,7 +485,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
     ghost predicate DeleteCacheEntryEnsuresPublicly(input: Types.DeleteCacheEntryInput, output: Result<(), Types.Error>)
     {true}
 
-    method DeleteCacheEntry'(input: Types.DeleteCacheEntryInput)
+    method {:vcs_split_on_every_assert} DeleteCacheEntry'(input: Types.DeleteCacheEntryInput)
       returns (output: Result<(), Types.Error>)
       requires ValidState()
       modifies Modifies - {History}
@@ -510,11 +511,29 @@ module {:options "/functionSyntax:4" } LocalCMC {
         // to keep others from using this value.
         // This is "more" thread safe.
         cache.Remove(input.identifier);
-        assert |cache.Keys()| <= |old@CAN_REMOVE(cache.Keys())|;
+        assert cell !in cache.Values();
+
+        assert MutableMapIsInjective(cache) by {
+          // Since the map values are themselves heap objects, we need to check that they too are unchanged
+          assert forall k <- cache.Keys() :: old(allocated(cache.Select(k))) && unchanged(cache.Select(k));
+          assert MutableMapIsInjective(old@CAN_REMOVE(cache));
+
+          assert MutableMapContains(old@CAN_REMOVE(cache), cache);
+          LemmaMutableMapContainsPreservesInjectivity(old@CAN_REMOVE(cache), cache);
+        }
+        assert |cache.Keys()| == |old@CAN_REMOVE(cache.Keys())| - 1;
         assert cache.Size() <= old@CAN_REMOVE(cache.Size()) <= entryCapacity;
         queue.remove(cell);
+        assert multiset(cache.Values()) == multiset(queue.Items) by {
+          var cacheMultiset := multiset(cache.Values());
+          var queueMultiset := multiset(queue.Items);
+          assert cacheMultiset[cell := 0] == queueMultiset[cell := 0];
+          assert cell !in cacheMultiset;
+          assert cell !in queueMultiset;
+        }
         Modifies := Modifies - {cell};
       }
+
       output := Success(());
     }
 
@@ -602,4 +621,26 @@ module {:options "/functionSyntax:4" } LocalCMC {
       return Success(());
     }
   }
+
+  // TODO move this into MutableMap
+  ghost predicate MutableMapIsInjective<K, V>(m: MutableMap<K, V>)
+    reads m
+  {
+    forall k <- m.Keys(), k' <- m.Keys() | k != k' :: m.Select(k) != m.Select(k')
+  }
+
+  // TODO move this into MutableMap
+  ghost predicate MutableMapContains<K, V>(big: MutableMap<K, V>, small: MutableMap<K, V>)
+    reads {big, small}
+  {
+    && small.Keys() <= big.Keys()
+    && forall k <- small.Keys() :: small.Select(k) == big.Select(k)
+  }
+
+  // TODO move this into MutableMap
+  lemma LemmaMutableMapContainsPreservesInjectivity<K, V>(big: MutableMap<K, V>, small: MutableMap<K, V>)
+    requires MutableMapContains(big, small)
+    requires MutableMapIsInjective(big)
+    ensures MutableMapIsInjective(small)
+  {}
 }
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy
index f4f8b5d25..dd8a6104c 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsHierarchicalKeyring.dfy
@@ -603,7 +603,7 @@ module AwsKmsHierarchicalKeyring {
     }
   }
 
-  method SortByTime(queryResponse: DDB.ItemList)
+  method {:vcs_split_on_every_assert} SortByTime(queryResponse: DDB.ItemList)
     returns (output: branchKeyItem)
     requires |queryResponse| > 0
     requires 
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy
index 3dc566bc3..f7f04e03c 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy
@@ -20,7 +20,7 @@ module MrkAwareStrictMultiKeyring {
   import AwsKmsMrkKeyring
   import opened AwsKmsUtils
 
-  method MrkAwareStrictMultiKeyring(
+  method {:vcs_split_on_every_assert} MrkAwareStrictMultiKeyring(
     generator: Option<string>,
     awsKmsKeys: Option<seq<string>>,
     clientSupplier: Types.IClientSupplier,
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy
index 90e63c89f..82d54b9f7 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy
@@ -20,7 +20,7 @@ module StrictMultiKeyring {
   import AwsKmsKeyring
   import opened AwsKmsUtils
 
-  method StrictMultiKeyring(
+  method {:vcs_split_on_every_assert} StrictMultiKeyring(
     generator: Option<string>,
     awsKmsKeys: Option<seq<string>>,
     clientSupplier: Types.IClientSupplier,
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy
index 8e3d28b5d..17a236a84 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy
@@ -186,6 +186,7 @@ module MultiKeyring {
       for i := 0 to |this.childKeyrings|
         invariant returnMaterials.plaintextDataKey.Some?
         invariant unchanged(History);
+        invariant i < |this.childKeyrings| ==> this.childKeyrings[i].Modifies <= Modifies
       {
         var onEncryptInput := Types.OnEncryptInput(materials := returnMaterials);
 
diff --git a/AwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts b/AwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts
index 02ae8aef2..747385be9 100644
--- a/AwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts
+++ b/AwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts
@@ -52,7 +52,7 @@ repositories {
 }
 
 dependencies {
-    implementation("dafny.lang:DafnyRuntime:3.10.0")
+    implementation("org.dafny:DafnyRuntime:4.0.0")
     implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
     implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
     implementation("software.amazon.cryptography:AwsCryptographyPrimitives:1.0-SNAPSHOT")
diff --git a/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj b/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj
index 4c6f97a81..89b0516a2 100644
--- a/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj
+++ b/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj
@@ -11,7 +11,7 @@
 
     <ItemGroup>
         <PackageReference Include="AWSSDK.Core" Version="3.7.103" />
-        <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+        <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
         <PackageReference Include="Portable.BouncyCastle" Version="1.8.5.2" />
         <!--
           System.Collections.Immutable can be removed once dafny.msbuild is updated with
diff --git a/AwsCryptographyPrimitives/Makefile b/AwsCryptographyPrimitives/Makefile
index c2f728d11..788534b6b 100644
--- a/AwsCryptographyPrimitives/Makefile
+++ b/AwsCryptographyPrimitives/Makefile
@@ -3,11 +3,10 @@
 
 CORES=2
 
-include ../SharedMakefile.mk
+include ../SharedMakefileV2.mk
 
 SMITHY_NAMESPACE=aws.cryptography.primitives
 MAX_RESOURCE_COUNT=10000000
-# Order is important
-# In java they MUST be built
-# in the order they depend on each other
-LIBRARIES := 
+
+STD_LIBRARY=StandardLibrary
+SMITHY_DEPS=model
diff --git a/AwsCryptographyPrimitives/runtimes/java/build.gradle.kts b/AwsCryptographyPrimitives/runtimes/java/build.gradle.kts
index 0737a2eb3..9bca86f77 100644
--- a/AwsCryptographyPrimitives/runtimes/java/build.gradle.kts
+++ b/AwsCryptographyPrimitives/runtimes/java/build.gradle.kts
@@ -52,7 +52,7 @@ repositories {
 }
 
 dependencies {
-    implementation("dafny.lang:DafnyRuntime:3.10.0")
+    implementation("org.dafny:DafnyRuntime:4.0.0")
     implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
     implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
     implementation("org.bouncycastle:bcprov-jdk18on:1.72")
diff --git a/AwsCryptographyPrimitives/runtimes/net/Crypto.csproj b/AwsCryptographyPrimitives/runtimes/net/Crypto.csproj
index 184ee9340..08b07205a 100644
--- a/AwsCryptographyPrimitives/runtimes/net/Crypto.csproj
+++ b/AwsCryptographyPrimitives/runtimes/net/Crypto.csproj
@@ -11,7 +11,7 @@
 
   <ItemGroup>
     <PackageReference Include="AWSSDK.Core" Version="3.7.12.2" />
-    <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+    <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
     <PackageReference Include="Portable.BouncyCastle" Version="1.8.5.2" />
     <!--
       System.Collections.Immutable can be removed once dafny.msbuild is updated with
diff --git a/ComAmazonawsDynamodb/Makefile b/ComAmazonawsDynamodb/Makefile
index 2e1ed1ffd..b6dd1afe3 100644
--- a/ComAmazonawsDynamodb/Makefile
+++ b/ComAmazonawsDynamodb/Makefile
@@ -3,12 +3,10 @@
 
 CORES=2
 
-include ../SharedMakefile.mk
+include ../SharedMakefileV2.mk
 
 SMITHY_NAMESPACE=com.amazonaws.dynamodb
 MAX_RESOURCE_COUNT=10000000
-# Order is important
-# In java they MUST be built
-# in the order they depend on each other
-LIBRARIES := 
-AWS_SDK_CMD := --aws-sdk
\ No newline at end of file
+AWS_SDK_CMD := --aws-sdk
+STD_LIBRARY=StandardLibrary
+SMITHY_DEPS=model
diff --git a/ComAmazonawsDynamodb/runtimes/java/build.gradle.kts b/ComAmazonawsDynamodb/runtimes/java/build.gradle.kts
index fa6bea3dd..63649d4a8 100644
--- a/ComAmazonawsDynamodb/runtimes/java/build.gradle.kts
+++ b/ComAmazonawsDynamodb/runtimes/java/build.gradle.kts
@@ -52,7 +52,7 @@ repositories {
 }
 
 dependencies {
-    implementation("dafny.lang:DafnyRuntime:3.10.0")
+    implementation("org.dafny:DafnyRuntime:4.0.0")
     implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
     implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
     implementation(platform("software.amazon.awssdk:bom:2.19.1"))
diff --git a/ComAmazonawsDynamodb/runtimes/net/ComAmazonawsDynamodb.csproj b/ComAmazonawsDynamodb/runtimes/net/ComAmazonawsDynamodb.csproj
index f506ff537..0497d8c25 100644
--- a/ComAmazonawsDynamodb/runtimes/net/ComAmazonawsDynamodb.csproj
+++ b/ComAmazonawsDynamodb/runtimes/net/ComAmazonawsDynamodb.csproj
@@ -10,7 +10,7 @@
   </PropertyGroup>
 
   <ItemGroup>
-    <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+    <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
     <PackageReference Include="AWSSDK.Core" Version="3.7.103" />
     <PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.101.8" />
     <!--
diff --git a/ComAmazonawsKms/Makefile b/ComAmazonawsKms/Makefile
index 49757042f..552ba737a 100644
--- a/ComAmazonawsKms/Makefile
+++ b/ComAmazonawsKms/Makefile
@@ -3,12 +3,10 @@
 
 CORES=2
 
-include ../SharedMakefile.mk
+include ../SharedMakefileV2.mk
 
 SMITHY_NAMESPACE=com.amazonaws.kms
 MAX_RESOURCE_COUNT=10000000
-# Order is important
-# In java they MUST be built
-# in the order they depend on each other
-LIBRARIES := 
-AWS_SDK_CMD := --aws-sdk
\ No newline at end of file
+AWS_SDK_CMD := --aws-sdk
+STD_LIBRARY=StandardLibrary
+SMITHY_DEPS=model
diff --git a/ComAmazonawsKms/runtimes/java/build.gradle.kts b/ComAmazonawsKms/runtimes/java/build.gradle.kts
index b4fa11db9..51d47d4c1 100644
--- a/ComAmazonawsKms/runtimes/java/build.gradle.kts
+++ b/ComAmazonawsKms/runtimes/java/build.gradle.kts
@@ -52,7 +52,7 @@ repositories {
 }
 
 dependencies {
-    implementation("dafny.lang:DafnyRuntime:3.10.0")
+    implementation("org.dafny:DafnyRuntime:4.0.0")
     implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
     implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
     implementation(platform("software.amazon.awssdk:bom:2.19.1"))
diff --git a/ComAmazonawsKms/runtimes/net/AWS-KMS.csproj b/ComAmazonawsKms/runtimes/net/AWS-KMS.csproj
index 41df2cb26..388ee00b3 100644
--- a/ComAmazonawsKms/runtimes/net/AWS-KMS.csproj
+++ b/ComAmazonawsKms/runtimes/net/AWS-KMS.csproj
@@ -10,7 +10,7 @@
   </PropertyGroup>
 
   <ItemGroup>
-    <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+    <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
     <PackageReference Include="AWSSDK.Core" Version="3.7.11.12" />
     <PackageReference Include="AWSSDK.KeyManagementService" Version="3.7.3.20" />
     <!--
diff --git a/Makefile b/Makefile
index 7e65a8c37..0bc2151d6 100644
--- a/Makefile
+++ b/Makefile
@@ -1,9 +1,20 @@
 
 
 verify:
-	CORES=4 $(MAKE) -C AwsCryptographyPrimitives verify
-	CORES=4 $(MAKE) -C ComAmazonawsKms verify
-	CORES=4 $(MAKE) -C AwsCryptographicMaterialProviders verify
+	$(MAKE) -C StandardLibrary verify CORES=4
+	$(MAKE) -C AwsCryptographyPrimitives verify CORES=4
+	$(MAKE) -C ComAmazonawsKms verify CORES=4
+	$(MAKE) -C ComAmazonawsDynamodb verify CORES=4
+	$(MAKE) -C AwsCryptographicMaterialProviders verify CORES=4
+	$(MAKE) -C AwsEncryptionSDK verify CORES=4
+
+dafny-reportgenerator:
+	$(MAKE) -C StandardLibrary dafny-reportgenerator
+	$(MAKE) -C AwsCryptographyPrimitives dafny-reportgenerator
+	$(MAKE) -C ComAmazonawsKms dafny-reportgenerator
+	$(MAKE) -C ComAmazonawsDynamodb dafny-reportgenerator
+	$(MAKE) -C AwsCryptographicMaterialProviders dafny-reportgenerator
+	$(MAKE) -C AwsEncryptionSDK dafny-reportgenerator
 
 duvet: | duvet_extract duvet_report
 
diff --git a/SharedMakefileV2.mk b/SharedMakefileV2.mk
index 534fa4a2f..5e8f0f056 100644
--- a/SharedMakefileV2.mk
+++ b/SharedMakefileV2.mk
@@ -53,22 +53,30 @@ verify:
 		-vcsCores:$(CORES) \
 		-compile:0 \
 		-definiteAssignment:3 \
+		-quantifierSyntax:3 \
+		-unicodeChar:0 \
+		-functionSyntax:3 \
 		-verificationLogger:csv \
-		-timeLimit:300 \
+		-timeLimit:100 \
 		-trace \
 		`find . -name *.dfy`
 
 # Verify single file FILE with text logger.
 # This is useful for debugging resource count usage within a file.
+# Use PROC to further scope the verification
 verify_single:
 	@: $(if ${CORES},,CORES=2);
 	dafny \
 		-vcsCores:$(CORES) \
 		-compile:0 \
 		-definiteAssignment:3 \
+		-quantifierSyntax:3 \
+		-unicodeChar:0 \
+		-functionSyntax:3 \
 		-verificationLogger:text \
-		-timeLimit:300 \
+		-timeLimit:100 \
 		-trace \
+		$(if ${PROC},-proc:*$(PROC)*,) \
 		$(FILE)
 
 #Verify only a specific namespace at env var $(SERVICE)
@@ -78,11 +86,29 @@ verify_service:
 		-vcsCores:$(CORES) \
 		-compile:0 \
 		-definiteAssignment:3 \
+		-quantifierSyntax:3 \
+		-unicodeChar:0 \
+		-functionSyntax:3 \
 		-verificationLogger:csv \
-		-timeLimit:300 \
+		-timeLimit:100 \
 		-trace \
 		`find ./dafny/$(SERVICE) -name '*.dfy'` \
 
+format:
+	dafny format \
+		--function-syntax 3 \
+		--quantifier-syntax 3 \
+		--unicode-char false \
+		`find . -name '*.dfy'`
+
+format-check:
+	dafny format \
+		--check \
+		--function-syntax 3 \
+		--quantifier-syntax 3 \
+		--unicode-char false \
+		`find . -name '*.dfy'`
+
 dafny-reportgenerator:
 	dafny-reportgenerator \
 		summarize-csv-results \
@@ -92,8 +118,8 @@ dafny-reportgenerator:
 # Dafny helper targets
 
 # Transpile the entire project's impl
-_transpile_implementation_all: TRANSPILE_TARGETS=$(patsubst %, ./dafny/%/src/Index.dfy, $(PROJECT_SERVICES))
-_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
+_transpile_implementation_all: TRANSPILE_TARGETS=$(if ${PROJECT_SERVICES}, $(patsubst %, ./dafny/%/src/Index.dfy, $(PROJECT_SERVICES)), src/Index.dfy)
+_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(if ${PROJECT_INDEX}, $(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX)), )
 _transpile_implementation_all: transpile_implementation
 
 # The `$(OUT)` and $(TARGET) variables are problematic.
@@ -117,15 +143,18 @@ transpile_implementation:
 		-spillTargetCode:3 \
 		-compile:0 \
 		-optimizeErasableDatatypeWrapper:0 \
+		-quantifierSyntax:3 \
+		-unicodeChar:0 \
+		-functionSyntax:3 \
 		-useRuntimeLib \
 		-out $(OUT) \
 		$(TRANSPILE_TARGETS) \
-		-library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
 		$(TRANSPILE_DEPENDENCIES)
 
 # Transpile the entire project's tests
-_transpile_test_all: TRANSPILE_TARGETS=$(patsubst %, `find ./dafny/%/test -name '*.dfy'`, $(PROJECT_SERVICES))
-_transpile_test_all: TRANSPILE_DEPENDENCIES=$(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
+_transpile_test_all: TRANSPILE_TARGETS=$(if ${PROJECT_SERVICES}, $(patsubst %, `find ./dafny/%/test -name '*.dfy'`, $(PROJECT_SERVICES)), `find ./test -name '*.dfy'`)
+_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${PROJECT_SERVICES}, $(patsubst %, -library:dafny/%/src/Index.dfy, $(PROJECT_SERVICES)), -library:src/Index.dfy)
 _transpile_test_all: transpile_test
 
 transpile_test:
@@ -136,15 +165,20 @@ transpile_test:
 		-runAllTests:1 \
 		-compile:0 \
 		-optimizeErasableDatatypeWrapper:0 \
+		-quantifierSyntax:3 \
+		-unicodeChar:0 \
+		-functionSyntax:3 \
 		-useRuntimeLib \
 		-out $(OUT) \
 		$(TRANSPILE_TARGETS) \
-		-library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy \
+		$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
 		$(TRANSPILE_DEPENDENCIES)
 
 
+# If we are not the StandardLibrary, transpile the StandardLibrary.
+# Transpile all other dependencies
 transpile_dependencies:
-	$(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_implementation_$(LANG)
+	$(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) transpile_implementation_$(LANG), )
 	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% transpile_implementation_$(LANG);, $(PROJECT_DEPENDENCIES))
 
 ########################## Code-Gen targets
@@ -159,73 +193,67 @@ transpile_dependencies:
 # a single target can decide what parts it wants to build.
 
 _polymorph:
+	$(if $(PROJECT_SERVICES), $(MAKE) _polymorph_v2, $(MAKE) _polymorph_v1)
+
+_polymorph_v1:
 	@: $(if ${CODEGEN_CLI_ROOT},,$(error You must pass the path CODEGEN_CLI_ROOT: CODEGEN_CLI_ROOT=/[path]/[to]/smithy-dafny/codegen/smithy-dafny-codegen-cli));
 	cd $(CODEGEN_CLI_ROOT); \
 	./../gradlew run --args="\
 	$(OUTPUT_DAFNY) \
 	$(OUTPUT_DOTNET) \
 	$(OUTPUT_JAVA) \
-	--model $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model \
-	--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
-	$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
-	--namespace $($(namespace_var)) \
+	--model $(SMITHY_MODEL_ROOT) \
+	--dependent-model $(PROJECT_ROOT)/model \
+	$(patsubst %, --dependent-model $(PROJECT_ROOT)/%, $(LIBRARY_MODEL)) \
+	--namespace $(SMITHY_NAMESPACE) \
 	$(AWS_SDK_CMD) \
 	$(OUTPUT_LOCAL_SERVICE) \
 	";
 
-# Generates all target runtime code for all namespaces in this project.
-.PHONY: polymorph_code_gen
-polymorph_code_gen:
+_polymorph_v2:
 	for service in $(PROJECT_SERVICES) ; do \
 		export service_deps_var=SERVICE_DEPS_$${service} ; \
 		export namespace_var=SERVICE_NAMESPACE_$${service} ; \
 		export SERVICE=$${service} ; \
-		$(MAKE) _polymorph_code_gen || exit 1; \
+		$(MAKE) _polymorph_v2_per_service || exit 1; \
 	done
 
-_polymorph_code_gen: OUTPUT_DAFNY=--output-dafny $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
-_polymorph_code_gen: OUTPUT_DOTNET=--output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/
-_polymorph_code_gen: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
-_polymorph_code_gen: _polymorph
+_polymorph_v2_per_service:
+	@: $(if ${CODEGEN_CLI_ROOT},,$(error You must pass the path CODEGEN_CLI_ROOT: CODEGEN_CLI_ROOT=/[path]/[to]/smithy-dafny/codegen/smithy-dafny-codegen-cli));
+	cd $(CODEGEN_CLI_ROOT); \
+	./../gradlew run --args="\
+	$(OUTPUT_DAFNY) \
+	$(OUTPUT_DOTNET) \
+	$(OUTPUT_JAVA) \
+	--model $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model \
+	--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
+	$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
+	--namespace $($(namespace_var)) \
+	$(AWS_SDK_CMD) \
+	$(OUTPUT_LOCAL_SERVICE) \
+	";
+
+# Generates all target runtime code for all namespaces in this project.
+.PHONY: polymorph_code_gen
+polymorph_code_gen: OUTPUT_DAFNY=--output-dafny $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+polymorph_code_gen: OUTPUT_DOTNET=--output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/
+polymorph_code_gen: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
+polymorph_code_gen: _polymorph_code_gen
 
 # Generates dafny code for all namespaces in this project
 .PHONY: polymorph_dafny
-polymorph_dafny:
-	for service in $(PROJECT_SERVICES) ; do \
-		export service_deps_var=SERVICE_DEPS_$${service} ; \
-		export namespace_var=SERVICE_NAMESPACE_$${service} ; \
-		export SERVICE=$${service} ; \
-		$(MAKE) _polymorph_dafny || exit 1; \
-	done
-
-_polymorph_dafny: OUTPUT_DAFNY=--output-dafny $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
-_polymorph_dafny: _polymorph
+polymorph_dafny: OUTPUT_DAFNY=--output-dafny $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model --include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
+polymorph_dafny: _polymorph
 
 # Generates dotnet code for all namespaces in this project
 .PHONY: polymorph_dotnet
-polymorph_dotnet:
-	for service in $(PROJECT_SERVICES) ; do \
-		export service_deps_var=SERVICE_DEPS_$${service} ; \
-		export namespace_var=SERVICE_NAMESPACE_$${service} ; \
-		export SERVICE=$${service} ; \
-		$(MAKE) _polymorph_dotnet || exit 1; \
-	done
-
-_polymorph_dotnet: OUTPUT_DOTNET=--output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SMITHY_NAMESPACE)/
-_polymorph_dotnet: _polymorph
+polymorph_dotnet: OUTPUT_DOTNET=--output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SMITHY_NAMESPACE)/
+polymorph_dotnet: _polymorph
 
 # Generates java code for all namespaces in this project
 .PHONY: polymorph_java
-polymorph_java:
-	for service in $(PROJECT_SERVICES) ; do \
-		export service_deps_var=SERVICE_DEPS_$${service} ; \
-		export namespace_var=SERVICE_NAMESPACE_$${service} ; \
-		export SERVICE=$${service} ; \
-		$(MAKE) _polymorph_java || exit 1; \
-	done
-
-_polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
-_polymorph_java: _polymorph
+polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
+polymorph_java: _polymorph
 
 ########################## .NET targets
 
@@ -289,8 +317,10 @@ _mv_test_java:
 transpile_dependencies_java: LANG=java
 transpile_dependencies_java: transpile_dependencies
 
+# If we are not StandardLibrary, locally deploy the StandardLibrary.
+# Locally deploy all other dependencies 
 mvn_local_deploy_dependencies:
-	$(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) mvn_local_deploy
+	$(if $(strip $(STD_LIBRARY)), $(MAKE) -C $(PROJECT_ROOT)/$(STD_LIBRARY) mvn_local_deploy, )
 	$(patsubst %, $(MAKE) -C $(PROJECT_ROOT)/% mvn_local_deploy;, $(PROJECT_DEPENDENCIES))
 
 # The Java MUST all exist already through the transpile step.
diff --git a/StandardLibrary/Makefile b/StandardLibrary/Makefile
index cdf5d75d0..a04d4dcf7 100644
--- a/StandardLibrary/Makefile
+++ b/StandardLibrary/Makefile
@@ -3,7 +3,16 @@
 
 CORES=2
 
-include ../SharedMakefile.mk
+include ../SharedMakefileV2.mk
 
 MAX_RESOURCE_COUNT=500000000
 LIBRARIES := 
+
+# Since everything depends on the StandardLibrary
+# it is included as a library in the SharedMakefile.
+# However, this means this it could not build...
+# So we empty the variable here
+# and check in the Makefile
+transpile_implementation: STD_LIBRARY=
+transpile_test: STD_LIBRARY=
+transpile_dependencies: STD_LIBRARY=
diff --git a/StandardLibrary/runtimes/java/build.gradle.kts b/StandardLibrary/runtimes/java/build.gradle.kts
index 990c317e1..36c9f39ec 100644
--- a/StandardLibrary/runtimes/java/build.gradle.kts
+++ b/StandardLibrary/runtimes/java/build.gradle.kts
@@ -51,7 +51,7 @@ repositories {
 }
 
 dependencies {
-    implementation("dafny.lang:DafnyRuntime:3.10.0")
+    implementation("org.dafny:DafnyRuntime:4.0.0")
     implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
 }
 publishing {
diff --git a/StandardLibrary/runtimes/net/STD.csproj b/StandardLibrary/runtimes/net/STD.csproj
index ce69c8abc..822812ac0 100644
--- a/StandardLibrary/runtimes/net/STD.csproj
+++ b/StandardLibrary/runtimes/net/STD.csproj
@@ -10,7 +10,7 @@
   </PropertyGroup>
 
   <ItemGroup>
-    <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+    <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
     <!--
       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/StandardLibrary/src/Base64.dfy b/StandardLibrary/src/Base64.dfy
index b1947013c..7010d0b9d 100644
--- a/StandardLibrary/src/Base64.dfy
+++ b/StandardLibrary/src/Base64.dfy
@@ -111,7 +111,7 @@ module Base64 {
     [b0, b1, b2, b3]
   }
 
-  function method IndexSeqToUInt24(s: seq<index>): (x: uint24)
+  function method {:vcs_split_on_every_assert} IndexSeqToUInt24(s: seq<index>): (x: uint24)
     requires |s| == 4
     ensures UInt24ToIndexSeq(x) == s
   {
diff --git a/StandardLibrary/src/Base64Lemmas.dfy b/StandardLibrary/src/Base64Lemmas.dfy
index af0342178..3aaa7384f 100644
--- a/StandardLibrary/src/Base64Lemmas.dfy
+++ b/StandardLibrary/src/Base64Lemmas.dfy
@@ -48,7 +48,7 @@ module Base64Lemmas {
     ensures DecodeValid(s)[(|DecodeValid(s)| - 2)..] == Decode1Padding(s[(|s| - 4)..])
   {}
 
-  lemma DecodeValidEncode1Padding(s: seq<char>)
+  lemma {:vcs_split_on_every_assert} DecodeValidEncode1Padding(s: seq<char>)
     requires IsBase64String(s)
     requires |s| >= 4
     requires Is1Padding(s[(|s| - 4)..])
@@ -60,6 +60,7 @@ module Base64Lemmas {
       assert |DecodeValid(s)| % 3 == 2;
       EncodeUnpadded(DecodeValid(s)[..(|DecodeValid(s)| - 2)]) + Encode1Padding(DecodeValid(s)[(|DecodeValid(s)| - 2)..]);
     == { DecodeValidUnpaddedPartialFrom1PaddedSeq(s); }
+      assert IsUnpaddedBase64String(s[..(|s| - 4)]);
       EncodeUnpadded(DecodeUnpadded(s[..(|s| - 4)])) + Encode1Padding(DecodeValid(s)[(|DecodeValid(s)| - 2)..]);
     == { DecodeEncodeUnpadded(s[..(|s| - 4)]); }
       s[..(|s| - 4)] + Encode1Padding(DecodeValid(s)[(|DecodeValid(s)| - 2)..]);
@@ -86,7 +87,7 @@ module Base64Lemmas {
     ensures DecodeValid(s)[(|DecodeValid(s)| - 1)..] == Decode2Padding(s[(|s| - 4)..])
   {}
 
-  lemma DecodeValidEncode2Padding(s: seq<char>)
+  lemma {:vcs_split_on_every_assert} DecodeValidEncode2Padding(s: seq<char>)
     requires IsBase64String(s)
     requires |s| >= 4
     requires Is2Padding(s[(|s| - 4)..])
@@ -95,6 +96,7 @@ module Base64Lemmas {
     calc {
       Encode(DecodeValid(s));
     ==
+      assert |DecodeUnpadded(s[..|s|-4])| % 3 == 0;
       assert |DecodeValid(s)| % 3 == 1;
       EncodeUnpadded(DecodeValid(s)[..(|DecodeValid(s)| - 1)]) + Encode2Padding(DecodeValid(s)[(|DecodeValid(s)| - 1)..]);
     == { DecodeValidUnpaddedPartialFrom2PaddedSeq(s); }
diff --git a/StandardLibrary/src/Sorting.dfy b/StandardLibrary/src/Sorting.dfy
index 10a2fc1d6..d3d4957ad 100644
--- a/StandardLibrary/src/Sorting.dfy
+++ b/StandardLibrary/src/Sorting.dfy
@@ -122,7 +122,7 @@ module Sorting {
    * Sorting routines
    */
 
-  method SelectionSort<Data>(a: array<Data>, below: (Data, Data) -> bool)
+  method {:vcs_split_on_every_assert} SelectionSort<Data>(a: array<Data>, below: (Data, Data) -> bool)
     requires StandardLibrary.Transitive(below)
     requires Connected(below)
     modifies a
diff --git a/StandardLibrary/test/UTF8.dfy b/StandardLibrary/test/UTF8.dfy
index 1e548f23c..5342881db 100644
--- a/StandardLibrary/test/UTF8.dfy
+++ b/StandardLibrary/test/UTF8.dfy
@@ -24,7 +24,9 @@ module TestUTF8 {
 
   method {:test} TestDecodeHappyCase() {
     var unicodeBytes := [0x61, 0x62, 0x63, 0xCC, 0x86, 0xC7, 0xBD, 0xCE, 0xB2];
-    assert UTF8.ValidUTF8Range(unicodeBytes, 3, 9);
+    assert UTF8.Uses2Bytes([0xC7, 0xBD, 0xCE, 0xB2]);
+    assert [0xC7, 0xBD, 0xCE, 0xB2] == unicodeBytes[5..9];
+    assert UTF8.ValidUTF8Range(unicodeBytes, 7, 9);
     assert UTF8.ValidUTF8Range(unicodeBytes, 0, 9);
     var expectedString := "abc\u0306\u01FD\u03B2";
     var decoded :- expect UTF8.Decode(unicodeBytes);
diff --git a/TestVectorsAwsCryptographicMaterialProviders/Makefile b/TestVectorsAwsCryptographicMaterialProviders/Makefile
index 5957c4fb7..c4a53654e 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/Makefile
+++ b/TestVectorsAwsCryptographicMaterialProviders/Makefile
@@ -3,7 +3,7 @@
 
 CORES=2
 
-include ../SharedMakefile.mk
+include ../SharedMakefileV2.mk
 
 SMITHY_MODEL_ROOT := $(PROJECT_ROOT)/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model
 OUTPUT_LOCAL_SERVICE := --local-service-test
@@ -13,7 +13,7 @@ MAX_RESOURCE_COUNT=10000000
 # Order is important
 # In java they MUST be built
 # in the order they depend on each other
-LIBRARIES := \
+PROJECT_DEPENDENCIES := \
 	AwsCryptographyPrimitives \
 	ComAmazonawsKms \
 	ComAmazonawsDynamodb \
@@ -23,17 +23,21 @@ LIBRARIES := \
 # about where the files are located. 
 # This is here to get unblocked but should be removed once we have migrated packages
 # to the new packaging format.
-LIBRARIES_INDEX := \
+PROJECT_INDEX := \
 	AwsCryptographyPrimitives/src/Index.dfy \
 	ComAmazonawsKms/src/Index.dfy \
 	ComAmazonawsDynamodb/src/Index.dfy \
 	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Index.dfy \
+	AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Index.dfy \
 
-LIBRARY_MODEL := \
-	AwsCryptographyPrimitives/Model \
-	ComAmazonawsKms/Model \
-	ComAmazonawsDynamodb/Model \
-	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model
+STD_LIBRARY=StandardLibrary
+SMITHY_DEPS=model
+
+# LIBRARY_MODEL := \
+# 	AwsCryptographyPrimitives/Model \
+# 	ComAmazonawsKms/Model \
+# 	ComAmazonawsDynamodb/Model \
+# 	AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model
 
 format_net:
 	pushd runtimes/net && dotnet format && popd
diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts
index f23c33dd1..d0072caee 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts
+++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/java/build.gradle.kts
@@ -56,7 +56,7 @@ repositories {
 }
 
 dependencies {
-    implementation("dafny.lang:DafnyRuntime:3.10.0")
+    implementation("org.dafny:DafnyRuntime:4.0.0")
     implementation("software.amazon.dafny:conversion:1.0-SNAPSHOT")
     implementation("software.amazon.cryptography:StandardLibrary:1.0-SNAPSHOT")
     implementation("software.amazon.cryptography:AwsCryptographyPrimitives:1.0-SNAPSHOT")
diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/TestVectors.csproj b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/TestVectors.csproj
index 9cad959ef..23d65acc3 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/TestVectors.csproj
+++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/net/TestVectors.csproj
@@ -11,7 +11,7 @@
     </PropertyGroup>
 
     <ItemGroup>
-        <PackageReference Include="DafnyRuntime" Version="3.10.0.41215" />
+        <PackageReference Include="DafnyRuntime" Version="4.0.0.50303" />
         <!--
           System.Collections.Immutable can be removed once dafny.msbuild is updated with
           https://github.com/dafny-lang/dafny.msbuild/pull/10 and versioned