diff --git a/.github/workflows/library_go_tests.yml b/.github/workflows/library_go_tests.yml
index f38c5363e..8f31e011f 100644
--- a/.github/workflows/library_go_tests.yml
+++ b/.github/workflows/library_go_tests.yml
@@ -19,7 +19,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        library: [AwsEncryptionSDK]
+        library: [AwsEncryptionSDK, TestVectors]
         go-version: [ "1.23" ]
         os: [
           # Sed script doesn't work properly on windows
@@ -74,6 +74,22 @@ jobs:
           # This works because `node` is installed by default on GHA runners
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_go CORES=$CORES
+          
+      - name: Unzip .NET Retry Flag Manifests
+        shell: bash
+        working-directory: TestVectors/dafny/TestVectors/test/
+        run: |
+          unzip invalid-Net-4.0.0.zip -d invalid-Net-4.0.0
+          unzip v4-Net-4.0.1.zip -d v4-Net-4.0.1
+          unzip valid-Net-4.0.0.zip -d valid-Net-4.0.0
+
+      # TODO: Remove this after Go polymorph does not generate unwanted duplicate code.
+      - name: Purge polymorph code in Go
+        if: matrix.library == 'TestVectors'
+        working-directory: ./${{ matrix.library }}
+        shell: bash
+        run: |
+          make purge_polymorph_code
 
       - name: Test Go
         working-directory: ${{ matrix.library }}
diff --git a/.github/workflows/library_interop_test_vectors.yml b/.github/workflows/library_interop_test_vectors.yml
index e384bdfe9..36f83068e 100644
--- a/.github/workflows/library_interop_test_vectors.yml
+++ b/.github/workflows/library_interop_test_vectors.yml
@@ -25,7 +25,7 @@ jobs:
             ubuntu-latest,
             macos-13,
           ]
-        language: [java, net, rust]
+        language: [java, net, rust, go]
         # https://taskei.amazon.dev/tasks/CrypTool-5284
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
@@ -43,7 +43,7 @@ jobs:
           uses: aws-actions/configure-aws-credentials@v2
           with:
             aws-region: us-west-2
-            role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2
+            role-to-assume: arn:aws:iam::370957321024:role/GitHub-CI-Public-ESDK-Dafny-Role-us-west-2 
             role-session-name: InterOpTests
 
         - uses: actions/checkout@v3
@@ -75,7 +75,7 @@ jobs:
         # TODO - uncomment this after Rust formatter works
         # - name: Rustfmt Check
         #   uses: actions-rust-lang/rustfmt@v1
-
+        
         # TODO: Remove this after the formatting in Rust starts working
         - name: smithy-dafny Rust hacks
           if: matrix.language == 'rust'
@@ -87,6 +87,15 @@ jobs:
               sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' mpl/smithy-dafny/SmithyDafnyMakefile.mk
             fi
 
+        - name: Setup Go
+          uses: actions/setup-go@v5
+          with:
+            go-version: "1.23"
+    
+        - name: Install Go imports
+          run: |
+            go install golang.org/x/tools/cmd/goimports@latest
+
         - name: Setup NASM for Windows in Rust (aws-lc-sys)
           if: matrix.language == 'rust' && matrix.os == 'windows-latest'
           uses: ilammy/setup-nasm@v1
@@ -122,11 +131,11 @@ jobs:
             # This works because `node` is installed by default on GHA runners
             CORES=$(node -e 'console.log(os.cpus().length)')
             make transpile_net
-
+        
         - name: Install Smithy-Dafny codegen dependencies
           if: matrix.language == 'rust'
           uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
-
+    
         # TODO: Remove this after checking in Rust polymorph code
         - name: Run make polymorph_rust
           if: matrix.language == 'rust'
@@ -134,7 +143,7 @@ jobs:
           working-directory: ./${{ matrix.library }}
           run: |
             make polymorph_rust
-
+        
         - name: Build ${{ matrix.library }} implementation in Rust
           if: matrix.language == 'rust'
           shell: bash
@@ -142,6 +151,23 @@ jobs:
           run: |
             CORES=$(node -e 'console.log(os.cpus().length)')
             make transpile_rust CORES=$CORES
+        
+        - name: Build ${{ matrix.library }} implementation in Go
+          if: matrix.language == 'go'
+          shell: bash
+          working-directory: ./${{ matrix.library }}
+          run: |
+            # This works because `node` is installed by default on GHA runners
+            CORES=$(node -e 'console.log(os.cpus().length)')
+            make transpile_go
+
+        # TODO: Remove this after Go polymorph does not generate unwanted duplicate code.
+        - name: Purge polymorph code in Go
+          if: matrix.language == 'go'
+          shell: bash
+          working-directory: ./${{ matrix.library }}
+          run: |
+            make purge_polymorph_code
 
         - name: Setup gradle
           if: matrix.language == 'java'
