diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
index af51e21e8b..a6a72d7288 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
@@ -15,7 +15,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
   import AwsCryptographyPrimitivesTypes
   import ComAmazonawsDynamodbTypes
   import ComAmazonawsKmsTypes
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AlgorithmSuites.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AlgorithmSuites.dfy
index 74f74a9634..bc58deb71c 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AlgorithmSuites.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/AlgorithmSuites.dfy
@@ -82,26 +82,26 @@ module AlgorithmSuites {
     // If there is a KDF, the output length MUST match the encrypt length
     && (a.kdf.HKDF? ==>
           && a.kdf.HKDF.outputKeyLength == a.encrypt.AES_GCM.keyLength)
-       // If there is a signature, there MUST be a KDF
+    // If there is a signature, there MUST be a KDF
     && (a.signature.ECDSA? ==> a.kdf.HKDF?)
-       // If there is commitment, the KDF MUST match
+    // If there is commitment, the KDF MUST match
     && (a.commitment.HKDF? ==>
           && a.commitment.HKDF.saltLength == 32
           && a.commitment == a.kdf)
-       // If there is a IntermediateKeyWrapping, the KDFs MUST match
+    // If there is a IntermediateKeyWrapping, the KDFs MUST match
     && (a.edkWrapping.IntermediateKeyWrapping? ==>
           && a.kdf.HKDF?
           && a.edkWrapping.IntermediateKeyWrapping.keyEncryptionKeyKdf == a.kdf
           && a.edkWrapping.IntermediateKeyWrapping.macKeyKdf == a.kdf)
-       // If there is a KDF and no commitment then salt MUST be 0
+    // If there is a KDF and no commitment then salt MUST be 0
     && (a.kdf.HKDF? && a.commitment.None? ==> a.kdf.HKDF.saltLength == 0)
-       //= aws-encryption-sdk-specification/framework/algorithm-suites.md#algorithm-suites-signature-settings
-       //= type=implication
-       //# An algorithm suite with a symmetric signature algorithm MUST use [intermediate key wrapping](#intermediate-key-wrapping).
-       //
-       // If the algorithm suite includes an symmetric signature algorithm:
-       //= aws-encryption-sdk-specification/framework/algorithm-suites.md#symmetric-signature-algorithm
-       //# - The algorithm suite MUST also use [Intermediate Key Wrapping](#intermediate-key-wrapping).
+    //= aws-encryption-sdk-specification/framework/algorithm-suites.md#algorithm-suites-signature-settings
+    //= type=implication
+    //# An algorithm suite with a symmetric signature algorithm MUST use [intermediate key wrapping](#intermediate-key-wrapping).
+    //
+    // If the algorithm suite includes an symmetric signature algorithm:
+    //= aws-encryption-sdk-specification/framework/algorithm-suites.md#symmetric-signature-algorithm
+    //# - The algorithm suite MUST also use [Intermediate Key Wrapping](#intermediate-key-wrapping).
     && (!a.symmetricSignature.None? ==>
           && a.edkWrapping.IntermediateKeyWrapping?)
   }
