diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/BranchKeyValidators.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/BranchKeyValidators.dfy
new file mode 100644
index 0000000000..886006a6d9
--- /dev/null
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/BranchKeyValidators.dfy
@@ -0,0 +1,256 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+
+include "../src/Index.dfy"
+
+// methods to validate a Get* Branch Key result from the Branch Key Store client
+module {:options "/functionSyntax:4" } BranchKeyValidators {
+  import opened Wrappers
+  import opened StandardLibrary.UInt
+  import UTF8
+  import UUID
+  import Types = AwsCryptographyKeyStoreTypes
+  import Structure
+
+  method VerifyGetKeys(
+    identifier : string,
+    keyStore : Types.IKeyStoreClient,
+    storage : Types.IKeyStorageInterface,
+    nameonly versionUtf8Bytes?: Option<seq<uint8>> := None,
+    nameonly encryptionContext : Types.EncryptionContext := map[],
+    nameonly hierarchyVersion : Types.HierarchyVersion := Types.HierarchyVersion.v1
+  )
+    requires
+      keyStore.ValidState() && storage.ValidState()
+    modifies
+      keyStore.Modifies, storage.Modifies
+    ensures
+      keyStore.ValidState() && storage.ValidState()
+
+  {
+    var _ := testBeaconKeyHappyCase(
+      keyStore := keyStore,
+      branchKeyId := identifier,
+      encryptionContext := encryptionContext
+    );
+
+    var activeResult := testActiveBranchKeyHappyCase(
+      keyStore := keyStore,
+      branchKeyId := identifier,
+      encryptionContext := encryptionContext
+    );
+    var versionString :- expect UTF8.Decode(activeResult.branchKeyVersion);
+
+    var _ := testBranchKeyVersionHappyCase(
+      keyStore := keyStore,
+      branchKeyId := identifier,
+      branchKeyIdActiveVersion := versionString,
+      branchKeyIdActiveVersionUtf8Bytes := activeResult.branchKeyVersion,
+      encryptionContext := encryptionContext
+    );
+    VerifyGetKeysFromStorage(identifier, storage, hierarchyVersion:=hierarchyVersion);
+
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
+    //= type=test
+    //# This guid MUST be [version 4 UUID](https://www.ietf.org/rfc/rfc4122.txt)
+    var versionByteUUID :- expect UUID.ToByteArray(versionString);
+    var versionRoundTrip :- expect UUID.FromByteArray(versionByteUUID);
+    expect versionRoundTrip == versionString;
+  }
+
+
+  method VerifyGetKeysFromStorage(
+    identifier : string,
+    storage : Types.IKeyStorageInterface,
+    nameonly hierarchyVersion : Types.HierarchyVersion := Types.HierarchyVersion.v1
+  )
+    requires storage.ValidState()
+    modifies storage.Modifies
+    ensures storage.ValidState()
+  {
+    var active :- expect storage.GetEncryptedActiveBranchKey(
+      Types.GetEncryptedActiveBranchKeyInput(
+        Identifier := identifier
+      )
+    );
+    expect active.Item.Type.ActiveHierarchicalSymmetricVersion?;
+
+    var beacon :- expect storage.GetEncryptedBeaconKey(
+      Types.GetEncryptedBeaconKeyInput(
+        Identifier := identifier
+      )
+    );
+    expect beacon.Item.Type.ActiveHierarchicalSymmetricBeacon?;
+
+    var version :- expect storage.GetEncryptedBranchKeyVersion(
+      Types.GetEncryptedBranchKeyVersionInput(
+        Identifier := identifier,
+        Version := active.Item.Type.ActiveHierarchicalSymmetricVersion.Version
+      )
+    );
+    expect version.Item.Type.HierarchicalSymmetricVersion?;
+
+    var hvMatches? := match hierarchyVersion {
+      case v1
+        =>
+        && branchKeyContextSaysHV1(active.Item.EncryptionContext)
+        && branchKeyContextSaysHV1(beacon.Item.EncryptionContext)
+        && branchKeyContextSaysHV1(version.Item.EncryptionContext)
+      case v2
+        =>
+        && branchKeyContextSaysHV2(active.Item.EncryptionContext)
+        && branchKeyContextSaysHV2(beacon.Item.EncryptionContext)
+        && branchKeyContextSaysHV2(version.Item.EncryptionContext)
+    };
+    if (!hvMatches?) {
+      print "HV did not match expectation, did bkc have hv?: ", Structure.HIERARCHY_VERSION in active.Item.EncryptionContext;
+      if (Structure.HIERARCHY_VERSION in active.Item.EncryptionContext) {
+        print " Actual HV: ", active.Item.EncryptionContext[Structure.HIERARCHY_VERSION];
+      }
+    }
+    expect hvMatches?, "Hierarchy Version did not match expectation.";
+
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
+    //= type=test
+    //# This timestamp MUST be in ISO 8601 format in UTC, to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“)
+    expect ISO8601?(active.Item.CreateTime);
+    expect ISO8601?(beacon.Item.CreateTime);
+    expect ISO8601?(version.Item.CreateTime);
+  }
+
+  predicate branchKeyContextSaysHV1(bkc: Types.EncryptionContextString)
+  {
+    Structure.HIERARCHY_VERSION in bkc && bkc[Structure.HIERARCHY_VERSION] == Structure.HIERARCHY_VERSION_VALUE_1
+  }
+
+  predicate branchKeyContextSaysHV2(bkc: Types.EncryptionContextString)
+  {
+    Structure.HIERARCHY_VERSION in bkc && bkc[Structure.HIERARCHY_VERSION] == Structure.HIERARCHY_VERSION_VALUE_2
+  }
+
+  method testActiveBranchKeyHappyCase(
+    keyStore: Types.IKeyStoreClient,
+    branchKeyId: string,
+    nameonly versionUtf8Bytes?: Option<seq<uint8>> := None,
+    nameonly encryptionContext : Types.EncryptionContext := map[]
+  ) returns (output: Types.BranchKeyMaterials)
+    requires keyStore.ValidState()
+    modifies keyStore.Modifies
+    ensures keyStore.ValidState()
+  {
+    var activeResult :- expect keyStore.GetActiveBranchKey(
+      Types.GetActiveBranchKeyInput(
+        branchKeyIdentifier := branchKeyId
+      ));
+    expect isValidActiveBranchKeyResult?(activeResult, branchKeyId, encryptionContext, versionUtf8Bytes?);
+    return activeResult.branchKeyMaterials;
+  }
+
+  method testBranchKeyVersionHappyCase(
+    keyStore: Types.IKeyStoreClient,
+    branchKeyId: string,
+    branchKeyIdActiveVersion: string,
+    branchKeyIdActiveVersionUtf8Bytes: seq<uint8>,
+    nameonly encryptionContext : Types.EncryptionContext := map[]
+  ) returns (output: Types.BranchKeyMaterials)
+    requires keyStore.ValidState()
+    modifies keyStore.Modifies
+    ensures keyStore.ValidState()
+  {
+    var versionResult :- expect keyStore.GetBranchKeyVersion(
+      Types.GetBranchKeyVersionInput(
+        branchKeyIdentifier := branchKeyId,
+        branchKeyVersion := branchKeyIdActiveVersion
+      ));
+    expect isValidBranchKeyVersionResult?(versionResult, branchKeyId, encryptionContext, branchKeyIdActiveVersionUtf8Bytes);
+    return versionResult.branchKeyMaterials;
+  }
+
+  method testBeaconKeyHappyCase(
+    keyStore: Types.IKeyStoreClient,
+    branchKeyId: string,
+    nameonly encryptionContext : Types.EncryptionContext := map[]
+  ) returns (output: Types.BeaconKeyMaterials)
+    requires keyStore.ValidState()
+    modifies keyStore.Modifies
+    ensures keyStore.ValidState()
+  {
+    var beaconKeyResult :- expect keyStore.GetBeaconKey(
+      Types.GetBeaconKeyInput(
+        branchKeyIdentifier := branchKeyId
+      ));
+    expect beaconKeyResult.beaconKeyMaterials.beaconKeyIdentifier == branchKeyId, "Wrong Branch Key ID.";
+    expect beaconKeyResult.beaconKeyMaterials.beaconKey.Some?, "Beacon Key Materials MUST be present.";
+    expect |beaconKeyResult.beaconKeyMaterials.beaconKey.value| == 32, "Lenght of Beacon Key Materials MUST be 32 bytes.";
+    if (beaconKeyResult.beaconKeyMaterials.encryptionContext != encryptionContext) {
+      print "Beacon Key's encryption context is incorrect. Expected: ", encryptionContext, " but got: ", beaconKeyResult.beaconKeyMaterials.encryptionContext;
+      expect false, "Beacon Key's encryption context is incorrect.";
+    }
+    expect isValidBeaconResult?(beaconKeyResult, branchKeyId, encryptionContext);
+    return beaconKeyResult.beaconKeyMaterials;
+  }
+
+  predicate isValidBeaconResult?(
+    beaconKeyResult: Types.GetBeaconKeyOutput,
+    branchKeyId: string,
+    encryptionContext : Types.EncryptionContext
+  ) {
+    && beaconKeyResult.beaconKeyMaterials.beaconKeyIdentifier == branchKeyId
+    && beaconKeyResult.beaconKeyMaterials.beaconKey.Some?
+    && |beaconKeyResult.beaconKeyMaterials.beaconKey.value| == 32
+    && beaconKeyResult.beaconKeyMaterials.encryptionContext == encryptionContext
+  }
+
+  predicate isValidActiveBranchKeyResult?(
+    branchKeyResult: Types.GetActiveBranchKeyOutput,
+    branchKeyId: string,
+    encryptionContext : Types.EncryptionContext,
+    branchKeyIdActiveVersionUtf8Bytes: Option<seq<uint8>>
+  )
+  {
+    && branchKeyResult.branchKeyMaterials.branchKeyIdentifier == branchKeyId
+    && (branchKeyIdActiveVersionUtf8Bytes.None? ||
+        branchKeyResult.branchKeyMaterials.branchKeyVersion == branchKeyIdActiveVersionUtf8Bytes.value)
+    && |branchKeyResult.branchKeyMaterials.branchKey| == 32
+    && branchKeyResult.branchKeyMaterials.encryptionContext == encryptionContext
+  }
+
+  predicate isValidBranchKeyVersionResult?(
+    versionResult: Types.GetBranchKeyVersionOutput,
+    branchKeyId: string,
+    encryptionContext : Types.EncryptionContext,
+    branchKeyIdActiveVersionUtf8Bytes: seq<uint8>
+  )
+  {
+    && versionResult.branchKeyMaterials.branchKeyIdentifier == branchKeyId
+    && versionResult.branchKeyMaterials.branchKeyVersion == branchKeyIdActiveVersionUtf8Bytes
+    && |versionResult.branchKeyMaterials.branchKey| == 32
+    && versionResult.branchKeyMaterials.encryptionContext == encryptionContext
+  }
+
+  //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
+  //= type=test
+  //# This timestamp MUST be in ISO 8601 format in UTC, to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“)
+  lemma ISO8601Test()
+  {
+    assert ISO8601?("2024-08-06T17:23:25.000874Z");
+  }
+
+  //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
+  //= type=test
+  //# This timestamp MUST be in ISO 8601 format in UTC, to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“)
+  predicate ISO8601?(
+    CreateTime: string
+  )
+  {
+    // “YYYY-MM-DDTHH:mm:ss.ssssssZ“
+    && |CreateTime| == 27
+    && CreateTime[4] == '-'
+    && CreateTime[7] == '-'
+    && CreateTime[10] == 'T'
+    && CreateTime[13] == ':'
+    && CreateTime[16] == ':'
+    && CreateTime[19] == '.'
+    && CreateTime[26] == 'Z'
+  }
+}
\ No newline at end of file
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy
index 08b8a5b5ec..04300a7131 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/Fixtures.dfy
@@ -61,6 +61,7 @@ module Fixtures {
 
   const branchKeyStoreName := "KeyStoreDdbTable"
   const logicalKeyStoreName := branchKeyStoreName
+  // hierarchy-version-1 branch key
   const branchKeyId := "3f43a9af-08c5-4317-b694-3d3e883dcaef"
   const branchKeyIdActiveVersion := "a4905627-4b7f-4272-a847-f50dae245737"
   // This is branchKeyIdActiveVersion above, as utf8bytes
@@ -71,14 +72,16 @@ module Fixtures {
     56, 52, 55, 45, 102, 53, 48, 100, 97, 101,
     50, 52, 53, 55, 51, 55
   ]
-
   const branchKeyIdWithEC := "4bb57643-07c1-419e-92ad-0df0df149d7c"
-  const hv2BranchKeyId := "test-hv2-branch-key-badaa332-29f2-4c72-8ad7-071eb48499c3"
-  const hv2BranchKeyVersion := "347fdc7d-e93f-4166-97c2-5f5e0053d335"
+  // hierarchy-version-2 branch key
+  const hv2BranchKeyId := "4a0c7b92-3703-4209-8961-24b07ab6562b"
+  const hv2BranchKeyVersion := "a0496b5c-e048-42bc-8b75-68a004851803"
+  // This is hv2BranchKeyVersion above, as utf8bytes
+  // https://cyberchef.infosec.amazon.dev/#recipe=Encode_text('UTF-8%20(65001)')To_Decimal('Comma',false)&input=YTA0OTZiNWMtZTA0OC00MmJjLThiNzUtNjhhMDA0ODUxODAz&oenc=65001
   const hv2BranchKeyIdActiveVersionUtf8Bytes: seq<uint8> := [
-    51, 52, 55, 102, 100, 99, 55, 100, 45, 101, 57,
-    51, 102, 45, 52, 49, 54, 54, 45, 57, 55, 99, 50,
-    45, 53, 102, 53, 101, 48, 48, 53, 51, 100, 51, 51, 53
+    97, 48, 52, 57, 54, 98, 53, 99, 45, 101, 48, 52,
+    56, 45, 52, 50, 98, 99, 45, 56, 98, 55, 53, 45,
+    54, 56, 97, 48, 48, 52, 56, 53, 49, 56, 48, 51
   ]
   // THESE ARE TESTING RESOURCES DO NOT USE IN A PRODUCTION ENVIRONMENT
   const keyArn := "arn:aws:kms:us-west-2:370957321024:key/9d989aa2-2f9c-438c-a745-cc57d3ad0126"
@@ -99,6 +102,7 @@ module Fixtures {
   const KmsSrkConfigWest : Types.KMSConfiguration := Types.KMSConfiguration.kmsKeyArn(MrkArnWest)
   const KmsMrkConfigAP : Types.KMSConfiguration := Types.KMSConfiguration.kmsMRKeyArn(MrkArnAP)
   const KmsMrkEC : Types.EncryptionContext := map[UTF8.EncodeAscii("abc") := UTF8.EncodeAscii("123")]
+  const RobbieEC : Types.EncryptionContext := map[UTF8.EncodeAscii("Robbie") := UTF8.EncodeAscii("is a dog.")]
   const EastBranchKey : string := "MyEastBranch2"
   const EastBranchKeyIdActiveVersion : string := "6f22825b-bd56-4434-83e2-2782e2160172"
   const EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes: seq<uint8> := [
@@ -255,19 +259,14 @@ module Fixtures {
     return Success(keyStore);
   }
 
-  method KeyStoreWithOptionalClient(
-    nameonly kmsId: string := keyArn,
+  method KeyStoreFromKMSConfig(
+    nameonly kmsConfig: Types.KMSConfiguration,
     nameonly physicalName: string := branchKeyStoreName,
     nameonly logicalName: string := logicalKeyStoreName,
-    nameonly ddbClient?: Option<DDB.Types.IDynamoDBClient> := None,
-    nameonly kmsClient?: Option<KMS.Types.IKMSClient> := None,
-    nameonly srkKey: bool := true,
-    nameonly mrkKey: bool := false
+    nameonly ddbClient?: Option<DDB.Types.IDynamoDBClient> := None
   )
     returns (output: Result<Types.IKeyStoreClient, Types.Error>)
     requires DDB.Types.IsValid_TableName(physicalName)
-    requires KMS.Types.IsValid_KeyIdType(kmsId)
-    requires srkKey != mrkKey
     ensures output.Success? ==> output.value.ValidState()
     ensures output.Success?
             ==>
@@ -278,16 +277,6 @@ module Fixtures {
     if ddbClient?.Some? {
       assume {:axiom} fresh(ddbClient?.value) && fresh(ddbClient?.value.Modifies);
     }
-    if kmsClient?.Some? {
-      assume {:axiom} fresh(kmsClient?.value) && fresh(kmsClient?.value.Modifies);
-    }
-    expect srkKey != mrkKey;
-    var kmsConfig := if srkKey then
-      createSrkKMSConfig(kmsId)
-    else
-      createMrkKMSConfig(kmsId);
-    expect srkKey ==> kmsConfig.kmsKeyArn?;
-    expect mrkKey ==> kmsConfig.kmsMRKeyArn?;
     var keyStoreConfig := Types.KeyStoreConfig(
       id := None,
       kmsConfiguration := kmsConfig,
@@ -297,31 +286,12 @@ module Fixtures {
           Types.DynamoDBTable(
             ddbTableName := physicalName,
             ddbClient := ddbClient?
-          ))),
-      keyManagement := Some(
-        Types.kms(
-          Types.AwsKms(
-            kmsClient := kmsClient?
           )))
     );
     var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
     return Success(keyStore);
   }
 
-  function method createSrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration)
-    requires KMS.Types.IsValid_KeyIdType(kmsId)
-    ensures output.kmsKeyArn?
-  {
-    Types.KMSConfiguration.kmsKeyArn(kmsId)
-  }
-
-  function method createMrkKMSConfig(kmsId: string) : (output: Types.KMSConfiguration)
-    requires KMS.Types.IsValid_KeyIdType(kmsId)
-    ensures output.kmsMRKeyArn?
-  {
-    Types.KMSConfiguration.kmsMRKeyArn(kmsId)
-  }
-
   datatype allThree = | allThree (
     active: Types.EncryptedHierarchicalKey,
     beacon: Types.EncryptedHierarchicalKey,
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestConfig.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestConfig.dfy
index 5f96008f85..bd70caddfd 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestConfig.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestConfig.dfy
@@ -3,7 +3,10 @@
 
 include "../src/Index.dfy"
 include "Fixtures.dfy"
+include "BranchKeyValidators.dfy"
 
+// This really tests the logic in BKS/Index.dfy
+// and KmsArn.dfy
 module TestConfig {
   import Types = AwsCryptographyKeyStoreTypes
   import ComAmazonawsKmsTypes
@@ -14,6 +17,7 @@ module TestConfig {
   import opened Fixtures
   import UUID
   import ErrorMessages = KeyStoreErrorMessages
+  import BranchKeyValidators
 
   method {:test} TestInvalidKmsKeyArnConfig() {
     var kmsClient :- expect KMS.KMSClient();
@@ -188,4 +192,22 @@ module TestConfig {
     keyStore := KeyStore.KeyStore(keyStoreConfig);
     expect keyStore.Success?;
   }
+
+  // Actually tests constructing a Key Store with no Clients
+  method {:test} TestGetKeysWithNoClients() {
+    var kmsConfig := Types.KMSConfiguration.kmsKeyArn(keyArn);
+    var keyStoreConfig := Types.KeyStoreConfig(
+      id := None,
+      kmsConfiguration := kmsConfig,
+      logicalKeyStoreName := logicalKeyStoreName,
+      grantTokens := None,
+      ddbTableName := Some(branchKeyStoreName),
+      ddbClient := None,
+      kmsClient := None
+    );
+    var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
+    var _ := BranchKeyValidators.testBeaconKeyHappyCase(keyStore, branchKeyId);
+    var _ := BranchKeyValidators.testActiveBranchKeyHappyCase(keyStore, branchKeyId, versionUtf8Bytes?:=Some(branchKeyIdActiveVersionUtf8Bytes));
+    var _ := BranchKeyValidators.testBranchKeyVersionHappyCase(keyStore, branchKeyId, branchKeyIdActiveVersion, branchKeyIdActiveVersionUtf8Bytes);
+  }
 }
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestCreateKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestCreateKeys.dfy
index 9c6e2f99ed..06a0c5d5fd 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestCreateKeys.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestCreateKeys.dfy
@@ -4,7 +4,8 @@
 include "../src/Index.dfy"
 include "Fixtures.dfy"
 include "CleanupItems.dfy"
-include "TestGetKeys.dfy"
+include "BranchKeyValidators.dfy"
+
 
 module {:options "/functionSyntax:4" } TestCreateKeys {
   import Types = AwsCryptographyKeyStoreTypes
@@ -21,92 +22,58 @@ module {:options "/functionSyntax:4" } TestCreateKeys {
   import KmsArn
   import UUID
   import AwsArnParsing
-  import TestGetKeys
-
-  /*
-    // If you need to re-create the MRK Branch Keys
-  
-    method {:test} TestCreateMRK()
-    {
-      var ddbClient :- expect DDB.DynamoDBClient();
-  
-      var keyStoreConfigEast := Types.KeyStoreConfig(
-        id := None,
-        kmsConfiguration := KmsConfigEast,
-        logicalKeyStoreName := logicalKeyStoreName,
-        grantTokens := None,
-        ddbTableName := branchKeyStoreName,
-        ddbClient := Some(ddbClient)
-      );
-  
-      var keyStoreConfigWest := Types.KeyStoreConfig(
-        id := None,
-        kmsConfiguration := KmsConfigWest,
-        logicalKeyStoreName := logicalKeyStoreName,
-        grantTokens := None,
-        ddbTableName := branchKeyStoreName,
-        ddbClient := Some(ddbClient)
-      );
-  
-      var keyStoreEast :- expect KeyStore.KeyStore(keyStoreConfigEast);
-      var keyStoreWest :- expect KeyStore.KeyStore(keyStoreConfigWest);
-  
-      var branchKeyIdWest :- expect keyStoreWest.CreateKey(Types.CreateKeyInput(
-                                                             branchKeyIdentifier := Some(WestBranchKey),
-                                                             encryptionContext := Some(KmsMrkEC)
-                                                           ));
-  
-      var branchKeyIdEast :- expect keyStoreEast.CreateKey(Types.CreateKeyInput(
-                                                             branchKeyIdentifier := Some(EastBranchKey),
-                                                             encryptionContext := Some(KmsMrkEC)
-                                                           ));
-  
-      expect branchKeyIdEast.branchKeyIdentifier == EastBranchKey;
-      expect branchKeyIdWest.branchKeyIdentifier == WestBranchKey;
-    }
-  */
-
-  method {:test} TestCreateBranchAndBeaconKeys()
+  import BranchKeyValidators
+
+  const happyCaseId := "test-happy-case-create-key-hv-1"
+  method {:test} TestCreateMRKForHV1()
   {
-    var kmsClient :- expect KMS.KMSClient();
     var ddbClient :- expect DDB.DynamoDBClient();
-    var kmsConfig := Types.KMSConfiguration.kmsKeyArn(keyArn);
-
-    var keyStoreConfig := Types.KeyStoreConfig(
-      id := None,
-      kmsConfiguration := kmsConfig,
-      logicalKeyStoreName := logicalKeyStoreName,
-      storage := Some(
-        Types.ddb(
-          Types.DynamoDBTable(
-            ddbTableName := branchKeyStoreName,
-            ddbClient := Some(ddbClient)
-          ))),
-      keyManagement := Some(
-        Types.kms(
-          Types.AwsKms(
-            kmsClient := Some(kmsClient)
-          )))
+    var storage :- expect DefaultStorage(ddbClient? := Some(ddbClient));
+    var keyStoreEast :- expect KeyStoreFromKMSConfig(
+      kmsConfig := KmsConfigEast,
+      ddbClient? := Some(ddbClient)
     );
-
-    var keyStore :- expect KeyStore.KeyStore(keyStoreConfig);
-
-    var branchKeyId :- expect keyStore.CreateKey(Types.CreateKeyInput(
-                                                   branchKeyIdentifier := None,
-                                                   encryptionContext := None
-                                                 ));
-
-    // Get branch key items from storage
-    TestGetKeys.VerifyGetKeys(
-      identifier := branchKeyId.branchKeyIdentifier,
-      keyStore := keyStore,
-      storage := keyStore.config.storage
+    var uuid :- expect UUID.GenerateUUID();
+    var bkid := happyCaseId + "-east-mrk-" + uuid;
+    var bk :- expect keyStoreEast.CreateKey(
+      Types.CreateKeyInput(
+        branchKeyIdentifier := Some(bkid),
+        encryptionContext := Some(KmsMrkEC)
+      ));
+    expect bk.branchKeyIdentifier == bkid;
+    BranchKeyValidators.VerifyGetKeys(bkid, keyStoreEast, storage,
+                                      encryptionContext := KmsMrkEC);
+    var keyStoreWest :- expect KeyStoreFromKMSConfig(
+      // Passing in KmsMrkConfigWest causes the KMS Client to be created for us-west-2
+      // EastBranchKey's KMS-ARN is replicated to us-west-2
+      kmsConfig := KmsMrkConfigWest,
+      ddbClient? := Some(ddbClient)
     );
+    BranchKeyValidators.VerifyGetKeys(bkid, keyStoreWest, storage,
+                                      encryptionContext := KmsMrkEC);
+    var _ := CleanupItems.DeleteBranchKey(Identifier:=bkid, ddbClient:=ddbClient);
+  }
 
-    // Since this process uses a read DDB table,
-    // the number of records will forever increase.
-    // To avoid this, remove the items.
-    var _ := CleanupItems.DeleteBranchKey(Identifier:=branchKeyId.branchKeyIdentifier, ddbClient:=ddbClient);
+  method {:test} TestCreateSRKForHV1()
+  {
+    var ddbClient :- expect DDB.DynamoDBClient();
+    var storage :- expect DefaultStorage(ddbClient? := Some(ddbClient));
+    var kmsConfig := Types.KMSConfiguration.kmsKeyArn(keyArn);
+    var keyStore :- expect KeyStoreFromKMSConfig(
+      kmsConfig := kmsConfig,
+      ddbClient? := Some(ddbClient)
+    );
+    var uuid :- expect UUID.GenerateUUID();
+    var bkid := happyCaseId + "-srk-" + uuid;
+    var bk :- expect keyStore.CreateKey(
+      Types.CreateKeyInput(
+        branchKeyIdentifier := Some(bkid),
+        encryptionContext := Some(KmsMrkEC)
+      ));
+    expect bk.branchKeyIdentifier == bkid;
+    BranchKeyValidators.VerifyGetKeys(bkid, keyStore, storage,
+                                      encryptionContext := KmsMrkEC);
+    var _ := CleanupItems.DeleteBranchKey(Identifier:=bkid, ddbClient:=ddbClient);
   }
 
   method {:test} TestCreateOptions()
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy
index c1215f1181..169ac991f5 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/test/TestGetKeys.dfy
@@ -5,10 +5,9 @@ include "../src/Index.dfy"
 include "Fixtures.dfy"
 include "CleanupItems.dfy"
 include "../src/ErrorMessages.dfy"
+include "BranchKeyValidators.dfy"
 
-// TODO-HV2-M1: add more HV2 tests.
-// TODO-HV2-M1: Maybe rename this module to TestGetHv1Keys and create another TestGetHv2Keys
-module TestGetKeys {
+module {:options "/functionSyntax:4" } TestGetKeys {
   import Types = AwsCryptographyKeyStoreTypes
   import ComAmazonawsKmsTypes
   import KMS = Com.Amazonaws.Kms
@@ -21,207 +20,124 @@ module TestGetKeys {
   import UTF8
   import ErrorMessages = KeyStoreErrorMessages
   import UUID
+  import BranchKeyValidators
 
   const incorrectLogicalName := "MySuperAwesomeTableName"
 
-  method VerifyGetKeys(
-    identifier : string,
-    keyStore : Types.IKeyStoreClient,
-    storage : Types.IKeyStorageInterface
-  )
-    requires
-      keyStore.ValidState() && storage.ValidState()
-    modifies
-      keyStore.Modifies, storage.Modifies
-    ensures
-      keyStore.ValidState() && storage.ValidState()
-
+  method {:test} TestGetKeysHappyCase()
   {
-    testBeaconKeyHappyCase(keyStore, identifier);
-
-    var activeResult := testAndGetActiveBranchKeyHappyCase(keyStore, identifier);
-    var branchKeyVersion :- expect UTF8.Decode(activeResult.branchKeyMaterials.branchKeyVersion);
-
-    testBranchKeyVersionHappyCase(keyStore, identifier, branchKeyVersion, activeResult.branchKeyMaterials.branchKeyVersion);
-    VerifyGetKeysFromStorage(identifier, storage);
-
-    //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
-    //= type=test
-    //# This guid MUST be [version 4 UUID](https://www.ietf.org/rfc/rfc4122.txt)
-    var versionString :- expect UTF8.Decode(activeResult.branchKeyMaterials.branchKeyVersion);
-    var versionByteUUID :- expect UUID.ToByteArray(versionString);
-    var versionRoundTrip :- expect UUID.FromByteArray(versionByteUUID);
-    expect versionRoundTrip == versionString;
+    var ddbClient :- expect DDB.DynamoDBClient();
+    var keyStore :- expect DefaultKeyStore(kmsId := keyArn, physicalName := branchKeyStoreName, logicalName := logicalKeyStoreName, ddbClient? := Some(ddbClient));
+    var storage :- expect DefaultStorage(ddbClient? := Some(ddbClient));
+    BranchKeyValidators.VerifyGetKeys(branchKeyId, keyStore, storage, versionUtf8Bytes?:=Some(branchKeyIdActiveVersionUtf8Bytes));
   }
 
-  method {:test} TestGetKeysHappyCase()
+  method {:test} TestGetKeysHV2HappyCase()
   {
-    var kmsClient :- expect KMS.KMSClient();
     var ddbClient :- expect DDB.DynamoDBClient();
-    var kmsConfig := Types.KMSConfiguration.kmsKeyArn(keyArn);
-
-    var keyStore :- expect DefaultKeyStore(kmsId := keyArn, physicalName := branchKeyStoreName, logicalName := logicalKeyStoreName, ddbClient? := Some(ddbClient), kmsClient? := Some(kmsClient));
-
-    testBeaconKeyHappyCase(keyStore, branchKeyId);
-    testBeaconKeyHappyCase(keyStore, hv2BranchKeyId);
-
-    testActiveBranchKeyHappyCase(keyStore, branchKeyId, branchKeyIdActiveVersionUtf8Bytes);
-    testActiveBranchKeyHappyCase(keyStore, hv2BranchKeyId, hv2BranchKeyIdActiveVersionUtf8Bytes);
-
-    testBranchKeyVersionHappyCase(keyStore, branchKeyId, branchKeyIdActiveVersion, branchKeyIdActiveVersionUtf8Bytes);
-    testBranchKeyVersionHappyCase(keyStore, hv2BranchKeyId, hv2BranchKeyVersion, hv2BranchKeyIdActiveVersionUtf8Bytes);
+    var keyStore :- expect DefaultKeyStore(kmsId := keyArn, physicalName := branchKeyStoreName, logicalName := logicalKeyStoreName, ddbClient? := Some(ddbClient));
+    var storage :- expect DefaultStorage(ddbClient? := Some(ddbClient));
+    BranchKeyValidators.VerifyGetKeys(hv2BranchKeyId, keyStore, storage,
+                                      versionUtf8Bytes?:=Some(hv2BranchKeyIdActiveVersionUtf8Bytes),
+                                      hierarchyVersion := Types.HierarchyVersion.v2);
   }
 
-  // TODO-HV2-M1: Add MRK test for hv2
-  method {:test} {:isolate_assertions} TestGetActiveMrkKey()
+  method {:test} TestGetMRKeySameRegionHappyCase()
   {
     var ddbClient :- expect DDB.DynamoDBClient();
-
-    var westKeyStore :- expect KeyStoreWithOptionalClient(
-      kmsId := MrkArnWest,
-      physicalName := branchKeyStoreName,
-      logicalName := logicalKeyStoreName,
+    var keyStore :- expect KeyStoreFromKMSConfig(
+      kmsConfig := KmsMrkConfigWest,
       ddbClient? := Some(ddbClient)
     );
+    var storage :- expect DefaultStorage(ddbClient? := Some(ddbClient));
+    BranchKeyValidators.VerifyGetKeys(WestBranchKey, keyStore, storage,
+                                      versionUtf8Bytes?:=Some(WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes),
+                                      encryptionContext := KmsMrkEC);
+  }
 
-    var eastKeyStore :- expect KeyStoreWithOptionalClient(
-      kmsId := MrkArnEast,
-      physicalName := branchKeyStoreName,
-      logicalName := logicalKeyStoreName,
+  method {:test} TestGetMRKeyReplicatedRegionHappyCase()
+  {
+    var ddbClient :- expect DDB.DynamoDBClient();
+    var storage :- expect DefaultStorage(ddbClient? := Some(ddbClient));
+    var keyStore :- expect KeyStoreFromKMSConfig(
+      // Passing in KmsMrkConfigWest causes the KMS Client to be created for us-west-2
+      // EastBranchKey's KMS-ARN is replicated to us-west-2
+      kmsConfig := KmsMrkConfigWest,
       ddbClient? := Some(ddbClient)
     );
+    BranchKeyValidators.VerifyGetKeys(EastBranchKey, keyStore, storage,
+                                      versionUtf8Bytes?:=Some(EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes),
+                                      encryptionContext := KmsMrkEC);
+  }
 
-    var westMrkKeyStore :- expect KeyStoreWithOptionalClient(
-      kmsId := MrkArnWest,
-      physicalName := branchKeyStoreName,
-      logicalName := logicalKeyStoreName,
-      ddbClient? := Some(ddbClient),
-      srkKey := false,
-      mrkKey := true
-    );
-
-    var eastMrkKeyStore :- expect KeyStoreWithOptionalClient(
-      kmsId := MrkArnEast,
-      physicalName := branchKeyStoreName,
-      logicalName := logicalKeyStoreName,
-      ddbClient? := Some(ddbClient),
-      srkKey := false,
-      mrkKey := true
+  method {:test} TestGetMRKeyMrkNotReplicatedFails()
+  {
+    var ddbClient :- expect DDB.DynamoDBClient();
+    var keyStore :- expect KeyStoreFromKMSConfig(
+      // Passing in KmsMrkConfigAP causes the KMS Client to be created for ap-south-2
+      // EastBranchKey's KMS-ARN is NOT replicated to ap-south-2
+      kmsConfig := KmsMrkConfigAP,
+      // However, we MUST pass in a DDB Client, as that needs to be created in us-west-2,
+      // or the error will be a DDB Error.
+      ddbClient? := Some(ddbClient)
     );
+    testActiveBranchKeyKMSFailureCase(keyStore, EastBranchKey);
+    testBeaconKeyKMSFailureCase(keyStore, EastBranchKey);
+    testBranchKeyVersionKMSFailureCase(keyStore, EastBranchKey, EastBranchKeyIdActiveVersion);
+  }
 
-    var apMrkKeyStore :- expect KeyStoreWithOptionalClient(
-      kmsId := MrkArnAP,
-      physicalName := branchKeyStoreName,
-      logicalName := logicalKeyStoreName,
-      ddbClient? := Some(ddbClient),
-      srkKey := false,
-      mrkKey := true
+  method {:test} TestGetSRKeyButKmsArnOutOfRegionFails()
+  {
+    var keyStore :- expect KeyStoreFromKMSConfig(
+      kmsConfig := KmsConfigWest
     );
-
-    // All four set of keys (branch, beacon and version) should work when the regions match
-    testActiveBranchKeyHappyCase(westKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-    testBeaconKeyHappyCase(westKeyStore, WestBranchKey);
-    testBranchKeyVersionHappyCase(westKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-
-    testActiveBranchKeyHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-    testBeaconKeyHappyCase(eastKeyStore, EastBranchKey);
-    testBranchKeyVersionHappyCase(eastKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-
-    testActiveBranchKeyHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-    testBeaconKeyHappyCase(westMrkKeyStore, WestBranchKey);
-    testBranchKeyVersionHappyCase(westMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-
-    testActiveBranchKeyHappyCase(eastMrkKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-    testBeaconKeyHappyCase(eastMrkKeyStore, EastBranchKey);
-    testBranchKeyVersionHappyCase(eastMrkKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-
-    // MRK Configuration should work with the other region
-
-    testActiveBranchKeyHappyCase(westMrkKeyStore, EastBranchKey, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-    testBeaconKeyHappyCase(westMrkKeyStore, EastBranchKey);
-    testBranchKeyVersionHappyCase(westMrkKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion, EastBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-
-    testActiveBranchKeyHappyCase(eastMrkKeyStore, WestBranchKey, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-    testBeaconKeyHappyCase(eastMrkKeyStore, WestBranchKey);
-    testBranchKeyVersionHappyCase(eastMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion, WestBranchKeyBranchKeyIdActiveVersionUtf8Bytes);
-
-    // Plain Configuration should fail with the other region
-
-    GetActiveKeyWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey);
-    GetBeaconKeyWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey);
-    GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(westKeyStore, EastBranchKey, EastBranchKeyIdActiveVersion);
-
-    GetActiveKeyWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey);
-    GetBeaconKeyWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey);
-    GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(eastKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion);
-
-    // apMrkKeyStore should always fail
-
-    testActiveBranchKeyKMSFailureCase(apMrkKeyStore, WestBranchKey);
-    testBranchKeyVersionKMSFailureCase(apMrkKeyStore, WestBranchKey, WestBranchKeyIdActiveVersion);
-    testBeaconKeyKMSFailureCase(apMrkKeyStore, WestBranchKey);
+    GetActiveKeyWithIncorrectKmsKeyArnHelper(keyStore, EastBranchKey);
+    GetBeaconKeyWithIncorrectKmsKeyArnHelper(keyStore, EastBranchKey);
+    GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(keyStore, EastBranchKey, EastBranchKeyIdActiveVersion);
   }
 
   method {:test} TestKeyWithIncorrectKmsKeyArn() {
-    var kmsClient :- expect KMS.KMSClient();
-    var ddbClient :- expect DDB.DynamoDBClient();
-
-    var keyStore :- expect DefaultKeyStore(kmsId := postalHornKeyArn, physicalName := branchKeyStoreName, logicalName := logicalKeyStoreName, ddbClient? := Some(ddbClient), kmsClient? := Some(kmsClient));
-
+    var keyStore :- expect DefaultKeyStore(kmsId := postalHornKeyArn, physicalName := branchKeyStoreName, logicalName := logicalKeyStoreName);
     GetActiveKeyWithIncorrectKmsKeyArnHelper(keyStore, branchKeyId);
-    GetActiveKeyWithIncorrectKmsKeyArnHelper(keyStore, hv2BranchKeyId);
-
     GetBeaconKeyWithIncorrectKmsKeyArnHelper(keyStore, branchKeyId);
-    GetBeaconKeyWithIncorrectKmsKeyArnHelper(keyStore, hv2BranchKeyId);
-
     GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(keyStore, branchKeyId, branchKeyIdActiveVersion);
+  }
+
+  method {:test} TestKeyWithIncorrectKmsKeyArnHV2() {
+    var keyStore :- expect DefaultKeyStore(kmsId := postalHornKeyArn, physicalName := branchKeyStoreName, logicalName := logicalKeyStoreName);
+    GetActiveKeyWithIncorrectKmsKeyArnHelper(keyStore, hv2BranchKeyId);
+    GetBeaconKeyWithIncorrectKmsKeyArnHelper(keyStore, hv2BranchKeyId);
     GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(keyStore, hv2BranchKeyId, hv2BranchKeyVersion);
   }
 
   method {:test} TestGetActiveKeyWrongLogicalKeyStoreName() {
-    var kmsClient :- expect KMS.KMSClient();
-    var ddbClient :- expect DDB.DynamoDBClient();
-
-    var keyStore :- expect DefaultKeyStore(kmsId:=keyArn, physicalName := branchKeyStoreName, logicalName := incorrectLogicalName, ddbClient? := Some(ddbClient), kmsClient? := Some(kmsClient));
+    var keyStore :- expect DefaultKeyStore(kmsId:=keyArn, physicalName := branchKeyStoreName, logicalName := incorrectLogicalName);
     GetActiveKeyWrongLogicalKeyStoreName(keyStore, branchKeyId, Types.HierarchyVersion.v1);
-    GetActiveKeyWrongLogicalKeyStoreName(keyStore, hv2BranchKeyId, Types.HierarchyVersion.v2);
-
     GetBeaconKeyWrongLogicalKeyStoreName(keyStore, branchKeyId, Types.HierarchyVersion.v1);
-    GetBeaconKeyWrongLogicalKeyStoreName(keyStore, hv2BranchKeyId, Types.HierarchyVersion.v2);
-
     GetVersionKeyWrongLogicalKeyStoreName(keyStore, branchKeyId, branchKeyIdActiveVersion, Types.HierarchyVersion.v1);
+  }
+
+
+  method {:test} TestGetActiveKeyWrongLogicalKeyStoreNameHV2() {
+    var keyStore :- expect DefaultKeyStore(kmsId:=keyArn, physicalName := branchKeyStoreName, logicalName := incorrectLogicalName);
+    GetActiveKeyWrongLogicalKeyStoreName(keyStore, hv2BranchKeyId, Types.HierarchyVersion.v2);
+    GetBeaconKeyWrongLogicalKeyStoreName(keyStore, hv2BranchKeyId, Types.HierarchyVersion.v2);
     GetVersionKeyWrongLogicalKeyStoreName(keyStore, hv2BranchKeyId, hv2BranchKeyVersion, Types.HierarchyVersion.v2);
   }
 
+  // This test does not consider HV b/c it is really testing the storage layer
   method {:test} TestGetKeyDoesNotExistFails()
   {
-    var kmsClient :- expect KMS.KMSClient();
-    var ddbClient :- expect DDB.DynamoDBClient();
-
-    var keyStore :- expect DefaultKeyStore(kmsId := keyArn, physicalName := branchKeyStoreName, logicalName := logicalKeyStoreName, ddbClient? := Some(ddbClient), kmsClient? := Some(kmsClient));
+    var keyStore :- expect DefaultKeyStore(kmsId := keyArn, physicalName := branchKeyStoreName, logicalName := logicalKeyStoreName);
     GetActiveKeyDoesNotExistFailsHelper(keyStore, "Robbie");
     GetBeaconKeyDoesNotExistFailsHelper(keyStore, "Robbie");
     GetBranchKeyVersionDoesNotExistFailsHelper(keyStore, "Robbie", branchKeyIdActiveVersion);
   }
 
-  method {:test} TestGetKeysWithNoClients() {
-    var kmsConfig := Types.KMSConfiguration.kmsKeyArn(keyArn);
-
-    var keyStore :- expect KeyStoreWithOptionalClient(kmsId:=keyArn, physicalName:=branchKeyStoreName, logicalName := logicalKeyStoreName);
-
-    testActiveBranchKeyHappyCase(keyStore, branchKeyId, branchKeyIdActiveVersionUtf8Bytes);
-    testActiveBranchKeyHappyCase(keyStore, hv2BranchKeyId, hv2BranchKeyIdActiveVersionUtf8Bytes);
-
-    testBeaconKeyHappyCase(keyStore, branchKeyId);
-    testBeaconKeyHappyCase(keyStore, hv2BranchKeyId);
-
-    testBranchKeyVersionHappyCase(keyStore, branchKeyId, branchKeyIdActiveVersion, branchKeyIdActiveVersionUtf8Bytes);
-    testBranchKeyVersionHappyCase(keyStore, hv2BranchKeyId, hv2BranchKeyVersion, hv2BranchKeyIdActiveVersionUtf8Bytes);
-  }
-
   method GetActiveKeyWrongLogicalKeyStoreName(keyStore: Types.IKeyStoreClient, branchKeyId: string, hv: Types.HierarchyVersion)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var activeResult := keyStore.GetActiveBranchKey(
       Types.GetActiveBranchKeyInput(
@@ -242,6 +158,7 @@ module TestGetKeys {
   method GetBeaconKeyWrongLogicalKeyStoreName(keyStore: Types.IKeyStoreClient, branchKeyId: string, hv: Types.HierarchyVersion)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var beaconKeyResult := keyStore.GetBeaconKey(
       Types.GetBeaconKeyInput(
@@ -262,6 +179,7 @@ module TestGetKeys {
   method GetVersionKeyWrongLogicalKeyStoreName(keyStore: Types.IKeyStoreClient, branchKeyId: string, branchKeyIdActiveVersion: string, hv: Types.HierarchyVersion)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var versionResult := keyStore.GetBranchKeyVersion(
       Types.GetBranchKeyVersionInput(
@@ -283,6 +201,7 @@ module TestGetKeys {
   method GetActiveKeyDoesNotExistFailsHelper(keyStore: Types.IKeyStoreClient, branchKeyId: string)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var activeResult := keyStore.GetActiveBranchKey(
       Types.GetActiveBranchKeyInput(
@@ -295,6 +214,7 @@ module TestGetKeys {
   method GetBeaconKeyDoesNotExistFailsHelper(keyStore: Types.IKeyStoreClient, branchKeyId: string)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var beaconKeyResult := keyStore.GetBeaconKey(
       Types.GetBeaconKeyInput(
@@ -307,6 +227,7 @@ module TestGetKeys {
   method GetBranchKeyVersionDoesNotExistFailsHelper(keyStore: Types.IKeyStoreClient, branchKeyId: string, branchKeyIdActiveVersion: string)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var versionResult := keyStore.GetBranchKeyVersion(
       Types.GetBranchKeyVersionInput(
@@ -326,12 +247,16 @@ module TestGetKeys {
         branchKeyIdentifier := branchKeyId
       ));
     expect activeResult.Failure?;
+    if (activeResult.error != Types.KeyStoreException(message := ErrorMessages.GET_KEY_ARN_DISAGREEMENT)) {
+      print "Expected GET_KEY_ARN_DISAGREEMENT but got: ", activeResult.error;
+    }
     expect activeResult.error == Types.KeyStoreException(message := ErrorMessages.GET_KEY_ARN_DISAGREEMENT);
   }
 
   method GetBeaconKeyWithIncorrectKmsKeyArnHelper(keyStore: Types.IKeyStoreClient, branchKeyId: string)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var beaconKeyResult := keyStore.GetBeaconKey(
       Types.GetBeaconKeyInput(
@@ -345,6 +270,7 @@ module TestGetKeys {
   method GetBranchKeyVersionWithIncorrectKmsKeyArnHelper(keyStore: Types.IKeyStoreClient, branchKeyId: string, branchKeyIdActiveVersion: string)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var versionResult := keyStore.GetBranchKeyVersion(
       Types.GetBranchKeyVersionInput(
@@ -356,82 +282,19 @@ module TestGetKeys {
     expect versionResult.error == Types.KeyStoreException(message := ErrorMessages.GET_KEY_ARN_DISAGREEMENT);
   }
 
-  method testBeaconKeyHappyCase(keyStore: Types.IKeyStoreClient, branchKeyId: string)
-    requires keyStore.ValidState()
-    modifies keyStore.Modifies
-  {
-    var beaconKeyResult :- expect keyStore.GetBeaconKey(
-      Types.GetBeaconKeyInput(
-        branchKeyIdentifier := branchKeyId
-      ));
-    expect isValidBeaconResult?(beaconKeyResult, branchKeyId);
-  }
-
-  predicate method isValidBeaconResult?(beaconKeyResult: Types.GetBeaconKeyOutput, branchKeyId: string) {
-    && beaconKeyResult.beaconKeyMaterials.beaconKeyIdentifier == branchKeyId
-    && beaconKeyResult.beaconKeyMaterials.beaconKey.Some?
-    && |beaconKeyResult.beaconKeyMaterials.beaconKey.value| == 32
-  }
-
-  method testActiveBranchKeyHappyCase(keyStore: Types.IKeyStoreClient, branchKeyId: string, branchKeyIdActiveVersionUtf8Bytes: seq<uint8>)
-    requires keyStore.ValidState()
-    modifies keyStore.Modifies
-  {
-    var branchKeyResult :- expect keyStore.GetActiveBranchKey(
-      Types.GetActiveBranchKeyInput(
-        branchKeyIdentifier := branchKeyId
-      ));
-    expect isValidActiveBranchKeyResult?(branchKeyResult, branchKeyId, Some(branchKeyIdActiveVersionUtf8Bytes));
-  }
-
-  method testAndGetActiveBranchKeyHappyCase(keyStore: Types.IKeyStoreClient, branchKeyId: string, nameonly branchKeyIdActiveVersionUtf8Bytes: Option<seq<uint8>> := None)
-    returns (output: Types.GetActiveBranchKeyOutput)
-    requires keyStore.ValidState()
-    modifies keyStore.Modifies
-  {
-    var branchKeyResult :- expect keyStore.GetActiveBranchKey(
-      Types.GetActiveBranchKeyInput(
-        branchKeyIdentifier := branchKeyId
-      ));
-    expect isValidActiveBranchKeyResult?(branchKeyResult, branchKeyId, branchKeyIdActiveVersionUtf8Bytes);
-    return branchKeyResult;
-  }
-
-  predicate method isValidActiveBranchKeyResult?(branchKeyResult: Types.GetActiveBranchKeyOutput, branchKeyId: string, branchKeyIdActiveVersionUtf8Bytes: Option<seq<uint8>>) {
-    && branchKeyResult.branchKeyMaterials.branchKeyIdentifier == branchKeyId
-    && (branchKeyIdActiveVersionUtf8Bytes.None? ||
-        branchKeyResult.branchKeyMaterials.branchKeyVersion == branchKeyIdActiveVersionUtf8Bytes.value)
-    && |branchKeyResult.branchKeyMaterials.branchKey| == 32
-  }
-
-  method testBranchKeyVersionHappyCase(keyStore: Types.IKeyStoreClient, branchKeyId: string, branchKeyIdActiveVersion: string, branchKeyIdActiveVersionUtf8Bytes: seq<uint8>)
-    requires keyStore.ValidState()
-    modifies keyStore.Modifies
-  {
-    var versionResult :- expect keyStore.GetBranchKeyVersion(
-      Types.GetBranchKeyVersionInput(
-        branchKeyIdentifier := branchKeyId,
-        branchKeyVersion := branchKeyIdActiveVersion
-      ));
-    var testBytes :- expect UTF8.Encode(branchKeyIdActiveVersion);
-    expect isValidBranchKeyVersionResult?(versionResult, branchKeyId, branchKeyIdActiveVersionUtf8Bytes, testBytes);
-  }
-
-  predicate method isValidBranchKeyVersionResult?(versionResult: Types.GetBranchKeyVersionOutput, branchKeyId: string, branchKeyIdActiveVersionUtf8Bytes: seq<uint8>, testBytes: UTF8.ValidUTF8Bytes) {
-    && versionResult.branchKeyMaterials.branchKeyIdentifier == branchKeyId
-    && versionResult.branchKeyMaterials.branchKeyVersion == branchKeyIdActiveVersionUtf8Bytes == testBytes
-    && |versionResult.branchKeyMaterials.branchKey| == 32
-  }
-
   method testActiveBranchKeyKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var branchKeyResult := keyStore.GetActiveBranchKey(
       Types.GetActiveBranchKeyInput(
         branchKeyIdentifier := branchKeyId
       ));
     expect branchKeyResult.Failure?;
+    if (!branchKeyResult.error.ComAmazonawsKms?) {
+      print "Expected KMS Error, but got: ", branchKeyResult.error;
+    }
     expect branchKeyResult.error.ComAmazonawsKms?;
     expect branchKeyResult.error.ComAmazonawsKms.OpaqueWithText?;
   }
@@ -439,6 +302,7 @@ module TestGetKeys {
   method testBranchKeyVersionKMSFailureCase(keyStore: Types.IKeyStoreClient, branchKeyId: string, branchKeyIdActiveVersion: string)
     requires keyStore.ValidState()
     modifies keyStore.Modifies
+    ensures keyStore.ValidState()
   {
     var versionResult := keyStore.GetBranchKeyVersion(
       Types.GetBranchKeyVersionInput(
@@ -462,61 +326,4 @@ module TestGetKeys {
     expect beaconKeyResult.error.ComAmazonawsKms?;
     expect beaconKeyResult.error.ComAmazonawsKms.OpaqueWithText?;
   }
-
-  method VerifyGetKeysFromStorage(
-    identifier : string,
-    storage : Types.IKeyStorageInterface
-  )
-    requires storage.ValidState()
-    modifies storage.Modifies
-    ensures storage.ValidState()
-  {
-    var encryptedActiveFromStorage :- expect storage.GetEncryptedActiveBranchKey(
-      Types.GetEncryptedActiveBranchKeyInput(
-        Identifier := identifier
-      )
-    );
-
-    var encryptedBeaconFromStorage :- expect storage.GetEncryptedBeaconKey(
-      Types.GetEncryptedBeaconKeyInput(
-        Identifier := identifier
-      )
-    );
-
-    expect encryptedActiveFromStorage.Item.Type.ActiveHierarchicalSymmetricVersion?;
-
-    var encryptedVersionFromStorage :- expect storage.GetEncryptedBranchKeyVersion(
-      Types.GetEncryptedBranchKeyVersionInput(
-        Identifier := identifier,
-        Version := encryptedActiveFromStorage.Item.Type.ActiveHierarchicalSymmetricVersion.Version
-      )
-    );
-
-    //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-and-beacon-key-creation
-    //= type=test
-    //# This timestamp MUST be in ISO 8601 format in UTC, to microsecond precision (e.g. “YYYY-MM-DDTHH:mm:ss.ssssssZ“)
-    expect ISO8601?(encryptedActiveFromStorage.Item.CreateTime);
-    expect ISO8601?(encryptedBeaconFromStorage.Item.CreateTime);
-    expect ISO8601?(encryptedVersionFromStorage.Item.CreateTime);
-  }
-
-  lemma ISO8601Test()
-  {
-    assert ISO8601?("2024-08-06T17:23:25.000874Z");
-  }
-
-  predicate method ISO8601?(
-    CreateTime: string
-  )
-  {
-    // “YYYY-MM-DDTHH:mm:ss.ssssssZ“
-    && |CreateTime| == 27
-    && CreateTime[4] == '-'
-    && CreateTime[7] == '-'
-    && CreateTime[10] == 'T'
-    && CreateTime[13] == ':'
-    && CreateTime[16] == ':'
-    && CreateTime[19] == '.'
-    && CreateTime[26] == 'Z'
-  }
 }
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/AdminFixtures.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/AdminFixtures.dfy
index da3df95ec5..a4fc543fb7 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/AdminFixtures.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/AdminFixtures.dfy
@@ -44,7 +44,8 @@ module {:options "/functionSyntax:4" } AdminFixtures {
       ddbClient := ddbClient,
       logicalKeyStoreName := logicalName,
       ddbTableNameUtf8 := physicalNameUtf8,
-      logicalKeyStoreNameUtf8 := logicalNameUtf8);
+      logicalKeyStoreNameUtf8 := logicalNameUtf8
+    );
 
     var underTestConfig := Types.KeyStoreAdminConfig(
       logicalKeyStoreName := logicalName,
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/Mutations/TestDecryptEncrypt.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/Mutations/TestDecryptEncrypt.dfy
index 0fd671557e..9bdf790430 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/Mutations/TestDecryptEncrypt.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/Mutations/TestDecryptEncrypt.dfy
@@ -82,6 +82,7 @@ module {:options "/functionSyntax:4" } TestDecryptEncryptStrat {
 
     var timestamp :- expect Time.GetCurrentTimeStamp();
     var newCustomEC: KeyStoreTypes.EncryptionContextString := map["Koda" := timestamp];
+    // TODO-HV-2-M2: We should Mutate with Mrk Key as well
     var mutationsRequest := Types.Mutations(TerminalEncryptionContext := Some(newCustomEC));
     var initInput := Types.InitializeMutationInput(
       Identifier := testId,
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/TestAdminCreateKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/TestAdminCreateKeys.dfy
index be966b9035..c277add48d 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/TestAdminCreateKeys.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/TestAdminCreateKeys.dfy
@@ -4,8 +4,7 @@
 include "../src/Index.dfy"
 include "../../AwsCryptographyKeyStore/test/CleanupItems.dfy"
 include "../../AwsCryptographyKeyStore/test/Fixtures.dfy"
-include "../../AwsCryptographyKeyStore/test/TestGetKeys.dfy"
-include "../../AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy"
+include "../../AwsCryptographyKeyStore/test/BranchKeyValidators.dfy"
 include "AdminFixtures.dfy"
 
 module {:options "/functionSyntax:4" } TestAdminCreateKeys {
@@ -22,9 +21,12 @@ module {:options "/functionSyntax:4" } TestAdminCreateKeys {
   import UUID
   import CleanupItems
   import AdminFixtures
-  import TestGetKeys
+  import BranchKeyValidators
 
-  method {:test} TestCreateBranchAndBeaconKeys()
+  // TODO-HV-2-FOLLOW : TestCreateSRKForHV1, TestCreateForHV1NoBKID, TestCreateForHV1BbkidNoECFails
+
+  const happyCaseId := "test-happy-case-admin-create-key-hv-1"
+  method {:test} TestCreateMRKForHV1()
   {
     var ddbClient :- expect Fixtures.ProvideDDBClient();
     var kmsClient :- expect Fixtures.ProvideKMSClient();
@@ -32,26 +34,145 @@ module {:options "/functionSyntax:4" } TestAdminCreateKeys {
     var keyStore :- expect Fixtures.DefaultKeyStore(ddbClient?:=Some(ddbClient), kmsClient?:=Some(kmsClient));
     var strategy :- expect AdminFixtures.DefaultKeyManagerStrategy(kmsClient?:=Some(kmsClient));
     var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
+    var keyStoreEast :- expect KeyStoreFromKMSConfig(
+      kmsConfig := KmsMrkConfigEast,
+      ddbClient? := Some(ddbClient)
+    );
+    var uuid :- expect UUID.GenerateUUID();
+    var bkid := happyCaseId + "-west-mrk-" + uuid;
+    // Create an HV-1 BK with a West MRK by calling us-west-2
+    var bk :- expect underTest.CreateKey(
+      Types.CreateKeyInput(
+        Identifier := Some(bkid),
+        EncryptionContext := Some(KmsMrkEC),
+        KmsArn := Types.KmsSymmetricKeyArn.KmsMRKeyArn(MrkArnWest),
+        // us-west-2 b/c CI region is us-west-2 and KMS Client is created
+        Strategy := Some(strategy)
+      ));
+    expect bk.Identifier == bkid;
+    // Validate an HV-1 BK with a West MRK by calling us-east-1
+    BranchKeyValidators.VerifyGetKeys(bkid, keyStoreEast, storage,
+                                      encryptionContext := KmsMrkEC);
+    var keyStoreWest :- expect KeyStoreFromKMSConfig(
+      // Passing in KmsMrkConfigWest causes the KMS Client to be created for us-west-2
+      // bk's KMS-ARN is replicated to us-west-2
+      kmsConfig := KmsMrkConfigWest,
+      ddbClient? := Some(ddbClient)
+    );
+    // Validate an HV-1 BK with a West MRK by calling us-west-2
+    BranchKeyValidators.VerifyGetKeys(bkid, keyStoreWest, storage,
+                                      encryptionContext := KmsMrkEC);
+    var _ := CleanupItems.DeleteBranchKey(Identifier:=bkid, ddbClient:=ddbClient);
+  }
 
-    var input := Types.CreateKeyInput(
-      Identifier := None,
-      EncryptionContext := None,
-      KmsArn := Types.KmsSymmetricKeyArn.KmsKeyArn(keyArn),
-      Strategy := Some(strategy)
+  // TODO-HV-2-M2?: Document that BKSA ONLY calls KMS/DDB for the region of the supplied clients.
+  // or Ensure BKSA has similar behavior as BKS in terms of MRK region.
+  const happyCaseIdHV2 := "test-happy-case-admin-create-key-hv-2"
+  method {:test} TestCreateMRKForHV2()
+  {
+    var ddbClient :- expect Fixtures.ProvideDDBClient();
+    var kmsClient :- expect Fixtures.ProvideKMSClient();
+    var storage :- expect Fixtures.DefaultStorage(ddbClient?:=Some(ddbClient));
+    var strategy :- expect AdminFixtures.SimpleKeyManagerStrategy(kmsClient?:=Some(kmsClient));
+    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
+    var keyStoreEast :- expect KeyStoreFromKMSConfig(
+      kmsConfig := KmsMrkConfigEast,
+      ddbClient? := Some(ddbClient)
     );
-    var identifier? :- expect underTest.CreateKey(input);
-    var identifier := identifier?.Identifier;
-
-    // Get branch key items from storage
-    TestGetKeys.VerifyGetKeys(
-      identifier := identifier,
-      keyStore := keyStore,
-      storage := storage
+    var uuid :- expect UUID.GenerateUUID();
+    var bkid := happyCaseIdHV2 + "-west-mrk-" + uuid;
+    // Create an HV-2 BK with a West MRK by calling us-west-2
+    var bk :- expect underTest.CreateKey(
+      Types.CreateKeyInput(
+        Identifier := Some(bkid),
+        EncryptionContext := Some(RobbieEC),
+        KmsArn := Types.KmsSymmetricKeyArn.KmsMRKeyArn(MrkArnWest),
+        // us-west-2 b/c CI region is us-west-2 and KMS Client is created
+        Strategy := Some(strategy),
+        HierarchyVersion := Some(KeyStoreTypes.HierarchyVersion.v2)
+      ));
+    expect bk.Identifier == bkid;
+    // Validate an HV-2 BK with a West MRK by calling us-east-1
+    BranchKeyValidators.VerifyGetKeys(bkid, keyStoreEast, storage,
+                                      encryptionContext := RobbieEC,
+                                      hierarchyVersion := KeyStoreTypes.HierarchyVersion.v2);
+    var keyStoreWest :- expect KeyStoreFromKMSConfig(
+      // Passing in KmsMrkConfigWest causes the KMS Client to be created for us-west-2
+      // bk's KMS-ARN is replicated to us-west-2
+      kmsConfig := KmsMrkConfigWest,
+      ddbClient? := Some(ddbClient)
     );
+    // Validate an HV-2 BK with a West MRK by calling us-west-2
+    BranchKeyValidators.VerifyGetKeys(bkid, keyStoreWest, storage,
+                                      encryptionContext := RobbieEC,
+                                      hierarchyVersion := KeyStoreTypes.HierarchyVersion.v2);
+    var _ := CleanupItems.DeleteBranchKey(Identifier:=bkid, ddbClient:=ddbClient);
+  }
 
-    // Since this process uses a read DDB table,
-    // the number of records will forever increase.
-    // To avoid this, remove the items.
-    var _ := CleanupItems.DeleteBranchKey(Identifier:=identifier, ddbClient:=ddbClient);
+  method {:test} TestCreateSRKForHV2()
+  {
+    var ddbClient :- expect Fixtures.ProvideDDBClient();
+    var kmsClient :- expect Fixtures.ProvideKMSClient();
+    var storage :- expect Fixtures.DefaultStorage(ddbClient?:=Some(ddbClient));
+    var keyStore :- expect Fixtures.DefaultKeyStore(ddbClient?:=Some(ddbClient), kmsClient?:=Some(kmsClient));
+    var strategy :- expect AdminFixtures.SimpleKeyManagerStrategy(kmsClient?:=Some(kmsClient));
+    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
+    var uuid :- expect UUID.GenerateUUID();
+    var bkid := happyCaseIdHV2 + "-west-srk-" + uuid;
+    // Create an HV-2 BK with a West SRK by calling us-west-2
+    var bk :- expect underTest.CreateKey(
+      Types.CreateKeyInput(
+        Identifier := Some(bkid),
+        EncryptionContext := Some(RobbieEC),
+        KmsArn := Types.KmsSymmetricKeyArn.KmsKeyArn(keyArn),
+        // us-west-2 b/c CI region is us-west-2 and KMS Client is created
+        Strategy := Some(strategy),
+        HierarchyVersion := Some(KeyStoreTypes.HierarchyVersion.v2)
+      ));
+    expect bk.Identifier == bkid;
+    // Validate an HV-2 BK with a West SRK by calling us-west-2
+    BranchKeyValidators.VerifyGetKeys(bkid, keyStore, storage,
+                                      encryptionContext := RobbieEC,
+                                      hierarchyVersion := KeyStoreTypes.HierarchyVersion.v2);
+    var _ := CleanupItems.DeleteBranchKey(Identifier:=bkid, ddbClient:=ddbClient);
+  }
+
+  method {:test} TestCreateSRKForHV2NoEC()
+  {
+    var ddbClient :- expect Fixtures.ProvideDDBClient();
+    var kmsClient :- expect Fixtures.ProvideKMSClient();
+    var storage :- expect Fixtures.DefaultStorage(ddbClient?:=Some(ddbClient));
+    var keyStore :- expect Fixtures.DefaultKeyStore(ddbClient?:=Some(ddbClient), kmsClient?:=Some(kmsClient));
+    var strategy :- expect AdminFixtures.SimpleKeyManagerStrategy(kmsClient?:=Some(kmsClient));
+    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
+    var bk :- expect underTest.CreateKey(
+      Types.CreateKeyInput(
+        KmsArn := Types.KmsSymmetricKeyArn.KmsKeyArn(keyArn),
+        Strategy := Some(strategy),
+        HierarchyVersion := Some(KeyStoreTypes.HierarchyVersion.v2)
+      ));
+    BranchKeyValidators.VerifyGetKeys(bk.Identifier, keyStore, storage,
+                                      hierarchyVersion := KeyStoreTypes.HierarchyVersion.v2);
+    var _ := CleanupItems.DeleteBranchKey(Identifier:=bk.Identifier, ddbClient:=ddbClient);
+  }
+
+  method {:test} TestCreateSRKForHV2BkidWithNoECFails()
+  {
+    var ddbClient :- expect Fixtures.ProvideDDBClient();
+    var kmsClient :- expect Fixtures.ProvideKMSClient();
+    var storage :- expect Fixtures.DefaultStorage(ddbClient?:=Some(ddbClient));
+    var strategy :- expect AdminFixtures.SimpleKeyManagerStrategy(kmsClient?:=Some(kmsClient));
+    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
+    var uuid :- expect UUID.GenerateUUID();
+    var bkid := happyCaseIdHV2 + "-west-srk-no-ec-fails-" + uuid;
+    var bk? := underTest.CreateKey(
+      Types.CreateKeyInput(
+        Identifier := Some(bkid),
+        KmsArn := Types.KmsSymmetricKeyArn.KmsKeyArn(keyArn),
+        Strategy := Some(strategy),
+        HierarchyVersion := Some(KeyStoreTypes.HierarchyVersion.v2)
+      ));
+    expect bk?.Failure?, "Admin CreateKey, with an Identifier, but no EC, MUST Fail";
+    var _ := CleanupItems.DeleteBranchKey(Identifier:=bkid, ddbClient:=ddbClient);
   }
 }
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/TestAdminHV1Only.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/TestAdminHV1Only.dfy
index 21db35c333..715b74d6bb 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/TestAdminHV1Only.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStoreAdmin/test/TestAdminHV1Only.dfy
@@ -5,10 +5,8 @@ include "../src/Index.dfy"
 include "../../AwsCryptographyKeyStore/test/CleanupItems.dfy"
 include "../../AwsCryptographyKeyStore/test/Fixtures.dfy"
 include "../../AwsCryptographyKeyStore/test/TestGetKeys.dfy"
-include "../../AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy"
 include "AdminFixtures.dfy"
 
-// TODO-HV-2-M1 : remove HV-1 restriction for CreateKey
 // TODO-HV-2-M2 : remove HV-1 restriction for Mutations
 module {:options "/functionSyntax:4" } TestAdminHV1Only {
   import Types = AwsCryptographyKeyStoreAdminTypes
@@ -26,81 +24,6 @@ module {:options "/functionSyntax:4" } TestAdminHV1Only {
   import AdminFixtures
   import TestGetKeys
 
-  const happyCaseId := "test-create-key-hv-2-happy-case"
-
-  method {:test} TestCreateKeyForHV2HappyCase()
-  {
-    var ddbClient :- expect Fixtures.ProvideDDBClient();
-    var kmsClient :- expect Fixtures.ProvideKMSClient();
-    var storage :- expect Fixtures.DefaultStorage(ddbClient?:=Some(ddbClient));
-    var keyStore :- expect Fixtures.DefaultKeyStore(ddbClient?:=Some(ddbClient), kmsClient?:=Some(kmsClient));
-    var strategy :- expect AdminFixtures.SimpleKeyManagerStrategy(kmsClient?:=Some(kmsClient));
-    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
-
-    var input := Types.CreateKeyInput(
-      Identifier := None,
-      EncryptionContext := None,
-      KmsArn := Types.KmsSymmetricKeyArn.KmsKeyArn(keyArn),
-      Strategy := Some(strategy),
-      HierarchyVersion := Some(KeyStoreTypes.HierarchyVersion.v2)
-    );
-
-    var createKeyOutput? :- expect underTest.CreateKey(input);
-    expect createKeyOutput?.HierarchyVersion == KeyStoreTypes.HierarchyVersion.v2;
-
-    // Get branch key items from storage
-    TestGetKeys.VerifyGetKeys(
-      identifier := createKeyOutput?.Identifier,
-      keyStore := keyStore,
-      storage := storage
-    );
-
-    // Since this process uses a read DDB table,
-    // the number of records will forever increase.
-    // To avoid this, remove the items.
-    var _ := CleanupItems.DeleteBranchKey(Identifier:=createKeyOutput?.Identifier, ddbClient:=ddbClient);
-  }
-
-  method {:test} TestCreateKeyForHV2CreateOptions() {
-    var ddbClient :- expect Fixtures.ProvideDDBClient();
-    var kmsClient :- expect Fixtures.ProvideKMSClient();
-    var storage :- expect Fixtures.DefaultStorage(ddbClient?:=Some(ddbClient));
-    var keyStore :- expect Fixtures.DefaultKeyStore(ddbClient?:=Some(ddbClient), kmsClient?:=Some(kmsClient));
-    var strategy :- expect AdminFixtures.SimpleKeyManagerStrategy(kmsClient?:=Some(kmsClient));
-    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
-
-    // Create key with Custom EC & Branch Key Identifier
-    var uuid :- expect UUID.GenerateUUID();
-    var branchKeyId := happyCaseId + "-" + uuid;
-
-    var customEC := map[UTF8.EncodeAscii("Koda") := UTF8.EncodeAscii("Is a dog.")];
-
-    var input := Types.CreateKeyInput(
-      Identifier := Some(branchKeyId),
-      EncryptionContext := Some(customEC),
-      KmsArn := Types.KmsSymmetricKeyArn.KmsKeyArn(keyArn),
-      Strategy := Some(strategy),
-      HierarchyVersion := Some(KeyStoreTypes.HierarchyVersion.v2)
-    );
-
-    var createKeyOutput? :- expect underTest.CreateKey(input);
-    expect branchKeyId == createKeyOutput?.Identifier;
-    expect createKeyOutput?.HierarchyVersion == KeyStoreTypes.HierarchyVersion.v2;
-
-    // Get branch key items from storage
-    TestGetKeys.VerifyGetKeys(
-      identifier := branchKeyId,
-      keyStore := keyStore,
-      storage := storage
-    );
-
-    // Since this process uses a read DDB table,
-    // the number of records will forever increase.
-    // To avoid this, remove the items.
-    var _ := CleanupItems.DeleteBranchKey(Identifier:=branchKeyId, ddbClient:=ddbClient);
-  }
-
-  // TODO-HV-2-M2 : Probably make this a happy test?
   const testMutateForHV2FailsCaseId := "dafny-initialize-mutation-hv-2-rejection"
   method {:test} TestMutateForHV2Fails()
   {
@@ -108,7 +31,7 @@ module {:options "/functionSyntax:4" } TestAdminHV1Only {
     var testId := testMutateForHV2FailsCaseId + "-" + uuid;
     var ddbClient :- expect Fixtures.ProvideDDBClient();
     var kmsClient :- expect Fixtures.ProvideKMSClient();
-    var underTest :- expect AdminFixtures.DefaultAdmin();
+    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
     var strategy :- expect AdminFixtures.DefaultKeyManagerStrategy(kmsClient?:=Some(kmsClient));
     var systemKey := Types.SystemKey.trustStorage(trustStorage := Types.TrustStorage());
     Fixtures.CreateHappyCaseId(id:=testId);
@@ -136,7 +59,7 @@ module {:options "/functionSyntax:4" } TestAdminHV1Only {
     var testId := testMutateForHV1WithAwsKmsSimpleFailsCaseId + "-" + uuid;
     var ddbClient :- expect Fixtures.ProvideDDBClient();
     var kmsClient :- expect Fixtures.ProvideKMSClient();
-    var underTest :- expect AdminFixtures.DefaultAdmin();
+    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
     var simpleStrategy :- expect AdminFixtures.SimpleKeyManagerStrategy(kmsClient?:=Some(kmsClient));
     var systemKey := Types.SystemKey.trustStorage(trustStorage := Types.TrustStorage());
     Fixtures.CreateHappyCaseId(id:=testId);
@@ -165,7 +88,7 @@ module {:options "/functionSyntax:4" } TestAdminHV1Only {
     var testId := testMutateInitEncountersHV2FailsCaseId + "-" + uuid;
     var ddbClient :- expect Fixtures.ProvideDDBClient();
     var kmsClient :- expect Fixtures.ProvideKMSClient();
-    var underTest :- expect AdminFixtures.DefaultAdmin();
+    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
     var strategy :- expect AdminFixtures.DefaultKeyManagerStrategy(kmsClient?:=Some(kmsClient));
     var systemKey := Types.SystemKey.trustStorage(trustStorage := Types.TrustStorage());
     Fixtures.CreateHappyCaseId(id:=testId);
@@ -175,7 +98,7 @@ module {:options "/functionSyntax:4" } TestAdminHV1Only {
       alsoViolateBeacon? := true, ddbClient? := Some(ddbClient),
       kmsClient?:=Some(kmsClient), violateReservedAttribute:=true);
 
-    print logPrefix + "re-wrote the item to be described as HV-2 even though it's not" + "\n";
+    // print logPrefix + "re-wrote the item to be described as HV-2 even though it's not" + "\n";
 
     var mutationsRequest := Types.Mutations(TerminalKmsArn := Some(Fixtures.postalHornKeyArn));
     var initInput := Types.InitializeMutationInput(
@@ -186,13 +109,13 @@ module {:options "/functionSyntax:4" } TestAdminHV1Only {
       DoNotVersion := Some(true));
     var initializeOutput := underTest.InitializeMutation(initInput);
 
-    print logPrefix + "initializeOutput :: ", initializeOutput, "\n";
+    // print logPrefix + "initializeOutput :: ", initializeOutput, "\n";
 
     var _ := CleanupItems.DeleteBranchKey(Identifier:=testId, ddbClient:=ddbClient);
     expect initializeOutput.Failure?, "Should have failed InitializeMutation when HV-2 encountered by InitMutation.";
   }
 
-  // TODO-HV-2-M2 : Probably make this a happy test?
+  // TODO-HV-2-M3 : Probably make this a happy test?
   const testVersionKeyEncountersHV2FailsCaseId := "dafny-version-key-encounters-hv-2-rejection"
   const logPrefixVersion := "\n" + testVersionKeyEncountersHV2FailsCaseId + " :: "
   method {:test} TestVersionKeyEncountersHV2Fails()
@@ -201,7 +124,7 @@ module {:options "/functionSyntax:4" } TestAdminHV1Only {
     var testId := testVersionKeyEncountersHV2FailsCaseId + "-" + uuid;
     var ddbClient :- expect Fixtures.ProvideDDBClient();
     var kmsClient :- expect Fixtures.ProvideKMSClient();
-    var underTest :- expect AdminFixtures.DefaultAdmin();
+    var underTest :- expect AdminFixtures.DefaultAdmin(ddbClient?:=Some(ddbClient));
     var strategy :- expect AdminFixtures.DefaultKeyManagerStrategy(kmsClient?:=Some(kmsClient));
     var systemKey := Types.SystemKey.trustStorage(trustStorage := Types.TrustStorage());
     Fixtures.CreateHappyCaseId(id:=testId);
@@ -211,7 +134,7 @@ module {:options "/functionSyntax:4" } TestAdminHV1Only {
       alsoViolateBeacon? := true, ddbClient? := Some(ddbClient),
       kmsClient?:=Some(kmsClient), violateReservedAttribute:=true);
 
-    print logPrefixVersion + "re-wrote the item to be described as HV-2 even though it's not" + "\n";
+    // print logPrefixVersion + "re-wrote the item to be described as HV-2 even though it's not" + "\n";
 
     var versionInput := Types.VersionKeyInput(
       Identifier := testId,
@@ -219,7 +142,7 @@ module {:options "/functionSyntax:4" } TestAdminHV1Only {
       Strategy := Some(strategy));
     var actualOutput := underTest.VersionKey(versionInput);
 
-    print logPrefixVersion + "actualOutput :: ", actualOutput, "\n";
+    // print logPrefixVersion + "actualOutput :: ", actualOutput, "\n";
 
     var _ := CleanupItems.DeleteBranchKey(Identifier:=testId, ddbClient:=ddbClient);
     expect actualOutput.Failure?, "Should have failed VersionKey when HV-2 encountered by VersionKey.";