diff --git a/.gitignore b/.gitignore
index 8dc5091d9..28cec2197 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,9 @@ build
 doc/build
 AwsCryptographicMaterialProviders/runtimes/python/doc/generated/*
 
+# Dafny build artifacts
+bin
+
 # Duvet output
 specification_compliance_report.html
 
diff --git a/.gitmodules b/.gitmodules
index 79aede314..f67b5b319 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -3,7 +3,7 @@
 	url = https://github.com/dafny-lang/libraries.git 
 [submodule "smithy-dafny"]
 	path = smithy-dafny
-	url = https://robin-aws@github.com/smithy-lang/smithy-dafny.git
+	url = https://github.com/smithy-lang/smithy-dafny.git
 [submodule "aws-encryption-sdk-specification"]
 	path = aws-encryption-sdk-specification
 	url = https://github.com/awslabs/aws-encryption-sdk-specification.git 
diff --git a/AwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml b/AwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml
index 0451ab452..c8e6a4e09 100644
--- a/AwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml
+++ b/AwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml
@@ -14,8 +14,8 @@ readme = "README.md"
 
 [dependencies]
 aws-config = "1.5.15"
-aws-lc-rs = "1.12.2"
-aws-lc-sys = "0.25.0"
+aws-lc-rs = "=1.12.2"
+aws-lc-sys = "0.25.1"
 aws-sdk-dynamodb = "1.55.0"
 aws-sdk-kms = "1.51.0"
 aws-smithy-runtime-api = {version = "1.7.3", features = ["client"] }
diff --git a/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml b/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml
index de0253aed..44219dad7 100644
--- a/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml
+++ b/AwsCryptographyPrimitives/runtimes/rust/Cargo.toml
@@ -8,8 +8,8 @@ rust-version = "1.80.0"
 
 [dependencies]
 aws-config = "1.5.15"
-aws-lc-rs = "1.12.2"
-aws-lc-sys = "0.25.0"
+aws-lc-rs = "=1.12.2"
+aws-lc-sys = "0.25.1"
 aws-smithy-runtime-api = "1.7.3"
 aws-smithy-types = "1.2.12"
 chrono = "0.4.39"
diff --git a/StandardLibrary/Makefile b/StandardLibrary/Makefile
index 5e933ae9d..42cb82993 100644
--- a/StandardLibrary/Makefile
+++ b/StandardLibrary/Makefile
@@ -13,10 +13,46 @@ LIBRARIES :=
 # However, this means this it could not build...
 # So we empty the variable here
 # and check in the Makefile
-transpile_implementation: STD_LIBRARY=
-transpile_test: STD_LIBRARY=
 transpile_dependencies: STD_LIBRARY=
 
+# 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 \
+	translate $(TARGET) \
+		--stdin \
+		--no-verify \
+		--cores:$(CORES) \
+		--optimize-erasable-datatype-wrapper:false \
+		--unicode-char:false \
+		--function-syntax:3 \
+		--output $(OUT) \
+		$(if $(USE_DAFNY_STANDARD_LIBRARIES), ./bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
+		$(DAFNY_OPTIONS) \
+		$(DAFNY_OTHER_FILES) \
+		$(TRANSPILE_MODULE_NAME)
+
+transpile_test:
+	dafny --version
+	find ./dafny/**/$(TEST_INDEX_TRANSPILE) ./$(TEST_INDEX_TRANSPILE) -name "*.dfy" -name '*.dfy' | sed -e 's/^/include "/' -e 's/$$/"/' | dafny \
+		translate $(TARGET) \
+		--stdin \
+		--no-verify \
+		--cores:$(CORES) \
+		--optimize-erasable-datatype-wrapper:false \
+		--unicode-char:false \
+		--function-syntax:3 \
+		--output $(OUT) \
+		$(DAFNY_OPTIONS) \
+		$(DAFNY_OTHER_FILES) \
+		$(if $(strip $(STD_LIBRARY)) , --library:$(PROJECT_ROOT)/$(STD_LIBRARY)/src/Index.dfy, ) \
+		$(if $(USE_DAFNY_STANDARD_LIBRARIES) , --library:./bin/DafnyStandardLibraries-smithy-dafny-subset.doo, ) \
+		$(TRANSLATION_RECORD) \
+		$(SOURCE_TRANSLATION_RECORD) \
+		$(TRANSPILE_MODULE_NAME) \
+		$(TRANSPILE_DEPENDENCIES) \
+
 GO_MODULE_NAME="github.com/aws/aws-cryptographic-material-providers-library/releases/go/smithy-dafny-standard-library"
 
 # Python
@@ -32,3 +68,9 @@ RUST_OTHER_FILES := \
 
 polymorph_rust:
 	@echo no polymorph needed for StandardLibrary