@@ -177,8 +203,8 @@ jobs:
             ubuntu-latest,
             macos-13,
           ]
-        encrypting_language: [java, net, rust]
-        decrypting_language: [java, net, rust]
+        encrypting_language: [java, net, rust, go]
+        decrypting_language: [java, net, rust, go]
         # https://taskei.amazon.dev/tasks/CrypTool-5284
         dotnet-version: ["6.0.x"]
     runs-on: ${{ matrix.os }}
@@ -240,6 +266,15 @@ jobs:
             sed -i 's|rustfmt --edition 2021 runtimes/rust/src/implementation_from_dafny.rs|#&|' mpl/smithy-dafny/SmithyDafnyMakefile.mk
           fi
 
+      - name: Setup Go
+        uses: actions/setup-go@v5
+        with:
+          go-version: "1.23"
+
+      - name: Install Go imports
+        run: |
+          go install golang.org/x/tools/cmd/goimports@latest
+
       - name: Setup NASM for Windows in Rust (aws-lc-sys)
         if: matrix.decrypting_language == 'rust' && matrix.os == 'windows-latest'
         uses: ilammy/setup-nasm@v1
@@ -279,7 +314,7 @@ jobs:
       - name: Install Smithy-Dafny codegen dependencies
         if: matrix.decrypting_language == 'rust'
         uses: ./.github/actions/install_smithy_dafny_codegen_dependencies
-
+  
       # TODO: Remove this after checking in Rust polymorph code
       - name: Run make polymorph_rust
         if: matrix.decrypting_language == 'rust'
@@ -295,6 +330,23 @@ jobs:
         run: |
           CORES=$(node -e 'console.log(os.cpus().length)')
           make transpile_rust CORES=$CORES
+      
+      - name: Build ${{ matrix.library }} implementation in Go
+        if: matrix.decrypting_language == 'go'
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          # This works because `node` is installed by default on GHA runners
+          CORES=$(node -e 'console.log(os.cpus().length)')
+          make transpile_go
+          
+      # TODO: Remove this after Go polymorph does not generate unwanted duplicate code.
+      - name: Purge polymorph code in Go
+        if: matrix.decrypting_language == 'go'
+        shell: bash
+        working-directory: ./${{ matrix.library }}
+        run: |
+          make purge_polymorph_code
 
       - name: Download Encrypt Manifest Artifact
         uses: actions/download-artifact@v4
diff --git a/TestVectors/Makefile b/TestVectors/Makefile
index 81d595c2e..ad4bc090a 100644
--- a/TestVectors/Makefile
+++ b/TestVectors/Makefile
@@ -2,7 +2,7 @@
 # SPDX-License-Identifier: Apache-2.0
 
 CORES=2
-
+ENABLE_EXTERN_PROCESSING=1
 TRANSPILE_TESTS_IN_RUST=1
 
 include ../SharedMakefileV2.mk
@@ -101,6 +101,10 @@ IMPLEMENTATION_FROM_DAFNY_TV_RUST_ESDK_MAIN= \
 	let dafny_args = dafny_runtime::Sequence::from_array_owned(dafny_strings);\
 	r\#_WrappedESDKMain_Compile::_default::Main2(\&dafny_args);"
 
+IMPLEMENTATION_FROM_DAFNY_TV_GO_FILE=runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny.go
+IMPLEMENTATION_FROM_DAFNY_TV_GO_MPL_MAIN="m_WrappedMaterialProvidersMain.Companion_Default___.Main(_dafny.FromMainArguments(os.Args))"
+IMPLEMENTATION_FROM_DAFNY_TV_GO_ESDK_MAIN="m_WrappedESDKMain.Companion_Default___.Main2(_dafny.FromMainArguments(os.Args))"
+
 # TODO: Remove after wrapped client issue is fixed in Rust
 REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES=runtimes/rust/src/deps/aws_cryptography_primitives.rs
 REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_KEYSTORE=runtimes/rust/src/deps/aws_cryptography_keyStore.rs
@@ -109,9 +113,54 @@ REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_2 := 'pub mod wrapped;'
 REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1 := '\/\/ removed wrapped-client feature using sed;'
 REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_2 := '\/\/ removed wrapped module using sed;'
 
