diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/DefaultClientSupplier.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/DefaultClientSupplier.dfy
index 6ef80a204..fa20f9c8f 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/DefaultClientSupplier.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/DefaultClientSupplier.dfy
@@ -47,7 +47,7 @@ module DefaultClientSupplier {
       ensures GetClientEnsuresPublicly(input, output)
       ensures unchanged(History)
     {
-      var maybeClient := Kms.KMSClient();
+      var maybeClient := Kms.KMSClientForRegion(input.region);
       return maybeClient.MapFailure(e => ComAmazonawsKms(e));
     }
 
diff --git a/ComAmazonawsKms/runtimes/java/src/main/java/Dafny/Com/Amazonaws/Kms/__default.java b/ComAmazonawsKms/runtimes/java/src/main/java/Dafny/Com/Amazonaws/Kms/__default.java
index 4877f79d1..7a265ec96 100644
--- a/ComAmazonawsKms/runtimes/java/src/main/java/Dafny/Com/Amazonaws/Kms/__default.java
+++ b/ComAmazonawsKms/runtimes/java/src/main/java/Dafny/Com/Amazonaws/Kms/__default.java
@@ -34,11 +34,14 @@ public static Result<IKMSClient, Error> KMSClient() {
         }
     }
 
-    public static Result<IKMSClient, Error> KMSClient(final String region) {
+    public static Result<IKMSClient, Error> KMSClientForRegion(
+        final DafnySequence<? extends Character> region
+    ) {
         try {
+            final String regionString = new String((char[]) region.toArray().unwrap());
             KmsClientBuilder builder = KmsClient.builder();
-            KmsClient client = builder.region(Region.of(region)).build();
-            IKMSClient shim = new Shim(client, region);
+            KmsClient client = builder.region(Region.of(regionString)).build();
+            IKMSClient shim = new Shim(client, regionString);
             return Result.create_Success(shim);
         } catch (Exception e) {
             Error dafny_error = Error.create_KMSInternalException(
diff --git a/ComAmazonawsKms/runtimes/net/Extern/KMSClient.cs b/ComAmazonawsKms/runtimes/net/Extern/KMSClient.cs
index 356e84cc0..690280e1c 100644
--- a/ComAmazonawsKms/runtimes/net/Extern/KMSClient.cs
+++ b/ComAmazonawsKms/runtimes/net/Extern/KMSClient.cs
@@ -18,8 +18,6 @@ public static
       >
       KMSClient()
     {
-      // var region = RegionEndpoint.GetBySystemName("us-west-2");
-      // TODO add user agent, endpoint, and region
       var client = new AmazonKeyManagementServiceClient();
 
       return Result<
@@ -29,16 +27,36 @@ public static
         .create_Success(new KeyManagementServiceShim(client));
     }
 
-        public static _IOption<bool> RegionMatch(
-            Dafny.Com.Amazonaws.Kms.Types.IKMSClient client,
-            Dafny.ISequence<char> region)
-        {
-            string regionStr = TypeConversion.FromDafny_N6_smithy__N3_api__S6_String(region);
-            // We should never be passing anything other than KeyManagementServiceShim as the 'client'.
-            // If this cast fails, that indicates that there is something wrong with
-            // our code generation.
-            IAmazonKeyManagementService nativeClient = ((KeyManagementServiceShim)client)._impl;
-            return new Option_Some<bool>(nativeClient.Config.RegionEndpoint.SystemName.Equals(regionStr));
-        }    
+    public static
+      _IResult<
+        Types.IKMSClient,
+        Types._IError
+      >
+      KMSClientForRegion(
+        Dafny.ISequence<char> regionDafnyString
+      )
+    {
+      string regionStr = TypeConversion.FromDafny_N6_smithy__N3_api__S6_String(regionDafnyString);
+      var region = RegionEndpoint.GetBySystemName(regionStr);
+      var client = new AmazonKeyManagementServiceClient(region);
+
+      return Result<
+        Types.IKMSClient,
+        Types._IError
+      >
+        .create_Success(new KeyManagementServiceShim(client));
+    }
+
+    public static _IOption<bool> RegionMatch(
+        Dafny.Com.Amazonaws.Kms.Types.IKMSClient client,
+        Dafny.ISequence<char> region
+    ) {
+        string regionStr = TypeConversion.FromDafny_N6_smithy__N3_api__S6_String(region);
+        // We should never be passing anything other than KeyManagementServiceShim as the 'client'.
+        // If this cast fails, that indicates that there is something wrong with
+        // our code generation.
+        IAmazonKeyManagementService nativeClient = ((KeyManagementServiceShim)client)._impl;
+        return new Option_Some<bool>(nativeClient.Config.RegionEndpoint.SystemName.Equals(regionStr));
+    }    
   }
 }
diff --git a/ComAmazonawsKms/src/Index.dfy b/ComAmazonawsKms/src/Index.dfy
index 8cbc5930b..7d34efdbb 100644
--- a/ComAmazonawsKms/src/Index.dfy
+++ b/ComAmazonawsKms/src/Index.dfy
@@ -20,4 +20,12 @@ module {:extern "Dafny.Com.Amazonaws.Kms"} Com.Amazonaws.Kms refines AbstractCom
     region: string
   ): Option<bool>
 
+  method {:extern} KMSClientForRegion(region: string)
+    returns (res: Result<IKMSClient, Error>)
+    ensures res.Success? ==> 
+    && fresh(res.value)
+    && fresh(res.value.Modifies)
+    && fresh(res.value.History)
+    && res.value.ValidState()
+
 }