+
+polymorph_dafny: $(if $(USE_DAFNY_STANDARD_LIBRARIES), build_dafny_stdlibs, )
+
+build_dafny_stdlibs:
+	dafny build -t:lib --output $(LIBRARY_ROOT)/bin/DafnyStandardLibraries-smithy-dafny-subset.doo \
+		../smithy-dafny/TestModels/dafny-dependencies/StandardLibrary/DafnyStandardLibraries-smithy-dafny-subset.toml
diff --git a/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py b/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py
new file mode 100644
index 000000000..7a6eff36b
--- /dev/null
+++ b/StandardLibrary/runtimes/python/src/smithy_dafny_standard_library/internaldafny/extern/streams.py
@@ -0,0 +1,67 @@
+
+from _dafny import Seq
+from smithy_python.interfaces.blobs import ByteStream
+from smithy_dafny_standard_library.internaldafny.generated.Std_Streams import ByteStream as DafnyByteStream, RewindableByteStream as DafnyRewindableByteStream
+from smithy_dafny_standard_library.internaldafny.generated.Std_Enumerators import Enumerator
+from smithy_dafny_standard_library.internaldafny.generated.Std_Wrappers import Option, Option_Some, Option_None
+
+# Adaptor classes for wrapping up Python-native types as their
+# corresponding Dafny interfaces, and vice-versa.
+# These are the equivalent of type conversions,
+# but avoiding having to load all data into memory at once.
+
+class DafnyByteStreamAsByteStream(ByteStream):
+  """Wrapper class adapting a Dafny ByteStream as a native ByteStream."""
+
+  def __init__(self, dafny_byte_stream):
+    self.dafny_byte_stream = dafny_byte_stream
+
+  def read(self, size: int = -1) -> bytes:
+    # TODO: assert size is -1, buffer, 
+    # or define a more specialized Action<int, bytes> type for streams.
+    next = self.dafny_byte_stream.Next()
+    while next.is_Some and len(next.value) == 0:
+      next = self.dafny_byte_stream.Next()
+    # Do NOT return None, because that indicates "no data right now, might be more later"
+    return bytes(next.value) if next.is_Some else bytes()
+
+
+class RewindableDafnyByteStreamAsByteStream(DafnyByteStreamAsByteStream):
+  """Wrapper class adapting a Dafny RewindableByteStream as a native ByteStream
+  that supports tell and seek.
+  """
+
+  def __init__(self, dafny_byte_stream):
+    if not isinstance(dafny_byte_stream, DafnyRewindableByteStream):
+      raise ValueError("Rewindable stream required")
+    super().__init__(dafny_byte_stream)
+
+  def tell(self) -> int:
+    return self.dafny_byte_stream.Position()
+
+  def seek(self, offset, whence=0):
+    match whence:
+      case 0:
+        position = offset
+      case 1:
+        position = self.dafny_byte_stream.Position() + offset
+      case 2:
+        position = self.dafny_byte_stream.ContentLength() + offset
+    return self.dafny_byte_stream.Seek(position)
+
+
+class StreamingBlobAsDafnyDataStream(DafnyByteStream):
+  """Wrapper class adapting a native StreamingBlob as a Dafny ByteStream."""
+
+  def __init__(self, streaming_blob):
+    self.streaming_blob = streaming_blob
+
+  def Next(self):
+    return Enumerator.Next(self)
+
+  def Invoke(self, _) -> Option:
+    next = self.streaming_blob.read()
+    if next:
+      return Option_Some(Seq(next))
+    else:
+      return Option_None()
diff --git a/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml b/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml
index 6ec2c0ff1..8853941ad 100644
--- a/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml
+++ b/TestVectorsAwsCryptographicMaterialProviders/runtimes/rust/Cargo.toml
@@ -11,8 +11,8 @@ wrapped-client = []
 
 [dependencies]
 aws-config = "1.5.15"
-aws-lc-rs = "1.12.2"
-aws-lc-sys = "0.25.0"
+aws-lc-rs = "=1.12.2"
+aws-lc-sys = "0.25.1"
 aws-sdk-dynamodb = "1.55.0"
 aws-sdk-kms = "1.51.0"
 aws-smithy-runtime-api = {version = "1.7.3", features = ["client"] }
diff --git a/smithy-dafny b/smithy-dafny
index 5fb3f25ea..2ae8391d3 160000
--- a/smithy-dafny
+++ b/smithy-dafny
@@ -1 +1 @@
-Subproject commit 5fb3f25ea3444c51b2ad30b25ab03964cf866cd1
+Subproject commit 2ae8391d35729e948c681c470f9496cd9a4bc25f