+# Go
+
+GO_MODULE_NAME="github.com/aws/aws-encryption-sdk/testvectors"
+
+GO_DEPENDENCY_MODULE_NAMES := \
+	--dependency-library-name=aws.cryptography.encryptionSdk=github.com/aws/aws-encryption-sdk \
+	--dependency-library-name=com.amazonaws.dynamodb=github.com/aws/aws-cryptographic-material-providers-library/dynamodb \
+	--dependency-library-name=com.amazonaws.kms=github.com/aws/aws-cryptographic-material-providers-library/kms \
+	--dependency-library-name=aws.cryptography.keyStore=github.com/aws/aws-cryptographic-material-providers-library/mpl \
+	--dependency-library-name=aws.cryptography.primitives=github.com/aws/aws-cryptographic-material-providers-library/primitives \
+	--dependency-library-name=aws.cryptography.materialProviders=github.com/aws/aws-cryptographic-material-providers-library/mpl \
+    	--dependency-library-name=sdk.com.amazonaws.dynamodb=github.com/aws/aws-sdk-go-v2/service/dynamodb \
+    	--dependency-library-name=sdk.com.amazonaws.kms=github.com/aws/aws-sdk-go-v2/service/kms
+
+TRANSLATION_RECORD_GO := \
+	AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+	mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+	mpl/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+	mpl/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+	mpl/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+	mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr \
+	mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/ImplementationFromDafny-go.dtr
+
+# Constants for languages that drop extern names (Go)
+
+WRAPPED_INDEX_FILE_PATH=dafny/TestVectors/src/LibraryIndex.dfy
+WRAPPED_INDEX_FILE_WITH_EXTERN_STRING="module {:extern \"software.amazon.cryptography.encryptionsdk.internaldafny.wrapped\" } WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService"
+WRAPPED_INDEX_FILE_WITHOUT_EXTERN_STRING="module WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService"
+
 transpile_implementation_java: _replace_main_method_name_java
 transpile_implementation_net: _replace_main_method_name_net
 transpile_implementation_rust: _replace_main_method_name_rust
+transpile_implementation_go: _replace_main_method_name_go
+
+_polymorph_go: purge_polymorph_code
+
+# Smithy-dafny generated shim needs a long term fix. 
+# TODO: Remove this commands once smithy-dafny is fixed
+# This commands does not work on windows
+# https://taskei.amazon.dev/tasks/CrypTool-5283
+purge_polymorph_code:
+	find .. -name "shim.go" | xargs sed -i $(SED_PARAMETER) 's/(_static \*CompanionStruct_Default___)//g'
+	rm -rf runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygenerated \
+		runtimes/go/ImplementationFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes \
+		runtimes/go/ImplementationFromDafny-go/WrappedAwsCryptographyEncryptionSdkService \
+		runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygenerated \
+		runtimes/go/TestsFromDafny-go/awscryptographyencryptionsdksmithygeneratedtypes \
+		runtimes/go/TestsFromDafny-go/WrappedAwsCryptographyEncryptionSdkService
 
 # TODO: Remove after wrapped client issue is fixed in Rust
 _polymorph_rust: _remove_wrapped_client_rust
@@ -125,6 +174,9 @@ _replace_main_method_name_net:
 _replace_main_method_name_rust:
 	$(MAKE) _sed_file SED_FILE_PATH=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_FILE) SED_BEFORE_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_MPL_MAIN) SED_AFTER_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_RUST_ESDK_MAIN)
 
+_replace_main_method_name_go:
+	$(MAKE) _sed_file SED_FILE_PATH=$(IMPLEMENTATION_FROM_DAFNY_TV_GO_FILE) SED_BEFORE_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_GO_MPL_MAIN) SED_AFTER_STRING=$(IMPLEMENTATION_FROM_DAFNY_TV_GO_ESDK_MAIN)
+
 # TODO: Remove after wrapped client issue is fixed in Rust
 _remove_wrapped_client_rust:
 	$(MAKE) _sed_file SED_FILE_PATH=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_PRIMITIVES) SED_BEFORE_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_FROM_1) SED_AFTER_STRING=$(REMOVE_WRAPPED_CLIENT_AFTER_POLYMORPH_RUST_TO_1)
@@ -150,6 +202,10 @@ test_generate_vectors_rust:
 	cd ../../
 	cp dafny/TestVectors/test/keys.json runtimes/rust/
 
+test_generate_vectors_go:
+	go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go encrypt-manifest --encrypt-manifest-output ../
+	cp dafny/TestVectors/test/keys.json runtimes/go
+
 test_encrypt_vectors_java:
 	gradle -p runtimes/java run --args="encrypt --manifest-path . --decrypt-manifest-path ."
 
