diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
index b0372e8a9..a84587ea0 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographicMaterialProviders/Model/AwsCryptographyMaterialProvidersTypes.dfy
@@ -1712,7 +1712,7 @@ module {:extern "software.amazon.cryptography.materialproviders.internaldafny.ty
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyMaterialProvidersService
diff --git a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
index 0fad1ce05..bf5d9450f 100644
--- a/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
+++ b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/Model/AwsCryptographyKeyStoreTypes.dfy
@@ -282,7 +282,7 @@ module {:extern "software.amazon.cryptography.keystore.internaldafny.types" } Aw
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyKeyStoreService
diff --git a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy
index e442b0fff..a01e74bd8 100644
--- a/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy
+++ b/AwsCryptographyPrimitives/Model/AwsCryptographyPrimitivesTypes.dfy
@@ -689,7 +689,7 @@ module {:extern "software.amazon.cryptography.primitives.internaldafny.types" }
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyPrimitivesService
diff --git a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy
index dec776c14..b42a06773 100644
--- a/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy
+++ b/ComAmazonawsDynamodb/Model/ComAmazonawsDynamodbTypes.dfy
@@ -2725,7 +2725,7 @@ module {:extern "software.amazon.cryptography.services.dynamodb.internaldafny.ty
 
 
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractComAmazonawsDynamodbService {
diff --git a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy
index 6132487cb..a8a16c66a 100644
--- a/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy
+++ b/ComAmazonawsKms/Model/ComAmazonawsKmsTypes.dfy
@@ -1976,7 +1976,7 @@ module {:extern "software.amazon.cryptography.services.kms.internaldafny.types"
 
 
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractComAmazonawsKmsService {
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy
index 7d9894703..f37e544cf 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy
+++ b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/Model/AwsCryptographyMaterialProvidersTestVectorKeysTypes.dfy
@@ -260,7 +260,7 @@ module {:extern "software.amazon.cryptography.materialproviderstestvectorkeys.in
     // || (!exit(A(I)) && !access(B(I)))
     | CollectionOfErrors(list: seq<Error>, nameonly message: string)
       // The Opaque error, used for native, extern, wrapped or unknown errors
-    | Opaque(obj: object, alt_text : string)
+    | Opaque(obj: object, alt_text : string := "")
   type OpaqueError = e: Error | e.Opaque? witness *
 }
 abstract module AbstractAwsCryptographyMaterialProvidersTestVectorKeysService
diff --git a/smithy-dafny b/smithy-dafny
index e602cbf45..cff81f5ba 160000
--- a/smithy-dafny
+++ b/smithy-dafny
@@ -1 +1 @@
-Subproject commit e602cbf45e55108f3a753c1ea06d38bd5fcdbe3c
+Subproject commit cff81f5baa7104f6873aadc81d8e9a75121253cd