diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/AwsSdkCodegenConstants.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/AwsSdkCodegenConstants.java
index c3bae2d19..03f3fe90e 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/AwsSdkCodegenConstants.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/awssdk/AwsSdkCodegenConstants.java
@@ -2,5 +2,10 @@
 
 public class AwsSdkCodegenConstants {
     public static String AWS_SDK_CODEGEN_SYMBOLWRITER_DUMP_FILE_FILENAME = "awssdk_codegen_todelete.tmp";
+
+    // boto3 models `Timestamp` Smithy objects as `datetime.datetime` objects
+    // with millisecond precision masquerading as microsecond precision;
+    // e.x. datetime.datetime(2024, 6, 14, 16, 40, 15, 761000, tzinfo=tzlocal())
+    // --> 761000 is actually just 761 ms, but boto3 reports it with microsecond precision.
     public static String BOTO3_TIMESTAMP_STRING_FORMAT = "%Y-%m-%dT%H:%M:%S.%fZ";
 }
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java
index 55912bfae..9e239b9c5 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/DafnyToLocalServiceShapeVisitor.java
@@ -270,7 +270,10 @@ public String enumShape(EnumShape shape) {
 
   @Override
   public String timestampShape(TimestampShape shape) {
-    throw new UnsupportedOperationException("TimestampShape from within a LocalService not supported");
+    writer.addStdlibImport("datetime", "datetime");
+    return "datetime.fromisoformat(%1$s.VerbatimString(False))".formatted(
+            dataSource
+    );
   }
 
   @Override
diff --git a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java
index 59b307fde..3f9c45e61 100644
--- a/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java
+++ b/codegen/smithy-dafny-codegen/src/main/java/software/amazon/polymorph/smithypython/localservice/shapevisitor/LocalServiceToDafnyShapeVisitor.java
@@ -271,10 +271,13 @@ public String enumShape(EnumShape shape) {
       );
     }
 
-    @Override
-    public String timestampShape(TimestampShape shape) {
-      throw new UnsupportedOperationException("TimestampShape from within a LocalService not supported");
-    }
+  @Override
+  public String timestampShape(TimestampShape shape) {
+    writer.addStdlibImport("_dafny");
+    return "_dafny.Seq(%1$s.isoformat())".formatted(
+            dataSource
+    );
+  }
 
     @Override
     public String unionShape(UnionShape unionShape) {