diff --git a/SmithyDafnyMakefile.mk b/SmithyDafnyMakefile.mk
index 6c869e119e..376641d0af 100644
--- a/SmithyDafnyMakefile.mk
+++ b/SmithyDafnyMakefile.mk
@@ -154,7 +154,7 @@ clean-dafny-report:
 # Transpile the entire project's impl
 # For each index file listed in the project Makefile's PROJECT_INDEX variable,
 #   append a `-library:TestModels/$(PROJECT_INDEX) to the transpiliation target
-_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, -library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
+_transpile_implementation_all: TRANSPILE_DEPENDENCIES=$(patsubst %, --library:$(PROJECT_ROOT)/%, $(PROJECT_INDEX))
 _transpile_implementation_all: transpile_implementation
 
 # The `$(OUT)` and $(TARGET) variables are problematic.
@@ -189,22 +189,21 @@ transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src
 # `find` looks for `Index.dfy` files in either V1 or V2-styled project directories (single vs. multiple model files).
 transpile_implementation:
 	find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
-		-stdin \
-		-noVerify \
-		-vcsCores:$(CORES) \
-		-compileTarget:$(TARGET) \
-		-spillTargetCode:3 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-compileSuffix:1 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-useRuntimeLib \
-		-out $(OUT) \
-		$(DAFNY_OPTIONS) \
-		$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
+	translate $(TARGET) \
+		--stdin \
+		--no-verify \
+		--cores:$(CORES) \
+		--optimize-erasable-datatype-wrapper:false \
+		--unicode-char:false \
+		--function-syntax:3 \
+		--allow-warnings \
+		--output $(OUT) \
+		$(TRANSPILE_MODULE_NAME) \
+		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
+		$(TRANSLATION_RECORD) \
 		$(TRANSPILE_DEPENDENCIES)
 
+
 # If the project under transpilation uses `replaceable` modules,
 #   it MUST define a SRC_INDEX variable per language.
 # The purpose and usage of this is described in the `transpile_implementation` comments.
@@ -222,27 +221,26 @@ _transpile_test_all: TEST_INDEX_TRANSPILE=$(if $(TEST_INDEX),$(TEST_INDEX),test)
 #     append `-library:/path/to/Index.dfy` to the transpile target
 # Else: (i.e. single model/service in project), then:
 #   append `-library:/path/to/Index.dfy` to the transpile target
-_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, -library:dafny/%/$(SRC_INDEX_TRANSPILE)/Index.dfy, $(PROJECT_SERVICES)), -library:$(SRC_INDEX_TRANSPILE)/Index.dfy)
+_transpile_test_all: TRANSPILE_DEPENDENCIES=$(if ${DIR_STRUCTURE_V2}, $(patsubst %, --library:dafny/%/$(SRC_INDEX_TRANSPILE)/Index.dfy, $(PROJECT_SERVICES)), --library:$(SRC_INDEX_TRANSPILE)/Index.dfy)
 # Transpile the entire project's tests
 _transpile_test_all: transpile_test
 
 # `find` looks for tests in either V1 or V2-styled project directories (single vs. multiple model files).
 transpile_test:
 	find ./dafny/**/$(TEST_INDEX_TRANSPILE) ./$(TEST_INDEX_TRANSPILE) -name "*.dfy" -name '*.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