@@ -164,6 +220,9 @@ test_encrypt_vectors_rust:
 	cargo run --bin test-vectors --features="wrapped-client" --release -- encrypt --manifest-path . --decrypt-manifest-path . && \
 	cd ../../
 
+test_encrypt_vectors_go:
+	go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go encrypt --manifest-path=.. --decrypt-manifest-path=..
+
 test_decrypt_encrypt_vectors_java:
 	gradle -p runtimes/java run --args="decrypt --manifest-path . --manifest-name decrypt-manifest.json"
 
@@ -184,6 +243,20 @@ test_decrypt_encrypt_vectors_rust:
 	cargo run --bin test-vectors --features="wrapped-client" --release -- decrypt --manifest-path . --manifest-name decrypt-manifest.json && \
 	cd ../../
 
+test_decrypt_encrypt_vectors_go:
+	go -C runtimes/go/ImplementationFromDafny-go run ImplementationFromDafny.go decrypt --manifest-path=.. --manifest-name=decrypt-manifest.json
+
 _polymorph_dependencies:
 	@echo "No polymorphing of dependency"
 
+_sed_types_file_remove_extern:
+	@echo "No extern to process for ESDK TestVectors"
+
+_sed_index_file_remove_extern:
+	@echo "No extern to process for ESDK TestVectors"
+
+_sed_types_file_add_extern:
+	@echo "No extern to process for ESDK TestVectors"
+
+_sed_index_file_add_extern:
+	@echo "No extern to process for ESDK TestVectors"
diff --git a/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy b/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy
index 7097ff992..57d7f92f7 100644
--- a/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy
+++ b/TestVectors/dafny/TestVectors/src/LibraryIndex.dfy
@@ -3,9 +3,7 @@
 
 include "../Model/AwsCryptographyEncryptionSdkTypesWrapped.dfy"
 
-module
-  {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.wrapped" }
-  WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService
+module {:extern "software.amazon.cryptography.encryptionsdk.internaldafny.wrapped" } WrappedESDK refines WrappedAbstractAwsCryptographyEncryptionSdkService
 {
   import WrappedService = ESDK
 
@@ -51,4 +49,4 @@ module
       netV4_0_0_RetryPolicy := Some(netV4_0_0_RetryPolicy)
     )
   }