@@ -119,7 +119,7 @@ module AlgorithmSuites {
   {
     // Adheres to constraints for all algorithm suites
     && AlgorithmSuiteInfo?(a)
-       // All ESDK encrypt with AES_GCM
+    // All ESDK encrypt with AES_GCM
     && SupportedESDKEncrypt?(a.encrypt)
 
     // Specification for each supported ESDK Algorithm Suite
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy
index 05bdf5d772..4c80069e7d 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/LocalCMC.dfy
@@ -344,7 +344,7 @@ module {:options "/functionSyntax:4" } LocalCMC {
       && this in InternalModifies
       && queue in InternalModifies
       && cache in InternalModifies
-                  // I want to say that `queue.Items` is somehow in InternalModifies
+      // I want to say that `queue.Items` is somehow in InternalModifies
       && (forall i <- queue.Items :: i in InternalModifies)
       && Invariant()
     }
@@ -353,15 +353,15 @@ module {:options "/functionSyntax:4" } LocalCMC {
       reads this, queue, queue.Items, cache
     {
       && queue.Invariant()
-         // 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.
+      // 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.
       && MutableMapIsInjective(cache)
-         // Given that cache.Values and queue.Items are unique
-         // they MUST contain exactly the same elements.
+      // Given that cache.Values and queue.Items are unique
+      // they MUST contain exactly the same elements.
       && multiset(cache.Values()) == multiset(queue.Items)
-         // To remove the tail the key associated
-         // with the tail MUST be in the cache
+      // To remove the tail the key associated
+      // with the tail MUST be in the cache
       && (forall c <- queue.Items :: c.identifier in cache.Keys() && cache.Select(c.identifier) == c)
 
       && (ValueIsSafeBecauseItIsInMemory(cache.Size()); cache.Size() as uint64 <= entryCapacity)
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTracker.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTracker.dfy
index 897838ffb9..75813a4135 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTracker.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMCs/StormTracker.dfy
@@ -197,10 +197,10 @@ module {:options "/functionSyntax:4" }  StormTracker {
       ensures
         output ==>
           && result.expiryTime < 0x20C49BA5E353F7
-             // The + 1 comes because (now / 1000) * 1000 <= now
-             // Consider (5001 / 1000) <= 5
-             // (5001 / 1000) == 5
-             // but 5 * 1000 < 5001
+          // The + 1 comes because (now / 1000) * 1000 <= now
+          // Consider (5001 / 1000) <= 5
+          // (5001 / 1000) == 5
+          // but 5 * 1000 < 5001
           && (result.expiryTime  * 1000) - gracePeriod <= now < (result.expiryTime + 1) * 1000
     {
       // This is just showing where this constant comes from
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMM.dfy
index be0c7217fe..f505ee0ac4 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMM.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMM.dfy
@@ -36,10 +36,10 @@ module {:options "/functionSyntax:4" } CMM {
             //# - For every key in [Required Encryption Context Keys](structures.md#required-encryption-context-keys)
             //#   there MUST be a matching key in the [Encryption Context](structures.md#encryption-context-1).
             && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.encryptionMaterials)
-               //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials
-               //= type=implication
-               //# - The [Required Encryption Context Keys](structures.md#required-encryption-context-keys) MUST be
-               //#   a super set of the Required Encryption Context Keys in the [encryption materials request](#encryption-materials-request).
+            //= aws-encryption-sdk-specification/framework/cmm-interface.md#get-encryption-materials
+            //= type=implication
+            //# - The [Required Encryption Context Keys](structures.md#required-encryption-context-keys) MUST be
+            //#   a super set of the Required Encryption Context Keys in the [encryption materials request](#encryption-materials-request).
             && RequiredEncryptionContextKeys?(input.requiredEncryptionContextKeys, output.value.encryptionMaterials)
 
     ghost predicate DecryptMaterialsEnsuresPublicly(input: Types.DecryptMaterialsInput, output: Result<Types.DecryptMaterialsOutput, Types.Error>)
@@ -57,19 +57,19 @@ module {:options "/functionSyntax:4" } CMM {
               //# - The decryption materials returned MUST follow the specification for [decryption-materials](structures.md#decryption-materials).
               //# - The value of the plaintext data key MUST be non-NULL.
               ==> Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials))
-             //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-             //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context)
-             //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context)
-             //# in [decrypt materials request](#decrypt-materials-request).
-             //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context)
-             //# and [Encryption Context](structures.md#encryption-context),
-             //# the values MUST be equal or the operation MUST fail.
+          //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+          //# The CMM MUST validate the [Encryption Context](structures.md#encryption-context)
+          //# by comparing it to the customer supplied [Reproduced Encryption Context](structures.md#encryption-context)
+          //# in [decrypt materials request](#decrypt-materials-request).
+          //# For every key that exists in both [Reproduced Encryption Context](structures.md#encryption-context)
+          //# and [Encryption Context](structures.md#encryption-context),
+          //# the values MUST be equal or the operation MUST fail.
           && (output.Success? ==> ReproducedEncryptionContext?(input))
           && (!ReproducedEncryptionContext?(input) ==> output.Failure?)
-             //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-             //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
-             //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
-             //# SHOULD be appended to the decryption materials.
+          //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+          //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
+          //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
+          //# SHOULD be appended to the decryption materials.
           && (output.Success? ==> EncryptionContextComplete(input, output.value.decryptionMaterials))
   }
 
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy
index 90b47efe54..004869f20c 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/DefaultCMM.dfy
@@ -146,10 +146,10 @@ module DefaultCMM {
                   //# value `base64-encoded public verification key`
                   //# to the [encryption context](structures.md#encryption-context).
                   && Materials.EC_PUBLIC_KEY_FIELD in output.value.encryptionMaterials.encryptionContext
-                                                      //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
-                                                      //= type=implication
-                                                      //# If the algorithm suite contains a [signing algorithm](algorithm-suites.md#signature-algorithm),
-                                                      //# the default CMM MUST Generate a [signing key](structures.md#signing-key).
+                  //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
+                  //= type=implication
+                  //# If the algorithm suite contains a [signing algorithm](algorithm-suites.md#signature-algorithm),
+                  //# the default CMM MUST Generate a [signing key](structures.md#signing-key).
                   && output.value.encryptionMaterials.signingKey.Some?
                 )
 
@@ -193,25 +193,25 @@ module DefaultCMM {
         && output.Success?
         ==>
           && |keyring.History.OnEncrypt| == |old(keyring.History.OnEncrypt)| + 1
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
-             //= type=implication
-             //# On each call to Get Encryption Materials,
-             //# the default CMM MUST make a call to its [keyring's](#keyring)
-             //# [On Encrypt](keyring-interface.md#onencrypt) operation.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
+          //= type=implication
+          //# On each call to Get Encryption Materials,
+          //# the default CMM MUST make a call to its [keyring's](#keyring)
+          //# [On Encrypt](keyring-interface.md#onencrypt) operation.
           && Seq.Last(keyring.History.OnEncrypt).output.Success?
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
-             //= type=implication
-             //# The default CMM MUST obtain the Plaintext Data Key from the
-             //# On Encrypt Response and include it in the
-             //# [encryption materials](structures.md#encryption-materials) returned.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
+          //= type=implication
+          //# The default CMM MUST obtain the Plaintext Data Key from the
+          //# On Encrypt Response and include it in the
+          //# [encryption materials](structures.md#encryption-materials) returned.
           && Seq.Last(keyring.History.OnEncrypt).output.value.materials.plaintextDataKey
              == output.value.encryptionMaterials.plaintextDataKey
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
-             //= type=implication
-             //# The default CMM MUST obtain the
-             //# [Encrypted Data Keys](structures.md#encrypted-data-keys)
-             //# from the On Encrypt Response and include it
-             //# in the [encryption materials](structures.md#encryption-materials) returned.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#get-encryption-materials
+          //= type=implication
+          //# The default CMM MUST obtain the
+          //# [Encrypted Data Keys](structures.md#encrypted-data-keys)
+          //# from the On Encrypt Response and include it
+          //# in the [encryption materials](structures.md#encryption-materials) returned.
           && Seq.Last(keyring.History.OnEncrypt).output.value.materials.encryptedDataKeys
              == output.value.encryptionMaterials.encryptedDataKeys
 
@@ -320,11 +320,11 @@ module DefaultCMM {
       && (output.Success?
           ==>
             && Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials))
-         //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-         //= type=implication
-         //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
-         //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
-         //# SHOULD be appended to the decryption materials.
+      //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+      //= type=implication
+      //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
+      //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
+      //# SHOULD be appended to the decryption materials.
       && (output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials))
     }
 
@@ -421,18 +421,18 @@ module DefaultCMM {
                 //# - If the decrypt materials request contains an algorithm suite,
                 //# the decryption materials returned SHOULD contain the same algorithm suite.
                 && input.algorithmSuiteId == output.value.decryptionMaterials.algorithmSuite.id
-                   //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-                   //= type=implication
-                   //# If the algorithm suite obtained from the decryption request contains a [signing algorithm](algorithm-suites.md#signature-algorithm),
-                   //# the decryption materials MUST include the [signature verification key](structures.md#verification-key).
+                //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+                //= type=implication
+                //# If the algorithm suite obtained from the decryption request contains a [signing algorithm](algorithm-suites.md#signature-algorithm),
+                //# the decryption materials MUST include the [signature verification key](structures.md#verification-key).
                 && (output.value.decryptionMaterials.algorithmSuite.signature.ECDSA? ==> output.value.decryptionMaterials.verificationKey.Some?)
 
                 && (0 < |output.value.decryptionMaterials.requiredEncryptionContextKeys| ==> input.reproducedEncryptionContext.Some?)
-                   //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-                   //= type=implication
-                   //# - This set MUST include all keys added to the decryption materials encryption context
-                   //# that existed in the [decrypt materials request's](#decrypt-materials-request) reproduced encryption context
-                   //# but did not exist in the [decrypt materials request's](#decrypt-materials-request) encryption context.
+                //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+                //= type=implication
+                //# - This set MUST include all keys added to the decryption materials encryption context
+                //# that existed in the [decrypt materials request's](#decrypt-materials-request) reproduced encryption context
+                //# but did not exist in the [decrypt materials request's](#decrypt-materials-request) encryption context.
                 && (forall key <- output.value.decryptionMaterials.requiredEncryptionContextKeys
                       ::
                         && key !in input.encryptionContext
@@ -442,17 +442,17 @@ module DefaultCMM {
         && output.Success?
         ==>
           && |keyring.History.OnDecrypt| == |old(keyring.History.OnDecrypt)| + 1
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#decrypt-materials
-             //= type=implication
-             //# On each call to Decrypt Materials,
-             //# the default CMM MUST make a call to its [keyring's](#keyring)
-             //# [On Decrypt](keyring-interface.md#ondecrypt) operation.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#decrypt-materials
+          //= type=implication
+          //# On each call to Decrypt Materials,
+          //# the default CMM MUST make a call to its [keyring's](#keyring)
+          //# [On Decrypt](keyring-interface.md#ondecrypt) operation.
           && Seq.Last(keyring.History.OnDecrypt).output.Success?
-             //= aws-encryption-sdk-specification/framework/default-cmm.md#decrypt-materials
-             //= type=implication
-             //# The default CMM MUST obtain the Plaintext Data Key from
-             //# the On Decrypt response and include it in the decrypt
-             //# materials returned.
+          //= aws-encryption-sdk-specification/framework/default-cmm.md#decrypt-materials
+          //= type=implication
+          //# The default CMM MUST obtain the Plaintext Data Key from
+          //# the On Decrypt response and include it in the decrypt
+          //# materials returned.
           && Seq.Last(keyring.History.OnDecrypt).output.value.materials.plaintextDataKey
              == output.value.decryptionMaterials.plaintextDataKey
 
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy
index 9d762243ea..12cac8dabb 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/CMMs/RequiredEncryptionContextCMM.dfy
@@ -230,11 +230,11 @@ module RequiredEncryptionContextCMM {
       && (output.Success?
           ==>
             && Materials.DecryptionMaterialsWithPlaintextDataKey(output.value.decryptionMaterials))
-         //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
-         //= type=implication
-         //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
-         //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
-         //# SHOULD be appended to the decryption materials.
+      //= aws-encryption-sdk-specification/framework/cmm-interface.md#decrypt-materials
+      //= type=implication
+      //# - All key-value pairs that exist in [Reproduced Encryption Context](structures.md#encryption-context)
+      //# but do not exist in encryption context on the [decrypt materials request](#decrypt-materials-request)
+      //# SHOULD be appended to the decryption materials.
       && (output.Success? ==> CMM.EncryptionContextComplete(input, output.value.decryptionMaterials))
     }
 
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Commitment.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Commitment.dfy
index 6eb4d26477..b02ffabec6 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Commitment.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Commitment.dfy
@@ -46,13 +46,13 @@ module Commitment {
              //= type=implication
              //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.ESDK(REQUIRE_ENCRYPT_ALLOW_DECRYPT)
-                //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-require-decrypt
-                //= type=implication
-                //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
+             //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-require-decrypt
+             //= type=implication
+             //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.ESDK(ESDKCommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
-                //= aws-encryption-sdk-specification/framework/commitment-policy.md#dbe-require-encrypt-require-decrypt
-                //= type=implication
-                //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
+             //= aws-encryption-sdk-specification/framework/commitment-policy.md#dbe-require-encrypt-require-decrypt
+             //= type=implication
+             //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.DBE(DBECommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
            )
         && var suite := AlgorithmSuites.GetSuite(algorithm);
@@ -69,11 +69,11 @@ module Commitment {
              //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-allow-decrypt
              //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.ESDK(REQUIRE_ENCRYPT_ALLOW_DECRYPT)
-                //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-require-decrypt
-                //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
+             //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-require-decrypt
+             //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.ESDK(ESDKCommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
-                //= aws-encryption-sdk-specification/framework/commitment-policy.md#dbe-require-encrypt-require-decrypt
-                //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
+             //= aws-encryption-sdk-specification/framework/commitment-policy.md#dbe-require-encrypt-require-decrypt
+             //# - [Get Encryption Materials](./cmm-interface.md#get-encryption-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.DBE(DBECommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
            )
         && var suite := AlgorithmSuites.GetSuite(algorithm);
@@ -137,9 +137,9 @@ module Commitment {
              //= type=implication
              //# - [Decrypt Materials](./cmm-interface.md#decrypt-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.ESDK(ESDKCommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
-                //= aws-encryption-sdk-specification/framework/commitment-policy.md#dbe-require-encrypt-require-decrypt
-                //= type=implication
-                //# - [Decrypt Materials](./cmm-interface.md#decrypt-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
+             //= aws-encryption-sdk-specification/framework/commitment-policy.md#dbe-require-encrypt-require-decrypt
+             //= type=implication
+             //# - [Decrypt Materials](./cmm-interface.md#decrypt-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.DBE(DBECommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
            )
         && var suite := AlgorithmSuites.GetSuite(algorithm);
@@ -156,8 +156,8 @@ module Commitment {
              //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-require-decrypt
              //# - [Decrypt Materials](./cmm-interface.md#decrypt-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.ESDK(ESDKCommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
-                //= aws-encryption-sdk-specification/framework/commitment-policy.md#dbe-require-encrypt-require-decrypt
-                //# - [Decrypt Materials](./cmm-interface.md#decrypt-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
+             //= aws-encryption-sdk-specification/framework/commitment-policy.md#dbe-require-encrypt-require-decrypt
+             //# - [Decrypt Materials](./cmm-interface.md#decrypt-materials) MUST only support algorithm suites that have a [Key Commitment](./algorithm-suites.md#algorithm-suites-encryption-key-derivation-settings) value of True
              || commitmentPolicy == CommitmentPolicy.DBE(DBECommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
            )
         && var suite := AlgorithmSuites.GetSuite(algorithm);
@@ -175,9 +175,9 @@ module Commitment {
           //= type=implication
           //# - [Decrypt Materials](./cmm-interface.md#decrypt-materials) MUST support all algorithm suites
           || commitmentPolicy == CommitmentPolicy.ESDK(FORBID_ENCRYPT_ALLOW_DECRYPT)
-             //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-allow-decrypt
-             //= type=implication
-             //# - [Decrypt Materials](./cmm-interface.md#decrypt-materials) MUST support all algorithm suites
+          //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-allow-decrypt
+          //= type=implication
+          //# - [Decrypt Materials](./cmm-interface.md#decrypt-materials) MUST support all algorithm suites
           || commitmentPolicy == CommitmentPolicy.ESDK(REQUIRE_ENCRYPT_ALLOW_DECRYPT)
         )
       )
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Defaults.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Defaults.dfy
index a1654316ee..c67cc0ad6f 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Defaults.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Defaults.dfy
@@ -23,9 +23,9 @@ module Defaults {
       //= type=implication
       //# - `05 78` MUST be the default algorithm suite
       || commitmentPolicy == CommitmentPolicy.ESDK(REQUIRE_ENCRYPT_ALLOW_DECRYPT)
-         //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-require-decrypt
-         //= type=implication
-         //# - `05 78` MUST be the default algorithm suite
+      //= aws-encryption-sdk-specification/framework/commitment-policy.md#esdk-require-encrypt-require-decrypt
+      //= type=implication
+      //# - `05 78` MUST be the default algorithm suite
       || commitmentPolicy == CommitmentPolicy.ESDK(ESDKCommitmentPolicy.REQUIRE_ENCRYPT_REQUIRE_DECRYPT)
       ==>
         output == AlgorithmSuiteId.ESDK(ALG_AES_256_GCM_HKDF_SHA512_COMMIT_KEY_ECDSA_P384)
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy
index 98420cf572..43601f3fcc 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EcdhEdkWrapping.dfy
@@ -360,23 +360,23 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
       ==>
         && Invariant()
         && 0 < |crypto.History.AESEncrypt|
-           //= aws-encryption-sdk-specification/framework/raw-ecdh-keyring.md#data-key-wrapping
-           //= type=implication
-           //# The keyring MUST encrypt the plaintext data key
-           //# using AES-GCM and use the shared wrapping key as the wrapping key.
+        //= aws-encryption-sdk-specification/framework/raw-ecdh-keyring.md#data-key-wrapping
+        //= type=implication
+        //# The keyring MUST encrypt the plaintext data key
+        //# using AES-GCM and use the shared wrapping key as the wrapping key.
         && Seq.Last(crypto.History.AESEncrypt).output.Success?
         && var AESEncryptInput := Seq.Last(crypto.History.AESEncrypt).input;
         && var AESEncryptOutput := Seq.Last(crypto.History.AESEncrypt).output.value;
         && var iv := seq(ECDH_AES_256_ENC_ALG.ivLength as nat, _ => 0);
         && AESEncryptInput.encAlg == ECDH_AES_256_ENC_ALG
         && AESEncryptInput.msg == input.plaintextMaterial
-           //= aws-encryption-sdk-specification/framework/raw-ecdh-keyring.md#data-key-wrapping
-           //= type=implication
-           //# - It MUST use a zeroed out 12 byte IV
+        //= aws-encryption-sdk-specification/framework/raw-ecdh-keyring.md#data-key-wrapping
+        //= type=implication
+        //# - It MUST use a zeroed out 12 byte IV
         && AESEncryptInput.iv == iv
-           //= aws-encryption-sdk-specification/framework/raw-ecdh-keyring.md#data-key-wrapping
-           //= type=implication
-           // - It MUST use the serialized [encryption context](structures.md#encryption-context-1) as the additional authenticated data (AAD).
+        //= aws-encryption-sdk-specification/framework/raw-ecdh-keyring.md#data-key-wrapping
+        //= type=implication
+        // - It MUST use the serialized [encryption context](structures.md#encryption-context-1) as the additional authenticated data (AAD).
         && AESEncryptInput.aad == fixedInfo
         && |res.value.wrappedMaterial| > |AESEncryptOutput.cipherText| + |AESEncryptOutput.authTag|
     }
@@ -490,10 +490,10 @@ module {:options "/functionSyntax:4" } EcdhEdkWrapping {
             )
     ensures res.Success? ==>
               && Last(crypto.History.KdfCounterMode).output.Success?
-                 //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-ecdh-keyring.md#onencrypt
-                 //= type=implication
-                 //# If they Key Derivation step succeeds it MUST produce
-                 //# keying material with a length of 64 bytes.
+              //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-ecdh-keyring.md#onencrypt
+              //= type=implication
+              //# If they Key Derivation step succeeds it MUST produce
+              //# keying material with a length of 64 bytes.
               && |Last(crypto.History.KdfCounterMode).output.value| == KDF_EXPECTED_LEN as int
               && |res.value| == |Last(crypto.History.KdfCounterMode).output.value|
   {
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy
index 2184b84b31..b7b720612b 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/KeyWrapping/EdkWrapping.dfy
@@ -73,7 +73,7 @@ module EdkWrapping {
   method WrapEdkMaterial<T>(
     nameonly encryptionMaterials: Types.EncryptionMaterials,
     nameonly wrap: MaterialWrapping.WrapMaterial<T>,
-    nameonly generateAndWrap: MaterialWrapping.GenerateAndWrapMaterial<T>
+                                                 nameonly generateAndWrap: MaterialWrapping.GenerateAndWrapMaterial<T>
   ) returns (ret: Result<WrapEdkMaterialOutput<T>, Types.Error>)
     requires wrap.Invariant()
     requires generateAndWrap.Invariant()
@@ -177,7 +177,7 @@ module EdkWrapping {
                  wrapInfo := ret.value.wrapInfo)),
              [])
   {
-    // It would be nice if we could require this.
+      // It would be nice if we could require this.
     :- Need(Materials.ValidEncryptionMaterials(encryptionMaterials),
             Types.AwsCryptographicMaterialProvidersException(
               message := "Invalid materials for encryption."));
@@ -241,7 +241,7 @@ module EdkWrapping {
         );
     } else if (encryptionMaterials.plaintextDataKey.None?
                && encryptionMaterials.algorithmSuite.edkWrapping.IntermediateKeyWrapping?) {
-      // Generate pdk and wrap using Intermediate Key Wrapping
+        // Generate pdk and wrap using Intermediate Key Wrapping
       :- Need(encryptionMaterials.algorithmSuite.commitment.HKDF?,
               Types.AwsCryptographicMaterialProvidersException(
                 message := "Invalid algorithm suite: suites with intermediate key wrapping must use key commitment."));
@@ -313,7 +313,7 @@ module EdkWrapping {
                 Success(unwrapRes),
                 [])
   {
-    // TODO require this
+      // TODO require this
     :- Need(Materials.ValidDecryptionMaterials(decryptionMaterials),
             Types.AwsCryptographicMaterialProvidersException(
               message := "Invalid materials for decryption."));
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyring.dfy
index c98143c99d..58da4b25c4 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyring.dfy
@@ -27,7 +27,7 @@ module {:options "/functionSyntax:4" } Keyring {
           output.Success?
           ==>
             && Materials.EncryptionMaterialsHasPlaintextDataKey(output.value.materials)
-               // See the details of ValidEncryptionMaterialsTransition for the following
+            // See the details of ValidEncryptionMaterialsTransition for the following
 
             //= aws-encryption-sdk-specification/framework/keyring-interface.md#generate-data-key
             //= type=implication
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy
index b25688d0f0..701ae154ad 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsDiscoveryKeyring.dfy
@@ -180,10 +180,10 @@ module AwsKmsDiscoveryKeyring {
         ==>
           && var stringifiedEncCtx := StringifyEncryptionContext(input.materials.encryptionContext).Extract();
           && 0 < |client.History.Decrypt|
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
-             //= type=implication
-             //# - The length of the response’s `Plaintext` MUST equal the [key derivation input length](../algorithm-suites.md#key-derivation-input-length)
-             //#  specified by the [algorithm suite](../algorithm-suites.md) included in the input [decryption materials](../structures.md#decryption-materials).
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
+          //= type=implication
+          //# - The length of the response’s `Plaintext` MUST equal the [key derivation input length](../algorithm-suites.md#key-derivation-input-length)
+          //#  specified by the [algorithm suite](../algorithm-suites.md) included in the input [decryption materials](../structures.md#decryption-materials).
           && AlgorithmSuites.GetEncryptKeyLength(input.materials.algorithmSuite) as nat == |res.value.materials.plaintextDataKey.value|
           && var LastDecrypt := Seq.Last(client.History.Decrypt);
           && LastDecrypt.output.Success?
@@ -195,9 +195,9 @@ module AwsKmsDiscoveryKeyring {
                    EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, res.value.materials.algorithmSuite);
                  && maybeProviderWrappedMaterial.Success?
                  && KMS.IsValid_CiphertextType(maybeProviderWrappedMaterial.value)
-                    //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
-                    //= type=implication
-                    //# - Its provider ID MUST exactly match the value “aws-kms”.
+                 //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
+                 //= type=implication
+                 //# - Its provider ID MUST exactly match the value “aws-kms”.
                  && edk.keyProviderId == PROVIDER_ID
                  && KMS.IsValid_KeyIdType(awsKmsKey)
 
@@ -218,9 +218,9 @@ module AwsKmsDiscoveryKeyring {
                     //= type=implication
                     //# When calling [AWS KMS Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html), the keyring MUST call with a request constructed as follows:
                     == request
-                    //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
-                    //= type=implication
-                    //# If the response does satisfy these requirements then OnDecrypt MUST do the following with the response:
+                 //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
+                 //= type=implication
+                 //# If the response does satisfy these requirements then OnDecrypt MUST do the following with the response:
                  && Seq.Last(client.History.Decrypt).output.value.Plaintext.Some?
                  && (
                       input.materials.algorithmSuite.edkWrapping.DIRECT_KEY_WRAPPING? ==>
@@ -349,9 +349,9 @@ module AwsKmsDiscoveryKeyring {
       returns (output: Result<bool, Types.Error>)
       ensures Ensures(edk, output)
     {
-      // The Keyring produces UTF8 providerInfo.
-      // If an `aws-kms` encrypted data key's providerInfo is not UTF8
-      // this is an error, not simply an EDK to filter out.
+        // The Keyring produces UTF8 providerInfo.
+        // If an `aws-kms` encrypted data key's providerInfo is not UTF8
+        // this is an error, not simply an EDK to filter out.
       :- Need(UTF8.ValidUTF8Seq(edk.keyProviderInfo),
               Types.AwsCryptographicMaterialProvidersException(
                 message := "Invalid AWS KMS encoding, provider info is not UTF8."));
@@ -429,10 +429,10 @@ module AwsKmsDiscoveryKeyring {
       returns (res: Result<seq<AwsKmsEdkHelper>, Types.Error>)
       ensures Ensures(edk, res)
     {
-      // This transform only works if the given EDK is a valid AWS KMS-generated EDK
-      // Ideally we would add these as pre-conditions on the method, but we're extending the
-      // ActionWithResult trait which does not have pre-conditions and we cannot make our
-      // implementation more restrictive.
+        // This transform only works if the given EDK is a valid AWS KMS-generated EDK
+        // Ideally we would add these as pre-conditions on the method, but we're extending the
+        // ActionWithResult trait which does not have pre-conditions and we cannot make our
+        // implementation more restrictive.
       :- Need(edk.keyProviderId == PROVIDER_ID,
               Types.AwsCryptographicMaterialProvidersException(
                 message := "Encrypted data key was not generated by KMS"));
@@ -507,12 +507,12 @@ module AwsKmsDiscoveryKeyring {
         && KMS.IsValid_KeyIdType(keyArn)
         && var maybeStringifiedEncCtx := StringifyEncryptionContext(materials.encryptionContext);
         && maybeStringifiedEncCtx.Success?
-           // Confirm that the materials we're about to output are a valid transition
-           // from the input materials
+        // Confirm that the materials we're about to output are a valid transition
+        // from the input materials
         && Materials.DecryptionMaterialsTransitionIsValid(materials, res.value)
         && 0 < |client.History.Decrypt|
-           // Confirm that we called KMS in the right way and correctly returned the values
-           // it gave us
+        // Confirm that we called KMS in the right way and correctly returned the values
+        // it gave us
         && KMS.DecryptRequest(
              KeyId := Some(keyArn),
              CiphertextBlob := maybeProviderWrappedMaterial.value,
@@ -526,9 +526,9 @@ module AwsKmsDiscoveryKeyring {
              materials.algorithmSuite.edkWrapping.DIRECT_KEY_WRAPPING? ==>
                Seq.Last(client.History.Decrypt).output.value.Plaintext
                == res.value.plaintextDataKey)
-           //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
-           //= type=implication
-           //# - The `KeyId` field in the response MUST equal the AWS KMS ARN from the provider info
+        //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
+        //= type=implication
+        //# - The `KeyId` field in the response MUST equal the AWS KMS ARN from the provider info
         && Seq.Last(client.History.Decrypt).output.value.KeyId == Some(keyArn)
     }
 
@@ -584,9 +584,9 @@ module AwsKmsDiscoveryKeyring {
         //= type=implication
         //# - If a discovery filter is configured, its partition and the provider info partition MUST match.
         && discoveryFilter.value.partition == arn.partition
-           //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
-           //= type=implication
-           //# - If a discovery filter is configured, its set of accounts MUST contain the provider info account.
+        //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-discovery-keyring.md#ondecrypt
+        //= type=implication
+        //# - If a discovery filter is configured, its set of accounts MUST contain the provider info account.
         && discoveryFilter.value.accountIds <= [arn.account]
   {
     && match discoveryFilter {
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy
index 798b5c927a..b54e13b517 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsEcdhKeyring.dfy
@@ -186,8 +186,8 @@ module {:options "/functionSyntax:4" } AwsKmsEcdhKeyring {
         this.senderKmsKeyId.Some?,
         E("Keyring MUST be configured with a sender KMS Key ID")
       );
-      // Impossible to hit on encrypt, but dafny has a hard time inferring that if we are not discovery we
-      // will have senderKmsKeyId.
+        // Impossible to hit on encrypt, but dafny has a hard time inferring that if we are not discovery we
+        // will have senderKmsKeyId.
       :- Need(
         this.senderPublicKey.Some?,
         E("Keyring MUST be configured with a senderPublicKey")
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy
index 99ba43b24c..e0a4acd881 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsKeyring.dfy
@@ -171,10 +171,10 @@ module AwsKmsKeyring {
           && var maybeStringifiedEncCtx := StringifyEncryptionContext(input.materials.encryptionContext);
           && maybeStringifiedEncCtx.Success?
           && 0 < |client.History.GenerateDataKey|
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#onencrypt
-             //= type=implication
-             //# If the keyring calls AWS KMS GenerateDataKeys, it MUST use the
-             //# configured AWS KMS client to make the call.
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#onencrypt
+          //= type=implication
+          //# If the keyring calls AWS KMS GenerateDataKeys, it MUST use the
+          //# configured AWS KMS client to make the call.
           && Last(client.History.GenerateDataKey).input
              //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#onencrypt
              //= type=implication
@@ -228,12 +228,12 @@ module AwsKmsKeyring {
           && KMS.IsValid_CiphertextType(maybeProviderWrappedMaterial.value)
           && |client.History.GenerateDataKey| > 0
           && Last(client.History.GenerateDataKey).output.Success?
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#onencrypt
-             //= type=implication
-             //# If the Generate Data Key call succeeds, OnEncrypt MUST verify that
-             //# the response `Plaintext` length matches the specification of the
-             //# [algorithm suite](../algorithm-suites.md)'s Key Derivation Input
-             //# Length field.
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#onencrypt
+          //= type=implication
+          //# If the Generate Data Key call succeeds, OnEncrypt MUST verify that
+          //# the response `Plaintext` length matches the specification of the
+          //# [algorithm suite](../algorithm-suites.md)'s Key Derivation Input
+          //# Length field.
           && AlgorithmSuites.GetEncryptKeyLength(algSuite) as int == |res.value.materials.plaintextDataKey.value|
           && (
                exists returnedKeyId, kmsPlaintext
@@ -245,8 +245,8 @@ module AwsKmsKeyring {
                               Plaintext := Some(kmsPlaintext))
                       && (res.value.materials.algorithmSuite.edkWrapping.DIRECT_KEY_WRAPPING?
                           ==> kmsPlaintext == res.value.materials.plaintextDataKey.value)
-                         // If using Intermediate Key wrapping, the plaintext will either be
-                         // the intermediate key, or the input pdk
+                      // If using Intermediate Key wrapping, the plaintext will either be
+                      // the intermediate key, or the input pdk
                     )
              )
 
@@ -265,10 +265,10 @@ module AwsKmsKeyring {
           && StringifyEncryptionContext(input.materials.encryptionContext).Success?
           && var stringifiedEncCtx := StringifyEncryptionContext(input.materials.encryptionContext).Extract();
           && 0 < |client.History.Encrypt|
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#onencrypt
-             //= type=implication
-             //# The keyring MUST call [AWS KMS Encrypt]
-             //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Encrypt.html) using the configured AWS KMS client.
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#onencrypt
+          //= type=implication
+          //# The keyring MUST call [AWS KMS Encrypt]
+          //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Encrypt.html) using the configured AWS KMS client.
           && Last(client.History.Encrypt).input
              //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#onencrypt
              //= type=implication
@@ -447,13 +447,13 @@ module AwsKmsKeyring {
           && var maybeStringifiedEncCtx := StringifyEncryptionContext(input.materials.encryptionContext);
           && maybeStringifiedEncCtx.Success?
           && 0 < |client.History.Decrypt|
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-             //= type=implication
-             //# - The length of the response’s `Plaintext` MUST equal the
-             //# [key derivation input length](../algorithm-suites.md#key-derivation-input-length)
-             //# specified by the [algorithm suite](../algorithm-suites.md)
-             //# included in the input [decryption materials]
-             //# (../structures.md#decryption-materials).
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+          //= type=implication
+          //# - The length of the response’s `Plaintext` MUST equal the
+          //# [key derivation input length](../algorithm-suites.md#key-derivation-input-length)
+          //# specified by the [algorithm suite](../algorithm-suites.md)
+          //# included in the input [decryption materials]
+          //# (../structures.md#decryption-materials).
           && AlgorithmSuites.GetEncryptKeyLength(input.materials.algorithmSuite) as nat == |res.value.materials.plaintextDataKey.value|
           && var LastDecrypt := Last(client.History.Decrypt);
           && LastDecrypt.output.Success?
@@ -470,12 +470,12 @@ module AwsKmsKeyring {
                    && maybeWrappedMaterial.Success?
                    && edk.keyProviderId == PROVIDER_ID
                    && KMS.IsValid_CiphertextType(maybeWrappedMaterial.value)
-                      //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-                      //= type=implication
-                      //# When calling [AWS KMS Decrypt]
-                      //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html),
-                      //# the keyring MUST call with a request constructed
-                      //# as follows:
+                   //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+                   //= type=implication
+                   //# When calling [AWS KMS Decrypt]
+                   //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html),
+                   //# the keyring MUST call with a request constructed
+                   //# as follows:
                    && KMS.DecryptRequest(
                         //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
                         //= type=implication
@@ -506,16 +506,16 @@ module AwsKmsKeyring {
                       //# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html)
                       //# with the configured AWS KMS client.
                       == LastDecrypt.input
-                      //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-                      //= type=implication
-                      //# - The `KeyId` field in the response MUST equal the configured AWS
-                      //# KMS key identifier.
+                   //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+                   //= type=implication
+                   //# - The `KeyId` field in the response MUST equal the configured AWS
+                   //# KMS key identifier.
                    && LastDecrypt.output.value.KeyId == Some(awsKmsKey)
              )
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
-             //= type=implication
-             //# - MUST immediately return the modified [decryption materials]
-             //# (../structures.md#decryption-materials).
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-keyring.md#ondecrypt
+          //= type=implication
+          //# - MUST immediately return the modified [decryption materials]
+          //# (../structures.md#decryption-materials).
           && (
                input.materials.algorithmSuite.edkWrapping.DIRECT_KEY_WRAPPING?
                ==>
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy
index 96a5bd6eed..790077bf7c 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkDiscoveryKeyring.dfy
@@ -218,9 +218,9 @@ module AwsKmsMrkDiscoveryKeyring {
                    EdkWrapping.GetProviderWrappedMaterial(edk.ciphertext, output.value.materials.algorithmSuite);
                  && maybeProviderWrappedMaterial.Success?
                  && KMS.IsValid_CiphertextType(maybeProviderWrappedMaterial.value)
-                    //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-discovery-keyring.md#ondecrypt
-                    //= type=implication
-                    //# - Its provider ID MUST exactly match the value “aws-kms”.
+                 //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-discovery-keyring.md#ondecrypt
+                 //= type=implication
+                 //# - Its provider ID MUST exactly match the value “aws-kms”.
                  && edk.keyProviderId == PROVIDER_ID
                  && KMS.IsValid_KeyIdType(awsKmsKey)
                  && var request := KMS.DecryptRequest(
@@ -478,8 +478,8 @@ module AwsKmsMrkDiscoveryKeyring {
       && res.Success?
       ==>
         && Invariant()
-           // Confirm that the materials we're about to output are a valid transition
-           // from the input materials
+        // Confirm that the materials we're about to output are a valid transition
+        // from the input materials
         && Materials.DecryptionMaterialsTransitionIsValid(materials, res.value)
 
         // Confirm that all our input values were valid
@@ -493,8 +493,8 @@ module AwsKmsMrkDiscoveryKeyring {
         && maybeStringifiedEncCtx.Success?
 
         && 0 < |client.History.Decrypt|
-           // Confirm that we called KMS in the right way and correctly returned the values
-           // it gave us
+        // Confirm that we called KMS in the right way and correctly returned the values
+        // it gave us
         && KMS.DecryptRequest(
              KeyId := Some(keyArn),
              CiphertextBlob := maybeProviderWrappedMaterial.value,
@@ -593,10 +593,10 @@ module AwsKmsMrkDiscoveryKeyring {
         //# - If a discovery filter is configured, its partition and the
         //# provider info partition MUST match.
         && discoveryFilter.value.partition == arn.partition
-           //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-discovery-keyring.md#ondecrypt
-           //= type=implication
-           //# - If a discovery filter is configured, its set of accounts MUST
-           //# contain the provider info account.
+        //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-discovery-keyring.md#ondecrypt
+        //= type=implication
+        //# - If a discovery filter is configured, its set of accounts MUST
+        //# contain the provider info account.
         && arn.account in discoveryFilter.value.accountIds
     //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-discovery-keyring.md#ondecrypt
     //= type=implication
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy
index 6ccb57c327..b70a86372b 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/AwsKmsMrkKeyring.dfy
@@ -154,10 +154,10 @@ module AwsKmsMrkKeyring {
           && var maybeStringifiedEncCtx := StringifyEncryptionContext(input.materials.encryptionContext);
           && maybeStringifiedEncCtx.Success?
           && 0 < |client.History.GenerateDataKey|
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
-             //= type=implication
-             //# If the keyring calls AWS KMS GenerateDataKeys, it MUST use the
-             //# configured AWS KMS client to make the call.
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
+          //= type=implication
+          //# If the keyring calls AWS KMS GenerateDataKeys, it MUST use the
+          //# configured AWS KMS client to make the call.
           && Last(client.History.GenerateDataKey).input
              //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
              //= type=implication
@@ -203,12 +203,12 @@ module AwsKmsMrkKeyring {
           && GenerateResponse.CiphertextBlob.Some?
           && GenerateResponse.KeyId.Some?
           && UTF8.Encode(GenerateResponse.KeyId.value).Success?
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
-             //= type=implication
-             //# If verified, OnEncrypt MUST do the following with the response
-             //# from [AWS KMS GenerateDataKey]
-             //# (https://docs.aws.amazon.com/kms/latest/APIReference/
-             //# API_GenerateDataKey.html):
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
+          //= type=implication
+          //# If verified, OnEncrypt MUST do the following with the response
+          //# from [AWS KMS GenerateDataKey]
+          //# (https://docs.aws.amazon.com/kms/latest/APIReference/
+          //# API_GenerateDataKey.html):
           && |output.value.materials.encryptedDataKeys| == |input.materials.encryptedDataKeys| + 1
           && KMS.IsValid_CiphertextType(Last(output.value.materials.encryptedDataKeys).ciphertext)
           && Last(output.value.materials.encryptedDataKeys).ciphertext
@@ -240,10 +240,10 @@ module AwsKmsMrkKeyring {
           && var maybeStringifiedEncCtx := StringifyEncryptionContext(input.materials.encryptionContext);
           && maybeStringifiedEncCtx.Success?
           && 0 < |client.History.Encrypt|
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
-             //= type=implication
-             //# The keyring MUST call [AWS KMS Encrypt]
-             //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Encrypt.html) using the configured AWS KMS client.
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
+          //= type=implication
+          //# The keyring MUST call [AWS KMS Encrypt]
+          //# (https://docs.aws.amazon.com/kms/latest/APIReference/API_Encrypt.html) using the configured AWS KMS client.
           && Last(client.History.Encrypt).input
              //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
              //= type=implication
@@ -271,12 +271,12 @@ module AwsKmsMrkKeyring {
           && EncryptResponse.CiphertextBlob.Some?
           && EncryptResponse.KeyId.Some?
           && UTF8.Encode(EncryptResponse.KeyId.value).Success?
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
-             //= type=implication
-             //# If verified, OnEncrypt MUST do the following with the
-             //# response from [AWS KMS Encrypt]
-             //# (https://docs.aws.amazon.com/kms/latest/APIReference/
-             //# API_Encrypt.html):
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#onencrypt
+          //= type=implication
+          //# If verified, OnEncrypt MUST do the following with the
+          //# response from [AWS KMS Encrypt]
+          //# (https://docs.aws.amazon.com/kms/latest/APIReference/
+          //# API_Encrypt.html):
           && |output.value.materials.encryptedDataKeys| == |input.materials.encryptedDataKeys| + 1
           && Last(output.value.materials.encryptedDataKeys).ciphertext
              == EncryptResponse.CiphertextBlob.value
@@ -454,13 +454,13 @@ module AwsKmsMrkKeyring {
           && var maybeStringifiedEncCtx := StringifyEncryptionContext(input.materials.encryptionContext);
           && maybeStringifiedEncCtx.Success?
           && 0 < |client.History.Decrypt|
-             //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#ondecrypt
-             //= type=implication
-             //# - The length of the response’s `Plaintext` MUST equal the [key
-             //# derivation input length](../algorithm-suites.md#key-derivation-
-             //# input-length) specified by the [algorithm suite](../algorithm-
-             //# suites.md) included in the input [decryption materials]
-             //# (../structures.md#decryption-materials).
+          //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#ondecrypt
+          //= type=implication
+          //# - The length of the response’s `Plaintext` MUST equal the [key
+          //# derivation input length](../algorithm-suites.md#key-derivation-
+          //# input-length) specified by the [algorithm suite](../algorithm-
+          //# suites.md) included in the input [decryption materials]
+          //# (../structures.md#decryption-materials).
           && var suite := input.materials.algorithmSuite;
           && AlgorithmSuites.GetEncryptKeyLength(suite) as nat == |output.value.materials.plaintextDataKey.value|
           && var LastDecrypt := Last(client.History.Decrypt);
@@ -476,10 +476,10 @@ module AwsKmsMrkKeyring {
                  && maybeWrappedMaterial.Success?
                  && edk.keyProviderId == PROVIDER_ID
                  && KMS.IsValid_CiphertextType(maybeWrappedMaterial.value)
-                    //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#ondecrypt
-                    //= type=implication
-                    //# When calling [AWS KMS Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html),
-                    //# the keyring MUST call with a request constructed as follows:
+                 //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#ondecrypt
+                 //= type=implication
+                 //# When calling [AWS KMS Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html),
+                 //# the keyring MUST call with a request constructed as follows:
                  && KMS.DecryptRequest(
                       KeyId := Some(awsKmsKey),
                       CiphertextBlob := maybeWrappedMaterial.value,
@@ -494,10 +494,10 @@ module AwsKmsMrkKeyring {
                     //# Decrypt](https://docs.aws.amazon.com/kms/latest/APIReference/API_Decrypt.html)
                     //# with the configured AWS KMS client.
                     == LastDecrypt.input
-                    //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#ondecrypt
-                    //= type=implication
-                    //# - The `KeyId` field in the response MUST equal the configured AWS
-                    //# KMS key identifier.
+                 //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-keyring.md#ondecrypt
+                 //= type=implication
+                 //# - The `KeyId` field in the response MUST equal the configured AWS
+                 //# KMS key identifier.
                  && LastDecrypt.output.value.KeyId == Some(awsKmsKey)
                  && (
                       input.materials.algorithmSuite.edkWrapping.DIRECT_KEY_WRAPPING?
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/DiscoveryMultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/DiscoveryMultiKeyring.dfy
index 4449630c47..e5e9d3c705 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/DiscoveryMultiKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/DiscoveryMultiKeyring.dfy
@@ -54,11 +54,11 @@ module DiscoveryMultiKeyring {
       //= type=implication
       //# If an empty set of Region is provided this function MUST fail.
       || |regions| == 0
-         //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-multi-keyrings.md#aws-kms-discovery-multi-keyring
-         //= type=implication
-         //# If
-         //# any element of the set of regions is null or an empty string this
-         //# function MUST fail.
+      //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-multi-keyrings.md#aws-kms-discovery-multi-keyring
+      //= type=implication
+      //# If
+      //# any element of the set of regions is null or an empty string this
+      //# function MUST fail.
       || (exists r | r in regions :: r == "")
       ==>
         output.Failure?
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareDiscoveryMultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareDiscoveryMultiKeyring.dfy
index 93e5583104..3493440bdc 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareDiscoveryMultiKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareDiscoveryMultiKeyring.dfy
@@ -53,11 +53,11 @@ module MrkAwareDiscoveryMultiKeyring {
       //= type=implication
       //# If an empty set of Region is provided this function MUST fail.
       || |regions| == 0
-         //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-multi-keyrings.md#aws-kms-mrk-discovery-multi-keyring
-         //= type=implication
-         //# If
-         //# any element of the set of regions is null or an empty string this
-         //# function MUST fail.
+      //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-multi-keyrings.md#aws-kms-mrk-discovery-multi-keyring
+      //= type=implication
+      //# If
+      //# any element of the set of regions is null or an empty string this
+      //# function MUST fail.
       || (exists r | r in regions :: r == "")
       ==>
         output.Failure?
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy
index b49713c182..f6956a9563 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/MrkAwareStrictMultiKeyring.dfy
@@ -92,11 +92,11 @@ module MrkAwareStrictMultiKeyring {
         && (generator.None?
             ==>
               && output.value.generatorKeyring.None?)
-           //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-multi-keyrings.md#aws-kms-mrk-multi-keyring
-           //= type=implication
-           //# If there is a set of child identifiers then a set of [AWS KMS MRK
-           //# Keyring](aws-kms-mrk-keyring.md) MUST be created for each AWS KMS key
-           //# identifier by initialized each keyring with
+        //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-mrk-multi-keyrings.md#aws-kms-mrk-multi-keyring
+        //= type=implication
+        //# If there is a set of child identifiers then a set of [AWS KMS MRK
+        //# Keyring](aws-kms-mrk-keyring.md) MUST be created for each AWS KMS key
+        //# identifier by initialized each keyring with
         && (awsKmsKeys.Some?
             ==>
               && |awsKmsKeys.value| == |output.value.childKeyrings|
@@ -107,7 +107,7 @@ module MrkAwareStrictMultiKeyring {
                    && var awsKmsChild := childKeyring as AwsKmsMrkKeyring.AwsKmsMrkKeyring;
                    // AWS KMS key identifier
                    && awsKmsChild.awsKmsKey == awsKmsKeys.value[index]
-                      // The input list of AWS KMS grant tokens
+                   // The input list of AWS KMS grant tokens
                    && (grantTokens.Some? ==> awsKmsChild.grantTokens == grantTokens.value))
         && (awsKmsKeys.None?
             ==>
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy
index 83ce36389d..06065f7dc0 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/AwsKms/StrictMultiKeyring.dfy
@@ -85,11 +85,11 @@ module StrictMultiKeyring {
         && (generator.None?
             ==>
               && output.value.generatorKeyring.None?)
-           //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-multi-keyrings.md#aws-kms-multi-keyring
-           //= type=implication
-           //# If there is a set of child identifiers then a set of [AWS KMS Keyring]
-           //# (aws-kms-keyring.md) MUST be created for each AWS KMS key identifier
-           //# by initializing each keyring with
+        //= aws-encryption-sdk-specification/framework/aws-kms/aws-kms-multi-keyrings.md#aws-kms-multi-keyring
+        //= type=implication
+        //# If there is a set of child identifiers then a set of [AWS KMS Keyring]
+        //# (aws-kms-keyring.md) MUST be created for each AWS KMS key identifier
+        //# by initializing each keyring with
         && (awsKmsKeys.Some?
             ==>
               && |awsKmsKeys.value| == |output.value.childKeyrings|
@@ -100,7 +100,7 @@ module StrictMultiKeyring {
                    && var awsKmsChild := childKeyring as AwsKmsKeyring.AwsKmsKeyring;
                    // AWS KMS key identifier
                    && awsKmsChild.awsKmsKey == awsKmsKeys.value[index]
-                      // The input list of AWS KMS grant tokens
+                   // The input list of AWS KMS grant tokens
                    && (grantTokens.Some? ==> awsKmsChild.grantTokens == grantTokens.value))
         && (awsKmsKeys.None?
             ==>
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy
index 8cac0c59f9..cd4cf4aaa2 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/MultiKeyring.dfy
@@ -255,9 +255,9 @@ module {:options "-functionSyntax:4"} MultiKeyring {
             || Verified?(generatorKeyring.value)
             || generatorKeyring.value is MultiKeyring
           ) {
-          //= aws-encryption-sdk-specification/framework/multi-keyring.md#onencrypt
-          //# - If the generator keyring returns encryption materials missing a
-          //# plaintext data key, OnEncrypt MUST fail.
+            //= aws-encryption-sdk-specification/framework/multi-keyring.md#onencrypt
+            //# - If the generator keyring returns encryption materials missing a
+            //# plaintext data key, OnEncrypt MUST fail.
           :- Need(
             Materials.EncryptionMaterialsHasPlaintextDataKey(onEncryptOutput.value.materials),
             Types.AwsCryptographicMaterialProvidersException(
@@ -303,11 +303,11 @@ module {:options "-functionSyntax:4"} MultiKeyring {
             || Verified?(child)
             || child is MultiKeyring
           ) {
-          // We have to explicitly check for this because our child and generator keyrings are of type
-          // IKeyring, rather than VerifiableKeyring.
-          // If we knew we would always have VerifiableKeyrings, we would get this for free.
-          // However, we want to support customer implementations of keyrings which may or may
-          // not perform valid transitions.
+            // We have to explicitly check for this because our child and generator keyrings are of type
+            // IKeyring, rather than VerifiableKeyring.
+            // If we knew we would always have VerifiableKeyrings, we would get this for free.
+            // However, we want to support customer implementations of keyrings which may or may
+            // not perform valid transitions.
 
           :- Need(
             Materials.EncryptionMaterialsHasPlaintextDataKey(onEncryptOutput.value.materials),
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy
index 624741c0f8..3d65cd2512 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Keyrings/RawAESKeyring.dfy
@@ -414,20 +414,20 @@ module RawAESKeyring {
       SequenceIsSafeBecauseItIsInMemory(keyName);
       var keyname_size := |keyName| as uint64;
       && |info| as uint64 == Add4(keyname_size, AUTH_TAG_LEN_LEN as uint64, IV_LEN_LEN as uint64, wrappingAlgorithm.ivLength as uint64)
-         // The key name obtained from the encrypted data key's key provider information has a value equal to this keyring's key name.
+      // The key name obtained from the encrypted data key's key provider information has a value equal to this keyring's key name.
       && info[..keyname_size] == keyName
-         //= aws-encryption-sdk-specification/framework/raw-aes-keyring.md#authentication-tag-length
-         //= type=implication
-         //# This value MUST match the authentication tag length of the keyring's
-         //# configured wrapping algorithm
+      //= aws-encryption-sdk-specification/framework/raw-aes-keyring.md#authentication-tag-length
+      //= type=implication
+      //# This value MUST match the authentication tag length of the keyring's
+      //# configured wrapping algorithm
 
       && SeqToUInt32(info[keyname_size..keyname_size + AUTH_TAG_LEN_LEN as uint64]) == 128
       && 128 == wrappingAlgorithm.tagLength as uint32 * 8
       && SeqToUInt32(info[keyname_size + AUTH_TAG_LEN_LEN as uint64 .. keyname_size + AUTH_TAG_LEN_LEN as uint64 + IV_LEN_LEN as uint64]) == wrappingAlgorithm.ivLength as uint32
-         //= aws-encryption-sdk-specification/framework/raw-aes-keyring.md#iv-length
-         //= type=implication
-         //# This value MUST match the IV length of the keyring's
-         //# configured wrapping algorithm
+      //= aws-encryption-sdk-specification/framework/raw-aes-keyring.md#iv-length
+      //= type=implication
+      //# This value MUST match the IV length of the keyring's
+      //# configured wrapping algorithm
       && SeqToUInt32(info[keyname_size + AUTH_TAG_LEN_LEN as uint64 .. keyname_size + AUTH_TAG_LEN_LEN as uint64 + IV_LEN_LEN as uint64]) == 12
     }
 
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Materials.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Materials.dfy
index b221e1b4f2..bc3079fa35 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Materials.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/src/Materials.dfy
@@ -38,11 +38,11 @@ module Materials {
         && var suite := AS.GetSuite(input.algorithmSuiteId);
         && res.value.algorithmSuite == suite
         && (!suite.signature.None? <==> EC_PUBLIC_KEY_FIELD in res.value.encryptionContext)
-           //= aws-encryption-sdk-specification/framework/structures.md#signing-key
-           //= type=implication
-           //# If the
-           //# algorithm suite does not contain an asymmetric signing algorithm, the signing key
-           //# MUST NOT be present.
+        //= aws-encryption-sdk-specification/framework/structures.md#signing-key
+        //= type=implication
+        //# If the
+        //# algorithm suite does not contain an asymmetric signing algorithm, the signing key
+        //# MUST NOT be present.
         && (suite.signature.None? <==> res.value.signingKey.None?)
     //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-1
     //= type=implication
@@ -101,11 +101,11 @@ module Materials {
         && var suite := AS.GetSuite(input.algorithmSuiteId);
         && res.value.algorithmSuite == suite
         && (suite.signature.None? <==> EC_PUBLIC_KEY_FIELD !in input.encryptionContext)
-           //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-2
-           //= type=implication
-           //# The mapped value
-           //# from the reserved key `aws-crypto-public-key` SHOULD be the signature
-           //# verification key stored on the [decryption materials](#decryption-materials).
+        //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-2
+        //= type=implication
+        //# The mapped value
+        //# from the reserved key `aws-crypto-public-key` SHOULD be the signature
+        //# verification key stored on the [decryption materials](#decryption-materials).
         && var verificationKey := DecodeVerificationKey(input.encryptionContext);
         && (
           verificationKey.Success? && verificationKey.value.Some?
@@ -221,30 +221,30 @@ module Materials {
     && AS.AlgorithmSuite?(encryptionMaterials.algorithmSuite)
     && var suite := encryptionMaterials.algorithmSuite;
     && (suite.signature.None? <==> encryptionMaterials.signingKey.None?)
-       //= aws-encryption-sdk-specification/framework/structures.md#plaintext-data-key
-       //= type=implication
-       //# The plaintext data key MUST:
-       //# - Fit the specification for the [key derivation algorithm](algorithm-
-       //#   suites.md#key-derivation-algorithm) included in this decryption
-       //#   material's [algorithm suite](#algorithm-suite).
+    //= aws-encryption-sdk-specification/framework/structures.md#plaintext-data-key
+    //= type=implication
+    //# The plaintext data key MUST:
+    //# - Fit the specification for the [key derivation algorithm](algorithm-
+    //#   suites.md#key-derivation-algorithm) included in this decryption
+    //#   material's [algorithm suite](#algorithm-suite).
     && (encryptionMaterials.plaintextDataKey.Some? ==> AS.GetEncryptKeyLength(suite) as uint64 == |encryptionMaterials.plaintextDataKey.value| as uint64)
-       //= aws-encryption-sdk-specification/framework/structures.md#encrypted-data-keys
-       //= type=implication
-       //# If the plaintext data key is not included in this set of encryption
-       //# materials, this list MUST be empty.
+    //= aws-encryption-sdk-specification/framework/structures.md#encrypted-data-keys
+    //= type=implication
+    //# If the plaintext data key is not included in this set of encryption
+    //# materials, this list MUST be empty.
     && (encryptionMaterials.plaintextDataKey.None? ==> |encryptionMaterials.encryptedDataKeys| as uint64 == 0)
-       //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-1
-       //= type=implication
-       //# If an [encryption material](#encryption-materials) contains a [signing key]
-       //# (#signing-key), the [encryption context](#encryption-context) SHOULD
-       //# include the reserved key `aws-crypto-public-key`.
-       //
-       //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-1
-       //= type=implication
-       //# If an [encryption
-       //# material](#encryption-materials) does not contains a [signing key]
-       //# (#signing-key), the [encryption context](#encryption-context) SHOULD
-       //# NOT include the reserved key `aws-crypto-public-key`.
+    //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-1
+    //= type=implication
+    //# If an [encryption material](#encryption-materials) contains a [signing key]
+    //# (#signing-key), the [encryption context](#encryption-context) SHOULD
+    //# include the reserved key `aws-crypto-public-key`.
+    //
+    //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-1
+    //= type=implication
+    //# If an [encryption
+    //# material](#encryption-materials) does not contains a [signing key]
+    //# (#signing-key), the [encryption context](#encryption-context) SHOULD
+    //# NOT include the reserved key `aws-crypto-public-key`.
     && (!suite.signature.None? <==> EC_PUBLIC_KEY_FIELD in encryptionMaterials.encryptionContext)
 
     //= aws-encryption-sdk-specification/framework/structures.md#signing-key
@@ -256,17 +256,17 @@ module Materials {
     // But at this time existence is deemed acceptable.
     && (suite.signature.ECDSA? <==> encryptionMaterials.signingKey.Some?)
     && (!suite.signature.None? <==> EC_PUBLIC_KEY_FIELD in encryptionMaterials.encryptionContext)
-       //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-keys
-       //= type=implication
-       //# If the algorithm suite does contain a symmetric signing algorithm, this list MUST have length equal to the [encrypted data key list](#encrypted-data-keys).
+    //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-keys
+    //= type=implication
+    //# If the algorithm suite does contain a symmetric signing algorithm, this list MUST have length equal to the [encrypted data key list](#encrypted-data-keys).
     && (suite.symmetricSignature.HMAC? && encryptionMaterials.symmetricSigningKeys.Some? ==>
           |encryptionMaterials.symmetricSigningKeys.value| as uint64 == |encryptionMaterials.encryptedDataKeys| as uint64)
     && (suite.symmetricSignature.HMAC? ==>
           || encryptionMaterials.symmetricSigningKeys.Some?
           || (|encryptionMaterials.encryptedDataKeys| as uint64 == 0 && encryptionMaterials.symmetricSigningKeys.None?))
-       //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-keys
-       //= type=implication
-       //# If the algorithm suite does not contain a symmetric signing algorithm, this list MUST NOT be included in the materials.
+    //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-keys
+    //= type=implication
+    //# If the algorithm suite does not contain a symmetric signing algorithm, this list MUST NOT be included in the materials.
     && (suite.symmetricSignature.None? ==> encryptionMaterials.symmetricSigningKeys.None?)
 
     //= aws-encryption-sdk-specification/framework/structures.md#required-encryption-context-keys
@@ -436,18 +436,18 @@ module Materials {
     //# suites.md#encryption-algorithm)  included in this decryption
     //# material's [algorithm suite](#algorithm-suite-1).
     && (decryptionMaterials.plaintextDataKey.Some? ==> AS.GetEncryptKeyLength(suite) as uint64 == |decryptionMaterials.plaintextDataKey.value| as uint64)
-       //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-2
-       //= type=implication
-       //# If a [decryption materials](#decryption-materials) contains a [verification key]
-       //# (#verification-key), the [encryption context](#encryption-context) SHOULD
-       //# include the reserved key `aws-crypto-public-key`.
-       //
-       //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-2
-       //= type=implication
-       //# If a [decryption materials](#decryption-materials) does not contain a
-       //# [verification key](#verification-key), the [encryption context]
-       //# (#encryption-context) SHOULD NOT include the reserved key `aws-crypto-
-       //# public-key`.
+    //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-2
+    //= type=implication
+    //# If a [decryption materials](#decryption-materials) contains a [verification key]
+    //# (#verification-key), the [encryption context](#encryption-context) SHOULD
+    //# include the reserved key `aws-crypto-public-key`.
+    //
+    //= aws-encryption-sdk-specification/framework/structures.md#encryption-context-2
+    //= type=implication
+    //# If a [decryption materials](#decryption-materials) does not contain a
+    //# [verification key](#verification-key), the [encryption context]
+    //# (#encryption-context) SHOULD NOT include the reserved key `aws-crypto-
+    //# public-key`.
     && (!suite.signature.None? <==> EC_PUBLIC_KEY_FIELD in decryptionMaterials.encryptionContext)
 
     //= aws-encryption-sdk-specification/framework/structures.md#verification-key
@@ -459,16 +459,16 @@ module Materials {
     // But at this time existence is deemed acceptable.
     && (suite.signature.ECDSA? <==> decryptionMaterials.verificationKey.Some?)
     && (!suite.signature.None? <==> EC_PUBLIC_KEY_FIELD in decryptionMaterials.encryptionContext)
-       //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-key
-       //= type=implication
-       //# If the algorithm suite does contain a symmetric signing algorithm,
-       //# the symmetric signing key MUST also be included in the materials
-       //# if and only if the materials also include a [plaintext data key](#plaintext-data-key-1).
+    //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-key
+    //= type=implication
+    //# If the algorithm suite does contain a symmetric signing algorithm,
+    //# the symmetric signing key MUST also be included in the materials
+    //# if and only if the materials also include a [plaintext data key](#plaintext-data-key-1).
     && (!suite.symmetricSignature.None? ==> (decryptionMaterials.plaintextDataKey.Some? <==> decryptionMaterials.symmetricSigningKey.Some?))
-       //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-key
-       //= type=implication
-       //# If the algorithm suite does not contain a symmetric signing algorithm,
-       //# the symmetric signing key MUST NOT be included in the materials.
+    //= aws-encryption-sdk-specification/framework/structures.md#symmetric-signing-key
+    //= type=implication
+    //# If the algorithm suite does not contain a symmetric signing algorithm,
+    //# the symmetric signing key MUST NOT be included in the materials.
     && (suite.symmetricSignature.None? ==> decryptionMaterials.symmetricSigningKey.None?)
 
     //= aws-encryption-sdk-specification/framework/structures.md#required-encryption-context-keys-1
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
index a371045798..74138cd537 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
@@ -11,7 +11,7 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
   import opened UTF8
   import ComAmazonawsDynamodbTypes
   import ComAmazonawsKmsTypes
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy
index 5b6494a233..32a1c6bb29 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/AwsCryptographyKeyStoreOperations.dfy
@@ -180,11 +180,11 @@ module AwsCryptographyKeyStoreOperations refines AbstractAwsCryptographyKeyStore
                 && i.0.Success?
                 && i.1.Success?
                 && DDB.IsValid_AttributeName(Structure.ENCRYPTION_CONTEXT_PREFIX + i.0.value)
-                   // Dafny requires that I *prove* that k == Encode(Decode(k))
-                   // Since UTF8 can be lossy in some implementations
-                   // this is the simplest...
-                   // A prove that ValidUTF8Seq(i) ==> Decode(i).Success?
-                   // would improve the situation
+                // Dafny requires that I *prove* that k == Encode(Decode(k))
+                // Since UTF8 can be lossy in some implementations
+                // this is the simplest...
+                // A prove that ValidUTF8Seq(i) ==> Decode(i).Success?
+                // would improve the situation
                 && var encoded := UTF8.Encode(i.0.value);
                 && encoded.Success?
                 && i.2 == encoded.value
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeyStoreTable.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeyStoreTable.dfy
index d0b8626b05..4f3bd77090 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeyStoreTable.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeyStoreTable.dfy
@@ -33,9 +33,9 @@ module CreateKeyStoreTable {
   type keyStoreDescription = t: DDB.TableDescription | keyStoreHasExpectedConstruction?(t) witness *
   predicate method keyStoreHasExpectedConstruction?(t: DDB.TableDescription) {
     && t.AttributeDefinitions.Some? && t.KeySchema.Some? && t.TableName.Some? && t.TableArn.Some?
-       //= aws-encryption-sdk-specification/framework/branch-key-store.md#keyschema
-       //= type=implication
-       //# The following KeySchema MUST be configured on the table:
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#keyschema
+    //= type=implication
+    //# The following KeySchema MUST be configured on the table:
     && ToSet(t.AttributeDefinitions.value) >= ToSet(ATTRIBUTE_DEFINITIONS)
     && ToSet(t.KeySchema.value) >= ToSet(KEY_SCHEMA)
   }
@@ -75,14 +75,14 @@ module CreateKeyStoreTable {
         //# - [KeySchema](#keyschema) as defined below.
         && CreateTableInput.TableName == tableName
         && CreateTableInput.KeySchema == KEY_SCHEMA
-           //= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
-           //= type=implication
-           //# If the operation fails to create table, the operation MUST fail.
+        //= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
+        //= type=implication
+        //# If the operation fails to create table, the operation MUST fail.
         && (Seq.Last(ddbClient.History.CreateTable).output.Failure? ==> res.Failure?)
-           //= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
-           //= type=implication
-           //# If the operation successfully creates a table, the operation MUST return the AWS DDB Table Arn
-           //# back to the caller.
+        //= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
+        //= type=implication
+        //# If the operation successfully creates a table, the operation MUST return the AWS DDB Table Arn
+        //# back to the caller.
         && (
              && Seq.Last(ddbClient.History.CreateTable).output.Success?
              && Seq.Last(ddbClient.History.CreateTable).output.value.TableDescription.Some?
@@ -169,11 +169,11 @@ module CreateKeyStoreTable {
         res := Failure(Types.ComAmazonawsDynamodb(error));
       }
     } else {
-      //= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
-      //# If the response is successful, this operation validates that the table has the expected
-      //# [KeySchema](#keyschema) as defined below.
-      //# If the [KeySchema](#keyschema) does not match
-      //# this operation MUST yield an error.
+        //= aws-encryption-sdk-specification/framework/branch-key-store.md#createkeystore
+        //# If the response is successful, this operation validates that the table has the expected
+        //# [KeySchema](#keyschema) as defined below.
+        //# If the [KeySchema](#keyschema) does not match
+        //# this operation MUST yield an error.
       :- Need(
         && maybeDescribeTableResponse.value.Table.Some?
         && keyStoreHasExpectedConstruction?(maybeDescribeTableResponse.value.Table.value)
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy
index 5b6a7199d3..992e1548bd 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/CreateKeys.dfy
@@ -554,11 +554,11 @@ module {:options "/functionSyntax:4" } CreateKeys {
     //= type=implication
     //# The operation MUST call [AWS KMS API GenerateDataKeyWithoutPlaintext](https://docs.aws.amazon.com/kms/latest/APIReference/API_GenerateDataKeyWithoutPlaintext.html).
     generateHistory: KMS.DafnyCallEvent<KMS.GenerateDataKeyWithoutPlaintextRequest, Result<KMS.GenerateDataKeyWithoutPlaintextResponse, KMS.Error>>,
-    reEncryptHistory: KMS.DafnyCallEvent<KMS.ReEncryptRequest, Result<KMS.ReEncryptResponse, KMS.Error>>,
-    kmsClient: KMS.IKMSClient,
-    kmsConfiguration: Types.KMSConfiguration,
-    grantTokens: KMS.GrantTokenList,
-    decryptOnlyEncryptionContext: map<string, string>
+                                                                                           reEncryptHistory: KMS.DafnyCallEvent<KMS.ReEncryptRequest, Result<KMS.ReEncryptResponse, KMS.Error>>,
+                                                                                                                                                             kmsClient: KMS.IKMSClient,
+                                                                                                                                                             kmsConfiguration: Types.KMSConfiguration,
+                                                                                                                                                             grantTokens: KMS.GrantTokenList,
+                                                                                                                                                             decryptOnlyEncryptionContext: map<string, string>
   )
     reads kmsClient.History
     requires KMSKeystoreOperations.HasKeyId(kmsConfiguration) && KmsArn.ValidKmsArn?(KMSKeystoreOperations.GetKeyId(kmsConfiguration))
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy
index 8605e8efd8..3efbb8ff4b 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/GetKeys.dfy
@@ -429,12 +429,12 @@ module GetKeys {
 
   predicate AwsKmsBranchKeyDecryption?(
     getItemHistory: DDB.DafnyCallEvent<DDB.GetItemInput, Result<DDB.GetItemOutput, DDB.Error>>,
-    decryptHistory: KMS.DafnyCallEvent<KMS.DecryptRequest, Result<KMS.DecryptResponse, KMS.Error>>,
-    kmsClient: KMS.IKMSClient,
-    ddbClient: DDB.IDynamoDBClient,
-    kmsConfiguration: Types.KMSConfiguration,
-    grantTokens: KMS.GrantTokenList,
-    logicalKeyStoreName: string
+                                                                decryptHistory: KMS.DafnyCallEvent<KMS.DecryptRequest, Result<KMS.DecryptResponse, KMS.Error>>,
+                                                                                                                              kmsClient: KMS.IKMSClient,
+                                                                                                                              ddbClient: DDB.IDynamoDBClient,
+                                                                                                                              kmsConfiguration: Types.KMSConfiguration,
+                                                                                                                              grantTokens: KMS.GrantTokenList,
+                                                                                                                              logicalKeyStoreName: string
   )
     reads kmsClient.History
     reads ddbClient.History
@@ -468,11 +468,11 @@ module GetKeys {
     //# except the logical table name
     //# MUST equal the value with the same key in the AWS DDB response item.
     && (forall k <- versionEncryptionContext.Keys - {Structure.TABLE_FIELD}
-                    // Working around https://github.com/dafny-lang/dafny/issues/4214
-                    //  that will make the following fail to compile
-                    // :: match k
-                    //    case HIERARCHY_VERSION => versionEncryptionContext[Structure.HIERARCHY_VERSION] == versionItem[Structure.HIERARCHY_VERSION].N
-                    //    case _ => versionEncryptionContext[k] == versionItem[k].S)
+          // Working around https://github.com/dafny-lang/dafny/issues/4214
+          //  that will make the following fail to compile
+          // :: match k
+          //    case HIERARCHY_VERSION => versionEncryptionContext[Structure.HIERARCHY_VERSION] == versionItem[Structure.HIERARCHY_VERSION].N
+          //    case _ => versionEncryptionContext[k] == versionItem[k].S)
           :: if k == Structure.HIERARCHY_VERSION then
                versionEncryptionContext[Structure.HIERARCHY_VERSION] == versionItem[Structure.HIERARCHY_VERSION].N
              else
@@ -507,9 +507,9 @@ module GetKeys {
 
     && var decryptRequest := decryptHistory.input;
     && decryptRequest.KeyId.Some?
-       //= aws-encryption-sdk-specification/framework/branch-key-store.md#aws-kms-branch-key-decryption
-       //= type=implication
-       //# - `KeyId`, if the KMS Configuration is Discovery, MUST be the `kms-arn` attribute value of the AWS DDB response item.
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#aws-kms-branch-key-decryption
+    //= type=implication
+    //# - `KeyId`, if the KMS Configuration is Discovery, MUST be the `kms-arn` attribute value of the AWS DDB response item.
     && (kmsConfiguration.discovery? ==> decryptRequest.KeyId == Some(versionItem[Structure.KMS_FIELD].S))
 
     //= aws-encryption-sdk-specification/framework/branch-key-store.md#aws-kms-branch-key-decryption
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
index 39a82ed937..13c47d13a8 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy
@@ -41,25 +41,25 @@ module {:options "/functionSyntax:4" } Structure {
     //= type=implication
     //# - MUST have a `branch-key-id` attribute
     && (BRANCH_KEY_IDENTIFIER_FIELD in m)
-       //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
-       //= type=implication
-       //# - MUST have a `type` attribute
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
+    //= type=implication
+    //# - MUST have a `type` attribute
     && (TYPE_FIELD in m)
-       //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
-       //= type=implication
-       //# - MUST have a `create-time` attribute
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
+    //= type=implication
+    //# - MUST have a `create-time` attribute
     && (KEY_CREATE_TIME in m)
-       //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
-       //= type=implication
-       //# - MUST have a `hierarchy-version`
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
+    //= type=implication
+    //# - MUST have a `hierarchy-version`
     && (HIERARCHY_VERSION in m)
-       //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
-       //= type=implication
-       //# - MUST have a `tablename` attribute to store the logicalKeyStoreName
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
+    //= type=implication
+    //# - MUST have a `tablename` attribute to store the logicalKeyStoreName
     && (TABLE_FIELD in m)
-       //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
-       //= type=implication
-       //# - MUST have a `kms-arn` attribute
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
+    //= type=implication
+    //# - MUST have a `kms-arn` attribute
     && (KMS_FIELD in m) && KMS.IsValid_KeyIdType(m[KMS_FIELD])
 
     //= aws-encryption-sdk-specification/framework/branch-key-store.md#authenticating-a-keystore-item
@@ -74,9 +74,9 @@ module {:options "/functionSyntax:4" } Structure {
     //= type=implication
     //# - The `branch-key-id` field MUST not be an empty string
     && (SequenceIsSafeBecauseItIsInMemory(m[BRANCH_KEY_IDENTIFIER_FIELD]); 0 < |m[BRANCH_KEY_IDENTIFIER_FIELD]| as uint64)
-       //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
-       //= type=implication
-       //# - The `type` field MUST not be an empty string
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#encryption-context
+    //= type=implication
+    //# - The `type` field MUST not be an empty string
     && (SequenceIsSafeBecauseItIsInMemory(m[TYPE_FIELD]); 0 < |m[TYPE_FIELD]| as uint64)
 
     && (forall k <- m.Keys :: DDB.IsValid_AttributeName(k))
@@ -86,9 +86,9 @@ module {:options "/functionSyntax:4" } Structure {
     //# The ACTIVE encryption context MUST have a `version` attribute.
     && (BRANCH_KEY_ACTIVE_VERSION_FIELD in m <==>
         && m[TYPE_FIELD] == BRANCH_KEY_ACTIVE_TYPE)
-       //= aws-encryption-sdk-specification/framework/branch-key-store.md#active-encryption-context
-       //= type=implication
-       //# The ACTIVE encryption context value of the `type` attribute MUST equal to `"branch:ACTIVE"`.
+    //= aws-encryption-sdk-specification/framework/branch-key-store.md#active-encryption-context
+    //= type=implication
+    //# The ACTIVE encryption context value of the `type` attribute MUST equal to `"branch:ACTIVE"`.
     && (BRANCH_KEY_ACTIVE_VERSION_FIELD in m ==>
           //= aws-encryption-sdk-specification/framework/branch-key-store.md#active-encryption-context
           //= type=implication
@@ -107,9 +107,9 @@ module {:options "/functionSyntax:4" } Structure {
         //= type=implication
         //# The Beacon key encryption context value of the `type` attribute MUST equal to `"beacon:ACTIVE"`.
         || m[TYPE_FIELD] == BEACON_KEY_TYPE_VALUE
-           //= aws-encryption-sdk-specification/framework/branch-key-store.md#decrypt-only-encryption-context
-           //= type=implication
-           //# The `type` attribute MUST stores the branch key version formatted like `"branch:version:"` + `version`.
+        //= aws-encryption-sdk-specification/framework/branch-key-store.md#decrypt-only-encryption-context
+        //= type=implication
+        //# The `type` attribute MUST stores the branch key version formatted like `"branch:version:"` + `version`.
         || BRANCH_KEY_TYPE_PREFIX < m[TYPE_FIELD])
   }
 
@@ -124,12 +124,12 @@ module {:options "/functionSyntax:4" } Structure {
     ensures ToBranchKeyContext(output, encryptionContext[TABLE_FIELD]) == encryptionContext
   {
     map k <- encryptionContext.Keys + {BRANCH_KEY_FIELD} - {TABLE_FIELD}
-             // Working around https://github.com/dafny-lang/dafny/issues/4214
-             //  that will make the following fail to compile
-             // ::  match k
-             // case HIERARCHY_VERSION => DDB.AttributeValue.N(encryptionContext[HIERARCHY_VERSION])
-             // case BRANCH_KEY_FIELD => DDB.AttributeValue.B(encryptedKey)
-             // case _ => DDB.AttributeValue.S(encryptionContext[k])
+      // Working around https://github.com/dafny-lang/dafny/issues/4214
+      //  that will make the following fail to compile
+      // ::  match k
+      // case HIERARCHY_VERSION => DDB.AttributeValue.N(encryptionContext[HIERARCHY_VERSION])
+      // case BRANCH_KEY_FIELD => DDB.AttributeValue.B(encryptedKey)
+      // case _ => DDB.AttributeValue.S(encryptionContext[k])
       :: k := if k == HIERARCHY_VERSION then
         DDB.AttributeValue.N(encryptionContext[HIERARCHY_VERSION])
       else if k == BRANCH_KEY_FIELD then
@@ -145,12 +145,12 @@ module {:options "/functionSyntax:4" } Structure {
     requires BranchKeyItem?(item)
   {
     map k <- item.Keys - {BRANCH_KEY_FIELD} + {TABLE_FIELD}
-             // Working around https://github.com/dafny-lang/dafny/issues/4214
-             //  that will make the following fail to compile
-             // match k
-             // case HIERARCHY_VERSION => item[k].N
-             // case TABLE_FIELD => logicalKeyStoreName
-             // case _ => item[k].S
+      // Working around https://github.com/dafny-lang/dafny/issues/4214
+      //  that will make the following fail to compile
+      // match k
+      // case HIERARCHY_VERSION => item[k].N
+      // case TABLE_FIELD => logicalKeyStoreName
+      // case _ => item[k].S
       :: k := if k == HIERARCHY_VERSION then
         item[k].N
       else if k == TABLE_FIELD then
@@ -177,9 +177,9 @@ module {:options "/functionSyntax:4" } Structure {
               //= type=implication
               //# - [Branch Key](./structures.md#branch-key) MUST be the [decrypted branch key material](#aws-kms-branch-key-decryption)
               && output.value.branchKey == plaintextKey
-                 //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-materials-from-authenticated-encryption-context
-                 //= type=implication
-                 //# - [Branch Key Id](./structures.md#branch-key-id) MUST be the `branch-key-id`
+              //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-materials-from-authenticated-encryption-context
+              //= type=implication
+              //# - [Branch Key Id](./structures.md#branch-key-id) MUST be the `branch-key-id`
               && output.value.branchKeyIdentifier == encryptionContext[BRANCH_KEY_IDENTIFIER_FIELD]
 
               && var versionInformation
@@ -201,9 +201,9 @@ module {:options "/functionSyntax:4" } Structure {
               //# The version string MUST start with `branch:version:`.
               && BRANCH_KEY_TYPE_PREFIX < versionInformation
               && UTF8.Encode(versionInformation[|BRANCH_KEY_TYPE_PREFIX|..]).Success?
-                 //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-materials-from-authenticated-encryption-context
-                 //= type=implication
-                 //# The remaining string encoded as UTF8 bytes MUST be the Branch Key version.
+              //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-materials-from-authenticated-encryption-context
+              //= type=implication
+              //# The remaining string encoded as UTF8 bytes MUST be the Branch Key version.
               && output.value.branchKeyVersion == UTF8.Encode(versionInformation[|BRANCH_KEY_TYPE_PREFIX|..]).value
 
               //= aws-encryption-sdk-specification/framework/branch-key-store.md#branch-key-materials-from-authenticated-encryption-context
@@ -266,17 +266,17 @@ module {:options "/functionSyntax:4" } Structure {
           ::
             && UTF8.Decode(k).Success?
             && UTF8.Decode(output.value[k]).Success?
-               //= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context-from-authenticated-encryption-context
-               //= type=implication
-               //# For every key in the [encryption context](./structures.md#encryption-context-3)
-               //# the string `aws-crypto-ec:` + the UTF8 decode of this key
-               //# MUST exist as a key in the authenticated encryption context.
+            //= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context-from-authenticated-encryption-context
+            //= type=implication
+            //# For every key in the [encryption context](./structures.md#encryption-context-3)
+            //# the string `aws-crypto-ec:` + the UTF8 decode of this key
+            //# MUST exist as a key in the authenticated encryption context.
             && (ENCRYPTION_CONTEXT_PREFIX + UTF8.Decode(k).value in encryptionContext)
-               //= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context-from-authenticated-encryption-context
-               //= type=implication
-               //# Also, the value in the [encryption context](./structures.md#encryption-context-3) for this key
-               //# MUST equal the value in the authenticated encryption context
-               //# for the constructed key.
+            //= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context-from-authenticated-encryption-context
+            //= type=implication
+            //# Also, the value in the [encryption context](./structures.md#encryption-context-3) for this key
+            //# MUST equal the value in the authenticated encryption context
+            //# for the constructed key.
             && encryptionContext[ENCRYPTION_CONTEXT_PREFIX + UTF8.Decode(k).value] == UTF8.Decode(output.value[k]).value
   {
     // Get all keys that start with the prefix OR are the prefix
@@ -549,10 +549,10 @@ module {:options "/functionSyntax:4" } Structure {
             && decryptOnly[k] == active[k] == beacon[k]
          )
       && active[BRANCH_KEY_ACTIVE_VERSION_FIELD] == decryptOnly[TYPE_FIELD]
-         //= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context
-         //= type=implication
-         //# If custom [encryption context](./structures.md#encryption-context-3)
-         //# is associated with the branch key these values MUST be added to the AWS KMS encryption context.
+      //= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context
+      //= type=implication
+      //# If custom [encryption context](./structures.md#encryption-context-3)
+      //# is associated with the branch key these values MUST be added to the AWS KMS encryption context.
       && (forall k <- encryptionContext ::
             //= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context
             //= type=implication
@@ -561,9 +561,9 @@ module {:options "/functionSyntax:4" } Structure {
             && (ENCRYPTION_CONTEXT_PREFIX + k in decryptOnly)
             && (ENCRYPTION_CONTEXT_PREFIX + k in active)
             && (ENCRYPTION_CONTEXT_PREFIX + k in beacon)
-               //= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context
-               //= type=implication
-               //# Across all versions of a Branch Key, the custom encryption context MUST be equal.
+            //= aws-encryption-sdk-specification/framework/branch-key-store.md#custom-encryption-context
+            //= type=implication
+            //# Across all versions of a Branch Key, the custom encryption context MUST be equal.
             && encryptionContext[k]
             == decryptOnly[ENCRYPTION_CONTEXT_PREFIX + k]
             == active[ENCRYPTION_CONTEXT_PREFIX + k]
diff --git a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy
index 7714244df6..9149137f13 100644
--- a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy
+++ b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy
@@ -7,7 +7,7 @@ module {:extern "software.amazon.cryptography.primitives.internaldafny.types" }
   import opened Wrappers
   import opened StandardLibrary.UInt
   import opened UTF8
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types
diff --git a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy
index b5c3c9fe41..dc6583e076 100644
--- a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy
+++ b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy
@@ -7,7 +7,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty
   import opened Wrappers
   import opened StandardLibrary.UInt
   import opened UTF8
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types
diff --git a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy
index ff5520a289..057dade5d4 100644
--- a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy
+++ b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy
@@ -7,7 +7,7 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types"
   import opened Wrappers
   import opened StandardLibrary.UInt
   import opened UTF8
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types
diff --git a/StandardLibrary/runtimes/python/pyproject.toml b/StandardLibrary/runtimes/python/pyproject.toml
index 72d531713d..e758c983fc 100644
--- a/StandardLibrary/runtimes/python/pyproject.toml
+++ b/StandardLibrary/runtimes/python/pyproject.toml
@@ -18,7 +18,7 @@ include = [
 python = "^3.11.0"
 pytz = ">=2023.3.post1, <2026.0.0"
 # TODO: Longer-term, write something to pull this in from the project's project.properties file
-DafnyRuntimePython = "4.9.0"
+DafnyRuntimePython = "4.11.0"
 
 # Package testing
 
diff --git a/StandardLibrary/src/Actions.dfy b/StandardLibrary/src/Actions.dfy
index 536676873e..22212ddf3d 100644
--- a/StandardLibrary/src/Actions.dfy
+++ b/StandardLibrary/src/Actions.dfy
@@ -349,14 +349,14 @@ module Actions {
       if res.Success? then
         && Last(attemptsState).output.Success?
         && Last(attemptsState).output.value == res.value
-           // This is the engine that can be used to hoist proof obligations
+        // This is the engine that can be used to hoist proof obligations
         && action.Ensures(
              Last(attemptsState).input,
              Last(attemptsState).output,
              DropLast(attemptsState))
-           // Attempts are made until there is a success
-           // so attempts will be made up of failures
-           // with one final Success at the end.
+        // Attempts are made until there is a success
+        // so attempts will be made up of failures
+        // with one final Success at the end.
         && forall i
              | 0 <= i < |DropLast(attemptsState)|
              :: attemptsState[i].output.Failure?
diff --git a/StandardLibrary/src/GetOpt.dfy b/StandardLibrary/src/GetOpt.dfy
index 54f344f609..4881f9bd10 100644
--- a/StandardLibrary/src/GetOpt.dfy
+++ b/StandardLibrary/src/GetOpt.dfy
@@ -104,11 +104,11 @@ Not Future Directions :
 */
 
 include "../../libraries/src/Wrappers.dfy"
-  //include "../../../../submodules/MaterialProviders/libraries/src/Collections/Sequences/Seq.dfy"
+//include "../../../../submodules/MaterialProviders/libraries/src/Collections/Sequences/Seq.dfy"
 
 module {:options "-functionSyntax:4"} GetOpt {
   import opened Wrappers
-    // import Seq, replace when repaired
+  // import Seq, replace when repaired
 
   method Example(args : seq<string>) returns (output : Result<bool, string>)
     requires 0 < |args|
diff --git a/StandardLibrary/test/TestComputeSetToOrderedSequenceCharLess.dfy b/StandardLibrary/test/TestComputeSetToOrderedSequenceCharLess.dfy
index fdabe9edc6..0055f16e8a 100644
--- a/StandardLibrary/test/TestComputeSetToOrderedSequenceCharLess.dfy
+++ b/StandardLibrary/test/TestComputeSetToOrderedSequenceCharLess.dfy
@@ -3,7 +3,7 @@
 
 include "../src/StandardLibrary.dfy"
 include "../src/Sets.dfy"
-  // Just to make sure we don't conflict with dafny-lang/libraries' Sets.dfy
+// Just to make sure we don't conflict with dafny-lang/libraries' Sets.dfy
 include "../../libraries/src/Collections/Sets/Sets.dfy"
 
 
diff --git a/StandardLibrary/test/TestComputeSetToOrderedSequenceUInt8Less.dfy b/StandardLibrary/test/TestComputeSetToOrderedSequenceUInt8Less.dfy
index 15818ef331..57c2fd2676 100644
--- a/StandardLibrary/test/TestComputeSetToOrderedSequenceUInt8Less.dfy
+++ b/StandardLibrary/test/TestComputeSetToOrderedSequenceUInt8Less.dfy
@@ -4,7 +4,7 @@
 include "../src/StandardLibrary.dfy"
 include "../src/Sets.dfy"
 include "../src/Time.dfy"
-  // Just to make sure we don't conflict with dafny-lang/libraries' Sets.dfy
+// Just to make sure we don't conflict with dafny-lang/libraries' Sets.dfy
 include "../../libraries/src/Collections/Sets/Sets.dfy"
 
 // This function is commonly used for sorting
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy
index 201cf7476b..9d75c176f7 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy
@@ -11,7 +11,7 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
   import opened UTF8
   import AwsCryptographyMaterialProvidersTypes
   import ComAmazonawsKmsTypes
-    // Generic helpers for verification of mock/unit tests.
+  // Generic helpers for verification of mock/unit tests.
   datatype DafnyCallEvent<I, O> = DafnyCallEvent(input: I, output: O)
 
   // Begin Generated Types
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/CmmFromKeyDescription.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/CmmFromKeyDescription.dfy
index 8c9fb7ddb7..1a225caf24 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/CmmFromKeyDescription.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/CmmFromKeyDescription.dfy
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 
 include "../Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy"
-  // Yes this is including from somewhere else.
+// Yes this is including from somewhere else.
 include "../../TestVectorsAwsCryptographicMaterialProviders/src/LibraryIndex.dfy"
 include "KeyringFromKeyDescription.dfy"
 
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy
index 62757d8912..937a65876e 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0
 
 include "../Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy"
-  // Yes, this is reaching across.
-  // ideally all these functions would exist in the STD Library.
+// Yes, this is reaching across.
+// ideally all these functions would exist in the STD Library.
 include "../../TestVectorsAwsCryptographicMaterialProviders/src/JSONHelpers.dfy"
 
 module {:options "-functionSyntax:4"} KeyDescription {
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyMaterial.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyMaterial.dfy
index 4254d9f7f3..1440c7578e 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyMaterial.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyMaterial.dfy
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0
 
 include "../Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy"
-  // Yes, this is reaching across.
-  // ideally all these functions would exist in the STD Library.
+// Yes, this is reaching across.
+// ideally all these functions would exist in the STD Library.
 include "../../TestVectorsAwsCryptographicMaterialProviders/src/JSONHelpers.dfy"
 
 module {:options "-functionSyntax:4"} KeyMaterial {
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy
index 48fd2150a4..c62c89bd0a 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyringFromKeyDescription.dfy
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 
 include "../Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy"
-  // Yes this is including from somewhere else.
+// Yes this is including from somewhere else.
 include "../../TestVectorsAwsCryptographicMaterialProviders/src/LibraryIndex.dfy"
 include "KeyMaterial.dfy"
 include "CreateStaticKeyrings.dfy"
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeysVectorOperations.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeysVectorOperations.dfy
index b12f4b63b8..266e32d11f 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeysVectorOperations.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeysVectorOperations.dfy
@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0
 
 include "../Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy"
-  // Yes, this is reaching across.
-  // ideally all these functions would exist in the STD Library.
+// Yes, this is reaching across.
+// ideally all these functions would exist in the STD Library.
 include "../../TestVectorsAwsCryptographicMaterialProviders/src/LibraryIndex.dfy"
 include "../../TestVectorsAwsCryptographicMaterialProviders/src/JSONHelpers.dfy"
 include "KeyDescription.dfy"
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy
index 0c30ef191b..f244779f07 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/ParseJsonManifests.dfy
@@ -25,8 +25,8 @@ module {:options "-functionSyntax:4"} ParseJsonManifests {
   import CompleteVectors
   import KeyVectors
   import KeyVectorsTypes = AwsCryptographyMaterialProvidersTestVectorKeysTypes
-    // This is a HACK!
-    // This is *ONLY* because this is wrapping the MPL
+  // This is a HACK!
+  // This is *ONLY* because this is wrapping the MPL
   import AlgorithmSuites
 
   function BuildEncryptTestVector(keys: KeyVectors.KeyVectorsClient, obj: seq<(string, JSON)>)
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy
index 6420f5bba0..6a2dc83d2b 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/TestVectorsAwsCryptographicMaterialProviders/src/TestManifests.dfy
@@ -4,7 +4,7 @@
 include "TestVectors.dfy"
 include "ParseJsonManifests.dfy"
 include "MplManifestOptions.dfy"
-  // TODO it would be nice to have this included somehow...
+// TODO it would be nice to have this included somehow...
 include "../../KeyVectors/src/Index.dfy"
 include "../../../../StandardLibrary/src/Time.dfy"
 
diff --git a/project.properties b/project.properties
index 5d11f69e27..6e4e1c568c 100644
--- a/project.properties
+++ b/project.properties
@@ -5,7 +5,7 @@
 #     export `export `cat ./aws-cryptographic-material-providers-library-dafny/project.properties`
 # The Java project include this file as a Gradle properties
 # And the Dotnet projects include and parse this file.
-dafnyVersion=4.9.0
-dafnyVerifyVersion=4.9.1
+dafnyVersion=4.11.0
+dafnyVerifyVersion=4.11.0
 dafnyRustVersion=nightly-2025-01-30-7db1e5f
 mplVersion=1.11.1-SNAPSHOT