-		-stdin \
-		-noVerify \
-		-vcsCores:$(CORES) \
-		-compileTarget:$(TARGET) \
-		-spillTargetCode:3 \
-		-runAllTests:1 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-compileSuffix:1 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-useRuntimeLib \
-		-out $(OUT) \
-		$(if $(strip $(STD_LIBRARY)) , -library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
+		translate $(TARGET) \
+		--stdin \
+		--no-verify \
+		--cores:$(CORES) \
+		--include-test-runner \
+		--optimize-erasable-datatype-wrapper:false \
+		--unicode-char:false \
+		--function-syntax:3 \
+		--allow-warnings \
+		--output $(OUT) \
+		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
+		$(TRANSLATION_RECORD) \
+		$(SOURCE_TRANSLATION_RECORD) \
 		$(TRANSPILE_DEPENDENCIES) \
 
 # If we are not the StandardLibrary, transpile the StandardLibrary.
@@ -275,10 +273,12 @@ _polymorph:
 	$(OUTPUT_JAVA) \
 	$(OUTPUT_JAVA_TEST) \
 	$(OUTPUT_DOTNET) \
+	$(MODULE_NAME) \
 	$(OUTPUT_RUST) \
 	--model $(if $(DIR_STRUCTURE_V2), $(LIBRARY_ROOT)/dafny/$(SERVICE)/Model, $(SMITHY_MODEL_ROOT)) \
 	--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
 	$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
+	$(DEPENDENCY_MODULE_NAMES) \
 	--namespace $($(namespace_var)) \
 	$(OUTPUT_LOCAL_SERVICE_$(SERVICE)) \
 	$(AWS_SDK_CMD) \
@@ -292,13 +292,14 @@ _polymorph_wrapped:
 	--dafny-version $(DAFNY_VERSION) \
 	--library-root $(LIBRARY_ROOT) \
 	--properties-file $(LIBRARY_ROOT)/project.properties \
-	$(INPUT_DAFNY) \
 	$(OUTPUT_DAFNY_WRAPPED) \
 	$(OUTPUT_DOTNET_WRAPPED) \
 	$(OUTPUT_JAVA_WRAPPED) \
+	$(MODULE_NAME) \
 	--model $(if $(DIR_STRUCTURE_V2),$(LIBRARY_ROOT)/dafny/$(SERVICE)/Model,$(LIBRARY_ROOT)/Model) \
 	--dependent-model $(PROJECT_ROOT)/$(SMITHY_DEPS) \
 	$(patsubst %, --dependent-model $(PROJECT_ROOT)/%/Model, $($(service_deps_var))) \
+	$(DEPENDENCY_MODULE_NAMES) \
 	--namespace $($(namespace_var)) \
 	--local-service-test \
 	$(AWS_SDK_CMD) \
@@ -369,8 +370,6 @@ polymorph_dotnet:
 
 _polymorph_dotnet: OUTPUT_DOTNET=\
     $(if $(DIR_STRUCTURE_V2), --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/$(SERVICE)/, --output-dotnet $(LIBRARY_ROOT)/runtimes/net/Generated/)
-_polymorph_dotnet: INPUT_DAFNY=\
-		--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 _polymorph_dotnet: _polymorph
 
 # Generates java code for all namespaces in this project
@@ -387,8 +386,6 @@ polymorph_java:
 
 _polymorph_java: OUTPUT_JAVA=--output-java $(LIBRARY_ROOT)/runtimes/java/src/main/smithy-generated
 _polymorph_java: OUTPUT_JAVA_TEST=--output-java-test $(LIBRARY_ROOT)/runtimes/java/src/test/smithy-generated
-_polymorph_java: INPUT_DAFNY=\
-	--include-dafny $(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy
 _polymorph_java: _polymorph
 
 # Dependency for formatting generating Java code
@@ -419,6 +416,8 @@ transpile_net: | transpile_implementation_net transpile_test_net transpile_depen
 
 transpile_implementation_net: TARGET=cs
 transpile_implementation_net: OUT=runtimes/net/ImplementationFromDafny
+transpile_implementation_net: TRANSPILE_MODULE_NAME=$(if $(NET_NAMESPACE_NAME),--dotnet-namespace=$(NET_NAMESPACE_NAME).internaldafny,)
+transpile_implementation_net: TRANSLATION_RECORD=$(TRANSLATION_RECORD_NET)
 transpile_implementation_net: SRC_INDEX=$(NET_SRC_INDEX)
 transpile_implementation_net: _transpile_implementation_all
 
@@ -426,6 +425,8 @@ transpile_test_net: SRC_INDEX=$(NET_SRC_INDEX)
 transpile_test_net: TEST_INDEX=$(NET_TEST_INDEX)
 transpile_test_net: TARGET=cs
 transpile_test_net: OUT=runtimes/net/tests/TestsFromDafny
+transpile_test_net: TRANSLATION_RECORD=$(TRANSLATION_RECORD_NET)
+transpile_test_net: SOURCE_TRANSLATION_RECORD= --translation-record runtimes/net/ImplementationFromDafny-cs.dtr
 transpile_test_net: _transpile_test_all
 
 transpile_dependencies_net: LANG=net
@@ -467,10 +468,14 @@ transpile_java: | transpile_implementation_java transpile_test_java transpile_de
 
 transpile_implementation_java: TARGET=java
 transpile_implementation_java: OUT=runtimes/java/ImplementationFromDafny
+transpile_implementation_java: TRANSPILE_MODULE_NAME=$(if $(JAVA_PACKAGE_NAME),--java-package-name=$(JAVA_PACKAGE_NAME).internaldafny,)
+transpile_implementation_java: TRANSLATION_RECORD=$(TRANSLATION_RECORD_JAVA)
 transpile_implementation_java: _transpile_implementation_all _mv_implementation_java
 
 transpile_test_java: TARGET=java
 transpile_test_java: OUT=runtimes/java/TestsFromDafny
+transpile_test_java: TRANSLATION_RECORD=$(TRANSLATION_RECORD_JAVA)
+transpile_test_java: SOURCE_TRANSLATION_RECORD= --translation-record runtimes/java/src/main/dafny-generated/ImplementationFromDafny-java.dtr
 transpile_test_java: _transpile_test_all _mv_test_java
 
 # Currently Dafny compiles to Java by changing the directory name.
diff --git a/TestModels/Constraints/Makefile b/TestModels/Constraints/Makefile
index fa31cc5419..90cbc5e579 100644
--- a/TestModels/Constraints/Makefile
+++ b/TestModels/Constraints/Makefile
@@ -24,3 +24,17 @@ polymorph:
 	make polymorph_dafny
 	make polymorph_java
 	make polymorph_dotnet
+
+# Java
+
+JAVA_PACKAGE_NAME=simple.constraints
+
+TRANSLATION_RECORD_JAVA:= \
+    --translation-record ../dafny-dependencies/StandardLibrary/runtimes/java/src/main/dafny-generated/ImplementationFromDafny-java.dtr
+
+# NET
+
+NET_NAMESPACE_NAME=simple.constraints
+
+TRANSLATION_RECORD_NET:= \
+    --translation-record ../dafny-dependencies/StandardLibrary/runtimes/net/ImplementationFromDafny-cs.dtr
diff --git a/TestModels/Constraints/runtimes/java/src/test/java/WrappedSimpleConstraintsService/__default.java b/TestModels/Constraints/runtimes/java/src/test/java/WrappedSimpleConstraintsService/__default.java
new file mode 100644
index 0000000000..70a47cb527
--- /dev/null
+++ b/TestModels/Constraints/runtimes/java/src/test/java/WrappedSimpleConstraintsService/__default.java
@@ -0,0 +1,33 @@
+// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0
+package WrappedSimpleConstraintsService;
+
+import software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.Result;
+import simple.constraints.SimpleConstraints;
+import simple.constraints.ToNative;
+import simple.constraints.internaldafny.types.Error;
+import simple.constraints.internaldafny.types.ISimpleConstraintsClient;
+import simple.constraints.internaldafny.types.SimpleConstraintsConfig;
+import simple.constraints.wrapped.TestSimpleConstraints;
+
+public class __default extends _ExternBase___default {
+
+  public static Result<
+    ISimpleConstraintsClient,
+    Error
+  > WrappedSimpleConstraints(SimpleConstraintsConfig config) {
+    simple.constraints.model.SimpleConstraintsConfig wrappedConfig =
+      ToNative.SimpleConstraintsConfig(config);
+    simple.constraints.SimpleConstraints impl = SimpleConstraints
+      .builder()
+      .SimpleConstraintsConfig(wrappedConfig)
+      .build();
+    TestSimpleConstraints wrappedClient = TestSimpleConstraints
+      .builder()
+      .impl(impl)
+      .build();
+    return simple.constraints.internaldafny.SimpleConstraints.__default.CreateSuccessOfClient(
+      wrappedClient
+    );
+  }
+}
diff --git a/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs b/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs
index ef1e400b04..2ddd218057 100644
--- a/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs
+++ b/TestModels/Constraints/runtimes/net/Extern/WrappedSimpleConstraintsService.cs
@@ -1,17 +1,20 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
-using Wrappers_Compile;
+using software.amazon.cryptography.standardlibrary.internaldafny.Wrappers;
+using simple.constraints.internaldafny.types;
 using Simple.Constraints;
 using Simple.Constraints.Wrapped;
-using TypeConversion = Simple.Constraints.TypeConversion ;
-namespace simple.constraints.internaldafny.wrapped
+using TypeConversion = Simple.Constraints.TypeConversion;
+namespace WrappedSimpleConstraintsService
 {
-    public partial class __default {
-        public static _IResult<types.ISimpleConstraintsClient, types._IError> WrappedSimpleConstraints(types._ISimpleConstraintsConfig config) {
+    public partial class __default
+    {
+        public static _IResult<simple.constraints.internaldafny.types.ISimpleConstraintsClient, simple.constraints.internaldafny.types._IError> WrappedSimpleConstraints(simple.constraints.internaldafny.types._ISimpleConstraintsConfig config)
+        {
             var wrappedConfig = TypeConversion.FromDafny_N6_simple__N11_constraints__S23_SimpleConstraintsConfig(config);
-            var impl = new SimpleConstraints(wrappedConfig);
+            var impl = new Simple.Constraints.SimpleConstraints(wrappedConfig);
             var wrappedClient = new SimpleConstraintsShim(impl);
-            return Result<types.ISimpleConstraintsClient, types._IError>.create_Success(wrappedClient);
+            return Result<simple.constraints.internaldafny.types.ISimpleConstraintsClient, simple.constraints.internaldafny.types._IError>.create_Success(wrappedClient);
         }
     }
 }
diff --git a/TestModels/Constraints/src/Index.dfy b/TestModels/Constraints/src/Index.dfy
index f8979e553a..d3515f35e6 100644
--- a/TestModels/Constraints/src/Index.dfy
+++ b/TestModels/Constraints/src/Index.dfy
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 include "SimpleConstraintsImpl.dfy"
 
-module {:extern "simple.constraints.internaldafny" } SimpleConstraints refines AbstractSimpleConstraintsService {
+module {:extern "SimpleConstraints" } SimpleConstraints refines AbstractSimpleConstraintsService {
   import Operations = SimpleConstraintsImpl
 
   function method DefaultSimpleConstraintsConfig(): SimpleConstraintsConfig {
diff --git a/TestModels/Constraints/src/WrappedSimpleConstraintsImpl.dfy b/TestModels/Constraints/src/WrappedSimpleConstraintsImpl.dfy
index 2d2f19bf2c..9909aef606 100644
--- a/TestModels/Constraints/src/WrappedSimpleConstraintsImpl.dfy
+++ b/TestModels/Constraints/src/WrappedSimpleConstraintsImpl.dfy
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0
 include "../Model/SimpleConstraintsTypesWrapped.dfy"
 
-module {:extern "simple.constraints.internaldafny.wrapped"} WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService {
+module {:extern "WrappedSimpleConstraintsService"} WrappedSimpleConstraintsService refines WrappedAbstractSimpleConstraintsService {
     import WrappedService = SimpleConstraints
     function method WrappedDefaultSimpleConstraintsConfig(): SimpleConstraintsConfig {
         SimpleConstraintsConfig
diff --git a/TestModels/dafny-dependencies/StandardLibrary/Makefile b/TestModels/dafny-dependencies/StandardLibrary/Makefile
index 3dcd26f9c1..b8f4342e38 100644
--- a/TestModels/dafny-dependencies/StandardLibrary/Makefile
+++ b/TestModels/dafny-dependencies/StandardLibrary/Makefile
@@ -6,6 +6,8 @@ CORES=2
 include ../../SharedMakefile.mk
 
 MAX_RESOURCE_COUNT=500000000
+JAVA_PACKAGE_NAME=software.amazon.cryptography.standardlibrary
+NET_NAMESPACE_NAME=software.amazon.cryptography.standardlibrary
 
 # define standard colors
 ifneq (,$(findstring xterm,${TERM}))
@@ -86,21 +88,19 @@ transpile_dependencies:
 
 # Override SharedMakefile's transpile_implementation to not reference
 # StandardLibrary as a Library
+transpile_implementation: SRC_INDEX_TRANSPILE=$(if $(SRC_INDEX),$(SRC_INDEX),src)
 transpile_implementation:
 	find ./dafny/**/$(SRC_INDEX_TRANSPILE)/ ./$(SRC_INDEX_TRANSPILE)/ -name 'Index.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
-		-stdin \
-		-noVerify \
-		-vcsCores:$(CORES) \
-		-compileTarget:$(TARGET) \
-		-spillTargetCode:3 \
-		-compile:0 \
-		-optimizeErasableDatatypeWrapper:0 \
-		-compileSuffix:1 \
-		-unicodeChar:0 \
-		-functionSyntax:3 \
-		-useRuntimeLib \
-		$(DAFNY_OPTIONS) \
-		-out $(OUT)
+	translate $(TARGET) \
+		--stdin \
+		--no-verify \
+		--cores:$(CORES) \
+		--optimize-erasable-datatype-wrapper:false \
+		--unicode-char:false \
+		--function-syntax:3 \
+		--allow-warnings \
+		--output $(OUT) \
+		$(TRANSPILE_MODULE_NAME)
 
 # Override SharedMakefile's build_java to not install
 # StandardLibrary as a dependency
diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java b/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java
index 010dbed431..32de956315 100644
--- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java
+++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/java/src/main/java/UTF8/__default.java
@@ -1,13 +1,13 @@
 // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0
-package UTF8;
+package software.amazon.cryptography.standardlibrary.internaldafny.UTF8;
 
 import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.ByteSequence;
 import static software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence;
 import static software.amazon.smithy.dafny.conversion.ToNative.Simple.ByteBuffer;
 import static software.amazon.smithy.dafny.conversion.ToNative.Simple.String;
 
-import Wrappers_Compile.Result;
+import software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.Result;
 import dafny.DafnySequence;
 import java.nio.ByteBuffer;
 import java.nio.CharBuffer;
@@ -22,7 +22,7 @@
 // If we wanted to increase performance,
 // we could declare this NOT thread/concurrent safe,
 // and reset the coder everytime.
-public class __default extends UTF8._ExternBase___default {
+public class __default extends _ExternBase___default {
 
   // This is largely copied from Polymorph's dafny-java-conversion:
   // software.amazon.smithy.dafny.conversion.ToDafny.Simple.DafnyUtf8Bytes
diff --git a/TestModels/dafny-dependencies/StandardLibrary/runtimes/net/Extern/UTF8.cs b/TestModels/dafny-dependencies/StandardLibrary/runtimes/net/Extern/UTF8.cs
index b9ba40f833..3f4452abac 100644
--- a/TestModels/dafny-dependencies/StandardLibrary/runtimes/net/Extern/UTF8.cs
+++ b/TestModels/dafny-dependencies/StandardLibrary/runtimes/net/Extern/UTF8.cs
@@ -4,13 +4,13 @@
 using System;
 using System.Text;
 
-using Wrappers_Compile;
+using software.amazon.cryptography.standardlibrary.internaldafny.Wrappers;
 using ibyteseq = Dafny.ISequence<byte>;
 using byteseq = Dafny.Sequence<byte>;
 using icharseq = Dafny.ISequence<char>;
 using charseq = Dafny.Sequence<char>;
 
-namespace UTF8 {
+namespace software.amazon.cryptography.standardlibrary.internaldafny.UTF8 {
     public partial class __default {
         public static _IResult<ibyteseq, icharseq> Encode(icharseq str) {
             UTF8Encoding utf8 = new UTF8Encoding(false, true);
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java
index 4656098f54..002427868b 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydafny/DafnyApiCodegen.java
@@ -129,10 +129,7 @@ public Map<Path, TokenTree> generate() {
       namespace
     );
     final TokenTree typesModuleHeader = Token.of(
-      "module {:extern \"%s\" } %s".formatted(
-          DafnyNameResolverHelpers.dafnyExternNamespaceForShapeId(
-            serviceShape.getId()
-          ),
+      "module {:extern \"types\"} %s".formatted(
           typesModuleName
         )
     );
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java
index 572e2d6be5..a30ebce5d3 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/DotNetNameResolver.java
@@ -881,7 +881,7 @@ private String dafnyTypeForOptionalMember(
 
     final String baseType = dafnyTypeForShape(memberShape.getTarget());
     final String prefix = concrete ? "" : "_I";
-    return "Wrappers_Compile.%sOption<%s>".formatted(prefix, baseType);
+    return "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.%sOption<%s>".formatted(prefix, baseType);
   }
 
   private String dafnyTypeForService(final ServiceShape serviceShape) {
@@ -1060,7 +1060,7 @@ private String dafnyTypeForResult(
     final boolean concrete
   ) {
     final String resultType = concrete ? "Result" : "_IResult";
-    return "Wrappers_Compile.%s<%s, %s>".formatted(
+    return "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.%s<%s, %s>".formatted(
         resultType,
         valueType,
         errorType
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java
index 8882fde757..26b6d75114 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/localServiceWrapper/LocalServiceWrappedCodegen.java
@@ -88,7 +88,7 @@ public TokenTree generateWrappedServiceExtern(
       .of(
         "public static",
         // TODO fix the Error and don't hard code it :(
-        "Wrappers_Compile._IResult<Types.%s,Types._IError>".formatted(
+        "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers._IResult<Types.%s,Types._IError>".formatted(
             nameResolver.dafnyTypeForShape(serviceShape.getId())
           ),
         "Wrapped%s(Types.%s config)".formatted(
@@ -108,7 +108,7 @@ public TokenTree generateWrappedServiceExtern(
             ((LocalServiceWrappedNameResolver) nameResolver).shimClassForService()
           ),
         // TODO fix the Error and don't hard code it :(
-        "return Wrappers_Compile.Result<Types.%s,Types._IError>.create_Success(wrappedClient);".formatted(
+        "return software.amazon.cryptography.standardlibrary.internaldafny.Wrappers.Result<Types.%s,Types._IError>.create_Success(wrappedClient);".formatted(
             nameResolver.dafnyTypeForShape(serviceShape.getId())
           )
       )
@@ -123,4 +123,5 @@ public TokenTree generateWrappedServiceExtern(
         ".Wrapped"
       );
   }
+
 }
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/nativeWrapper/NativeWrapperCodegen.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/nativeWrapper/NativeWrapperCodegen.java
index 099d84d084..ff1d11df30 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/nativeWrapper/NativeWrapperCodegen.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithydotnet/nativeWrapper/NativeWrapperCodegen.java
@@ -54,7 +54,7 @@ public class NativeWrapperCodegen {
   protected static final List<String> UNCONDITIONAL_IMPORTS = List.of(
     "System",
     "_System",
-    "Wrappers_Compile"
+    "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers"
   );
 
   public NativeWrapperCodegen(
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java
index 9ec737662a..e4c67b0138 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/ToDafny.java
@@ -225,7 +225,7 @@ protected CodeBlock memberDeclaration(
     return CodeBlock.of(
       "$T $L",
       ParameterizedTypeName.get(
-        ClassName.get("Wrappers_Compile", "Option"),
+        ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"),
         subject.dafnyNameResolver.typeForShape(memberShape.getId())
       ),
       variable
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/JavaAwsSdkV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/JavaAwsSdkV1.java
index 1b577d1b78..d97bbc10d2 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/JavaAwsSdkV1.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/JavaAwsSdkV1.java
@@ -13,6 +13,8 @@
 import software.amazon.smithy.model.Model;
 import software.amazon.smithy.model.shapes.ServiceShape;
 
+import static software.amazon.polymorph.smithyjava.nameresolver.Dafny.convertNamespaceToPascalCase;
+
 /**
  * Generates all the Java Classes needed for
  * Dafny Generated Java to call AWS Services via
@@ -46,7 +48,7 @@ private JavaAwsSdkV1(
     this.packageName =
       DafnyNameResolverHelpers.packageNameForNamespace(
         serviceShape.getId().getNamespace()
-      );
+      ) + "." + convertNamespaceToPascalCase(serviceShape.getId().getNamespace());
   }
 
   public static JavaAwsSdkV1 createJavaAwsSdkV1(
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java
index 23c8a8edb0..a8ba2a2bcc 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v1/ToDafnyAwsV1.java
@@ -454,7 +454,7 @@ MethodSpec generateConvertOpaqueError() {
     CodeBlock memberDeclaration = CodeBlock.of(
       "$T $L",
       ParameterizedTypeName.get(
-        ClassName.get("Wrappers_Compile", "Option"),
+        ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"),
         ParameterizedTypeName.get(
           software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_SEQUENCE_CLASS_NAME,
           WildcardTypeName.subtypeOf(Character.class)
@@ -472,14 +472,14 @@ MethodSpec generateConvertOpaqueError() {
       "message",
       ClassName.get(Objects.class),
       "nativeValue.getMessage()",
-      ClassName.get("Wrappers_Compile", "Option"),
+      ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"),
       stringTypeDescriptor,
       COMMON_TO_DAFNY_SIMPLE,
       SIMPLE_CONVERSION_METHOD_FROM_SHAPE_TYPE
         .get(ShapeType.STRING)
         .methodName(),
       "nativeValue.getMessage()",
-      ClassName.get("Wrappers_Compile", "Option"),
+      ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"),
       stringTypeDescriptor
     );
     return MethodSpec
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java
index 0b9185dbe5..3a19a4a4ac 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/generator/awssdk/v2/ToDafnyAwsV2.java
@@ -688,7 +688,7 @@ MethodSpec generateConvertOpaqueError() {
     CodeBlock memberDeclaration = CodeBlock.of(
       "$T $L",
       ParameterizedTypeName.get(
-        ClassName.get("Wrappers_Compile", "Option"),
+        ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"),
         ParameterizedTypeName.get(
           software.amazon.polymorph.smithyjava.nameresolver.Constants.DAFNY_SEQUENCE_CLASS_NAME,
           WildcardTypeName.subtypeOf(Character.class)
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java
index ab2d8264f9..397ab92f7d 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Constants.java
@@ -16,11 +16,11 @@ public class Constants {
     "Unit"
   );
   public static final ClassName DAFNY_OPTION_CLASS_NAME = ClassName.get(
-    "Wrappers_Compile",
+    "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers",
     "Option"
   );
   public static final ClassName DAFNY_RESULT_CLASS_NAME = ClassName.get(
-    "Wrappers_Compile",
+    "software.amazon.cryptography.standardlibrary.internaldafny.Wrappers",
     "Result"
   );
   public static final ClassName DAFNY_TUPLE0_CLASS_NAME = ClassName.get(
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java
index 64f53a3d74..c9692067ee 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithyjava/nameresolver/Dafny.java
@@ -11,8 +11,10 @@
 import com.squareup.javapoet.WildcardTypeName;
 import java.math.BigDecimal;
 import java.math.BigInteger;
+import java.util.Arrays;
 import java.util.Map;
 import java.util.Objects;
+import java.util.stream.Collectors;
 import javax.annotation.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -174,13 +176,13 @@ public CodeBlock createNone(CodeBlock typeDescriptor) {
     if (datatypeConstructorsNeedTypeDescriptors()) {
       return CodeBlock.of(
         "$T.create_None($L)",
-        ClassName.get("Wrappers_Compile", "Option"),
+        ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option"),
         typeDescriptor
       );
     } else {
       return CodeBlock.of(
         "$T.create_None()",
-        ClassName.get("Wrappers_Compile", "Option")
+        ClassName.get("software.amazon.cryptography.standardlibrary.internaldafny.Wrappers", "Option")
       );
     }
   }
@@ -277,6 +279,13 @@ public static String aggregateSizeMethod(ShapeType shapeType) {
     };
   }
 
+  public static String convertNamespaceToPascalCase(final String namespace) {
+    String camelCase = Arrays.stream(namespace.split("\\."))
+            .map(part -> Character.toUpperCase(part.charAt(0)) + part.substring(1).toLowerCase())
+            .collect(Collectors.joining());
+    return camelCase;
+  }
+
   static String modelPackageNameForNamespace(final String namespace) {
     return DafnyNameResolverHelpers.dafnyExternNamespaceForNamespace(namespace);
   }