-}
\ No newline at end of file
+}
diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/WrappedESDK/extern.go b/TestVectors/runtimes/go/ImplementationFromDafny-go/WrappedESDK/extern.go
new file mode 100644
index 000000000..f7c876b96
--- /dev/null
+++ b/TestVectors/runtimes/go/ImplementationFromDafny-go/WrappedESDK/extern.go
@@ -0,0 +1,11 @@
+package WrappedESDK
+
+import (
+	"github.com/aws/aws-encryption-sdk/AwsCryptographyEncryptionSdkTypes"
+	"github.com/aws/aws-encryption-sdk/test/WrappedAwsCryptographyEncryptionSdkService"
+	"github.com/dafny-lang/DafnyStandardLibGo/Wrappers"
+)
+
+func (_static CompanionStruct_Default___) WrappedESDK(config AwsCryptographyEncryptionSdkTypes.AwsEncryptionSdkConfig) Wrappers.Result {
+	return WrappedAwsCryptographyEncryptionSdkService.WrappedESDK(config)
+}
diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod
new file mode 100644
index 000000000..b4ecbc1fd
--- /dev/null
+++ b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.mod
@@ -0,0 +1,47 @@
+module github.com/aws/aws-encryption-sdk/testvectors
+
+go 1.23.2
+
+replace (
+	github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 => ../../../../mpl/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 => ../../../../mpl/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../mpl/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/testvectors v0.0.0 => ../../../../mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-encryption-sdk v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-encryption-sdk/test v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/TestsFromDafny-go/
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0 => ../../../../mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/
+)
+
+require (
+	github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/testvectors v0.0.0
+	github.com/aws/aws-encryption-sdk v0.0.0
+	github.com/aws/aws-encryption-sdk/test v0.0.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0
+)
+
+require (
+	github.com/aws/aws-sdk-go-v2 v1.31.0 // indirect
+	github.com/aws/aws-sdk-go-v2/config v1.27.37 // indirect
+	github.com/aws/aws-sdk-go-v2/credentials v1.17.35 // indirect
+	github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 // indirect
+	github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 // indirect
+	github.com/aws/smithy-go v1.21.0 // indirect
+	github.com/google/uuid v1.6.0 // indirect
+	github.com/jmespath/go-jmespath v0.4.0 // indirect
+)
diff --git a/TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum
new file mode 100644
index 000000000..3f00f4e18
--- /dev/null
+++ b/TestVectors/runtimes/go/ImplementationFromDafny-go/go.sum
@@ -0,0 +1,48 @@
+github.com/aws/aws-sdk-go-v2 v1.31.0 h1:3V05LbxTSItI5kUqNwhJrrrY1BAXxXt0sN0l72QmG5U=
+github.com/aws/aws-sdk-go-v2 v1.31.0/go.mod h1:ztolYtaEUtdpf9Wftr31CJfLVjOnD/CVRkKOOYgF8hA=
+github.com/aws/aws-sdk-go-v2/config v1.27.37 h1:xaoIwzHVuRWRHFI0jhgEdEGc8xE1l91KaeRDsWEIncU=
+github.com/aws/aws-sdk-go-v2/config v1.27.37/go.mod h1:S2e3ax9/8KnMSyRVNd3sWTKs+1clJ2f1U6nE0lpvQRg=
+github.com/aws/aws-sdk-go-v2/credentials v1.17.35 h1:7QknrZhYySEB1lEXJxGAmuD5sWwys5ZXNr4m5oEz0IE=
+github.com/aws/aws-sdk-go-v2/credentials v1.17.35/go.mod h1:8Vy4kk7at4aPSmibr7K+nLTzG6qUQAUO4tW49fzUV4E=
+github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 h1:C/d03NAmh8C4BZXhuRNboF/DqhBkBCeDiJDcaqIT5pA=
+github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14/go.mod h1:7I0Ju7p9mCIdlrfS+JCgqcYD0VXz/N4yozsox+0o078=
+github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 h1:kYQ3H1u0ANr9KEKlGs/jTLrBFPo8P8NaH/w7A01NeeM=
+github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18/go.mod h1:r506HmK5JDUh9+Mw4CfGJGSSoqIiLCndAuqXuhbv67Y=
+github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 h1:Z7IdFUONvTcvS7YuhtVxN99v2cCoHRXOS4mTr0B/pUc=
+github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18/go.mod h1:DkKMmksZVVyat+Y+r1dEOgJEfUeA7UngIHWeKsi0yNc=
+github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 h1:VaRN3TlFdd6KxX1x3ILT5ynH6HvKgqdiXoTxAF4HQcQ=
+github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1/go.mod h1:FbtygfRFze9usAadmnGJNc8KsP346kEe+y2/oyhGAGc=
+github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 h1:DDN8yqYzFUDy2W5zk3tLQNKaO/1t0h3fNixPJacu264=
+github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1/go.mod h1:k5XW8MoMxsNZ20RJmsokakvENUwQyjv69R9GqrI4xdQ=
+github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 h1:QFASJGfT8wMXtuP3D5CRmMjARHv9ZmzFUMJznHDOY3w=
+github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5/go.mod h1:QdZ3OmoIjSX+8D1OPAzPxDfjXASbBMDsz9qvtyIhtik=
+github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 h1:dOxqOlOEa2e2heC/74+ZzcJOa27+F1aXFZpYgY/4QfA=
+github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19/go.mod h1:aV6U1beLFvk3qAgognjS3wnGGoDId8hlPEiBsLHXVZE=
+github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 h1:Xbwbmk44URTiHNx6PNo0ujDE6ERlsCKJD3u1zfnzAPg=
+github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20/go.mod h1:oAfOFzUB14ltPZj1rWwRc3d/6OgD76R8KlvU3EqM9Fg=
+github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 h1:jwWMpQ/1obJRdHaix9k10zWSnSMZGdDTZIDiS5CGzq8=
+github.com/aws/aws-sdk-go-v2/service/kms v1.36.0/go.mod h1:OHmlX4+o0XIlJAQGAHPIy0N9yZcYS/vNG+T7geSNcFw=
+github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 h1:2jrVsMHqdLD1+PA4BA6Nh1eZp0Gsy3mFSB5MxDvcJtU=
+github.com/aws/aws-sdk-go-v2/service/sso v1.23.1/go.mod h1:XRlMvmad0ZNL+75C5FYdMvbbLkd6qiqz6foR1nA1PXY=
+github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 h1:0L7yGCg3Hb3YQqnSgBTZM5wepougtL1aEccdcdYhHME=
+github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1/go.mod h1:FnvDM4sfa+isJ3kDXIzAB9GAwVSzFzSy97uZ3IsHo4E=
+github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 h1:8K0UNOkZiK9Uh3HIF6Bx0rcNCftqGCeKmOaR7Gp5BSo=
+github.com/aws/aws-sdk-go-v2/service/sts v1.31.1/go.mod h1:yMWe0F+XG0DkRZK5ODZhG7BEFYhLXi2dqGsv6tX0cgI=
+github.com/aws/smithy-go v1.21.0 h1:H7L8dtDRk0P1Qm6y0ji7MCYMQObJ5R9CRpyPhRUkLYA=
+github.com/aws/smithy-go v1.21.0/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg=
+github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 h1:g/xAj4F7Zt9wXJ6QjfbfocVi/ZYlAFpNddHCFyfzRDg=
+github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto=
+github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8=
+github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=
+github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0=
+github.com/google/uuid v1.6.0/go.mod h1:TIyPZe4MgqvfeYDBFedMoGGpEw/LqOeaOT+nhxU+yHo=
+github.com/jmespath/go-jmespath v0.4.0 h1:BEgLn5cpjn8UN1mAw4NjwDrS35OdebyEtFe+9YPoQUg=
+github.com/jmespath/go-jmespath v0.4.0/go.mod h1:T8mJZnbsbmF+m6zOOFylbeCJqk5+pHWvzYPziyZiYoo=
+github.com/jmespath/go-jmespath/internal/testify v1.5.1 h1:shLQSRRSCCPj3f2gpwzGwWFoC7ycTf1rcQZHOlsJ6N8=
+github.com/jmespath/go-jmespath/internal/testify v1.5.1/go.mod h1:L3OGu8Wl2/fWfCI6z80xFu9LTZmf1ZRjMHUOPmWr69U=
+github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZbAQM=
+github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4=
+github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME=
+gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0=
+gopkg.in/yaml.v2 v2.2.8 h1:obN1ZagJSUGI0Ek/LBmuj4SNLPfIny3KsKFopxRdj10=
+gopkg.in/yaml.v2 v2.2.8/go.mod h1:hI93XBmqTisBFMUTm0b8Fm+jr3Dg1NNxqwp+5A1VGuI=
diff --git a/TestVectors/runtimes/go/TestsFromDafny-go/TestWrappedESDKMain/extern.go b/TestVectors/runtimes/go/TestsFromDafny-go/TestWrappedESDKMain/extern.go
new file mode 100644
index 000000000..d670fc2ac
--- /dev/null
+++ b/TestVectors/runtimes/go/TestsFromDafny-go/TestWrappedESDKMain/extern.go
@@ -0,0 +1,19 @@
+package TestWrappedESDKMain
+
+import (
+	os "os"
+
+	"github.com/dafny-lang/DafnyRuntimeGo/v4/dafny"
+)
+
+// TODO: Remove this once Dafny bug is fixed.
+// Dafny bug: https://t.corp.amazon.com/9a9028fd-2711-4843-b8f0-09965f7e61a7/communication#f03694be-7410-47f9-866d-e43093b018f9
+var m_TestWrappedESDKMain = CompanionStruct_Default___{}
+
+func (CompanionStruct_Default___) GetTestVectorExecutionDirectory() dafny.Sequence {
+	cwd, err := os.Getwd()
+	if err != nil {
+		panic(err)
+	}
+	return dafny.SeqOfString(cwd + "/../../../")
+}
diff --git a/TestVectors/runtimes/go/TestsFromDafny-go/go.mod b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod
new file mode 100644
index 000000000..afed1f510
--- /dev/null
+++ b/TestVectors/runtimes/go/TestsFromDafny-go/go.mod
@@ -0,0 +1,49 @@
+module github.com/aws/aws-encryption-sdk/testvectors/test
+
+go 1.23.2
+
+replace (
+	github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0 => ../../../../mpl/ComAmazonawsDynamodb/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0 => ../../../../mpl/ComAmazonawsKms/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0 => ../../../../mpl/AwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0 => ../../../../mpl/AwsCryptographyPrimitives/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-cryptographic-material-providers-library/testvectors v0.0.0 => ../../../../mpl/TestVectorsAwsCryptographicMaterialProviders/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-encryption-sdk v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/ImplementationFromDafny-go/
+	github.com/aws/aws-encryption-sdk/test v0.0.0 => ../../../../AwsEncryptionSDK/runtimes/go/TestsFromDafny-go
+	github.com/aws/aws-encryption-sdk/testvectors v0.0.0 => ../ImplementationFromDafny-go/
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0 => ../../../../mpl/StandardLibrary/runtimes/go/ImplementationFromDafny-go/
+)
+
+require (
+	github.com/aws/aws-cryptographic-material-providers-library/dynamodb v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/kms v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/mpl v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/primitives v0.0.0
+	github.com/aws/aws-cryptographic-material-providers-library/testvectors v0.0.0
+	github.com/aws/aws-encryption-sdk v0.0.0
+	github.com/aws/aws-encryption-sdk/testvectors v0.0.0
+	github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2
+	github.com/dafny-lang/DafnyStandardLibGo v0.0.0
+)
+
+require (
+	github.com/aws/aws-encryption-sdk/test v0.0.0 // indirect
+	github.com/aws/aws-sdk-go-v2 v1.31.0 // indirect
+	github.com/aws/aws-sdk-go-v2/config v1.27.37 // indirect
+	github.com/aws/aws-sdk-go-v2/credentials v1.17.35 // indirect
+	github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 // indirect
+	github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 // indirect
+	github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 // indirect
+	github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 // indirect
+	github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 // indirect
+	github.com/aws/smithy-go v1.21.0 // indirect
+	github.com/google/uuid v1.6.0 // indirect
+	github.com/jmespath/go-jmespath v0.4.0 // indirect
+)
diff --git a/TestVectors/runtimes/go/TestsFromDafny-go/go.sum b/TestVectors/runtimes/go/TestsFromDafny-go/go.sum
new file mode 100644
index 000000000..3f00f4e18
--- /dev/null
+++ b/TestVectors/runtimes/go/TestsFromDafny-go/go.sum
@@ -0,0 +1,48 @@
+github.com/aws/aws-sdk-go-v2 v1.31.0 h1:3V05LbxTSItI5kUqNwhJrrrY1BAXxXt0sN0l72QmG5U=
+github.com/aws/aws-sdk-go-v2 v1.31.0/go.mod h1:ztolYtaEUtdpf9Wftr31CJfLVjOnD/CVRkKOOYgF8hA=
+github.com/aws/aws-sdk-go-v2/config v1.27.37 h1:xaoIwzHVuRWRHFI0jhgEdEGc8xE1l91KaeRDsWEIncU=
+github.com/aws/aws-sdk-go-v2/config v1.27.37/go.mod h1:S2e3ax9/8KnMSyRVNd3sWTKs+1clJ2f1U6nE0lpvQRg=
+github.com/aws/aws-sdk-go-v2/credentials v1.17.35 h1:7QknrZhYySEB1lEXJxGAmuD5sWwys5ZXNr4m5oEz0IE=
+github.com/aws/aws-sdk-go-v2/credentials v1.17.35/go.mod h1:8Vy4kk7at4aPSmibr7K+nLTzG6qUQAUO4tW49fzUV4E=
+github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14 h1:C/d03NAmh8C4BZXhuRNboF/DqhBkBCeDiJDcaqIT5pA=
+github.com/aws/aws-sdk-go-v2/feature/ec2/imds v1.16.14/go.mod h1:7I0Ju7p9mCIdlrfS+JCgqcYD0VXz/N4yozsox+0o078=
+github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18 h1:kYQ3H1u0ANr9KEKlGs/jTLrBFPo8P8NaH/w7A01NeeM=
+github.com/aws/aws-sdk-go-v2/internal/configsources v1.3.18/go.mod h1:r506HmK5JDUh9+Mw4CfGJGSSoqIiLCndAuqXuhbv67Y=
+github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18 h1:Z7IdFUONvTcvS7YuhtVxN99v2cCoHRXOS4mTr0B/pUc=
+github.com/aws/aws-sdk-go-v2/internal/endpoints/v2 v2.6.18/go.mod h1:DkKMmksZVVyat+Y+r1dEOgJEfUeA7UngIHWeKsi0yNc=
+github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1 h1:VaRN3TlFdd6KxX1x3ILT5ynH6HvKgqdiXoTxAF4HQcQ=
+github.com/aws/aws-sdk-go-v2/internal/ini v1.8.1/go.mod h1:FbtygfRFze9usAadmnGJNc8KsP346kEe+y2/oyhGAGc=
+github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1 h1:DDN8yqYzFUDy2W5zk3tLQNKaO/1t0h3fNixPJacu264=
+github.com/aws/aws-sdk-go-v2/service/dynamodb v1.35.1/go.mod h1:k5XW8MoMxsNZ20RJmsokakvENUwQyjv69R9GqrI4xdQ=
+github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5 h1:QFASJGfT8wMXtuP3D5CRmMjARHv9ZmzFUMJznHDOY3w=
+github.com/aws/aws-sdk-go-v2/service/internal/accept-encoding v1.11.5/go.mod h1:QdZ3OmoIjSX+8D1OPAzPxDfjXASbBMDsz9qvtyIhtik=
+github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19 h1:dOxqOlOEa2e2heC/74+ZzcJOa27+F1aXFZpYgY/4QfA=
+github.com/aws/aws-sdk-go-v2/service/internal/endpoint-discovery v1.9.19/go.mod h1:aV6U1beLFvk3qAgognjS3wnGGoDId8hlPEiBsLHXVZE=
+github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20 h1:Xbwbmk44URTiHNx6PNo0ujDE6ERlsCKJD3u1zfnzAPg=
+github.com/aws/aws-sdk-go-v2/service/internal/presigned-url v1.11.20/go.mod h1:oAfOFzUB14ltPZj1rWwRc3d/6OgD76R8KlvU3EqM9Fg=
+github.com/aws/aws-sdk-go-v2/service/kms v1.36.0 h1:jwWMpQ/1obJRdHaix9k10zWSnSMZGdDTZIDiS5CGzq8=
+github.com/aws/aws-sdk-go-v2/service/kms v1.36.0/go.mod h1:OHmlX4+o0XIlJAQGAHPIy0N9yZcYS/vNG+T7geSNcFw=
+github.com/aws/aws-sdk-go-v2/service/sso v1.23.1 h1:2jrVsMHqdLD1+PA4BA6Nh1eZp0Gsy3mFSB5MxDvcJtU=
+github.com/aws/aws-sdk-go-v2/service/sso v1.23.1/go.mod h1:XRlMvmad0ZNL+75C5FYdMvbbLkd6qiqz6foR1nA1PXY=
+github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1 h1:0L7yGCg3Hb3YQqnSgBTZM5wepougtL1aEccdcdYhHME=
+github.com/aws/aws-sdk-go-v2/service/ssooidc v1.27.1/go.mod h1:FnvDM4sfa+isJ3kDXIzAB9GAwVSzFzSy97uZ3IsHo4E=
+github.com/aws/aws-sdk-go-v2/service/sts v1.31.1 h1:8K0UNOkZiK9Uh3HIF6Bx0rcNCftqGCeKmOaR7Gp5BSo=
+github.com/aws/aws-sdk-go-v2/service/sts v1.31.1/go.mod h1:yMWe0F+XG0DkRZK5ODZhG7BEFYhLXi2dqGsv6tX0cgI=
+github.com/aws/smithy-go v1.21.0 h1:H7L8dtDRk0P1Qm6y0ji7MCYMQObJ5R9CRpyPhRUkLYA=
+github.com/aws/smithy-go v1.21.0/go.mod h1:irrKGvNn1InZwb2d7fkIRNucdfwR8R+Ts3wxYa/cJHg=
+github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2 h1:g/xAj4F7Zt9wXJ6QjfbfocVi/ZYlAFpNddHCFyfzRDg=
+github.com/dafny-lang/DafnyRuntimeGo/v4 v4.9.2/go.mod h1:l2Tm4N2DKuq3ljONC2vOATeM9PUpXbIc8SgXdwwqEto=
+github.com/davecgh/go-spew v1.1.0 h1:ZDRjVQ15GmhC3fiQ8ni8+OwkZQO4DARzQgrnXU1Liz8=
+github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=
+github.com/google/uuid v1.6.0 h1:NIvaJDMOsjHA8n1jAhLSgzrAzy1Hgr+hNrb57e+94F0=
+github.com/google/uuid v1.6.0/go.mod h1:TIyPZe4MgqvfeYDBFedMoGGpEw/LqOeaOT+nhxU+yHo=
+github.com/jmespath/go-jmespath v0.4.0 h1:BEgLn5cpjn8UN1mAw4NjwDrS35OdebyEtFe+9YPoQUg=
+github.com/jmespath/go-jmespath v0.4.0/go.mod h1:T8mJZnbsbmF+m6zOOFylbeCJqk5+pHWvzYPziyZiYoo=
+github.com/jmespath/go-jmespath/internal/testify v1.5.1 h1:shLQSRRSCCPj3f2gpwzGwWFoC7ycTf1rcQZHOlsJ6N8=
+github.com/jmespath/go-jmespath/internal/testify v1.5.1/go.mod h1:L3OGu8Wl2/fWfCI6z80xFu9LTZmf1ZRjMHUOPmWr69U=
+github.com/pmezard/go-difflib v1.0.0 h1:4DBwDE0NGyQoBHbLQYPwSUPoCMWR5BEzIk/f1lZbAQM=
+github.com/pmezard/go-difflib v1.0.0/go.mod h1:iKH77koFhYxTK1pcRnkKkqfTogsbg7gZNVY4sRDYZ/4=
+github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME=
+gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0=
+gopkg.in/yaml.v2 v2.2.8 h1:obN1ZagJSUGI0Ek/LBmuj4SNLPfIny3KsKFopxRdj10=
+gopkg.in/yaml.v2 v2.2.8/go.mod h1:hI93XBmqTisBFMUTm0b8Fm+jr3Dg1NNxqwp+5A1VGuI=