diff --git a/Source/DafnyCore/Backends/Python/PythonBackend.cs b/Source/DafnyCore/Backends/Python/PythonBackend.cs
index 38a571e549..4dc2f5a7c8 100644
--- a/Source/DafnyCore/Backends/Python/PythonBackend.cs
+++ b/Source/DafnyCore/Backends/Python/PythonBackend.cs
@@ -1,11 +1,13 @@
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Runtime.InteropServices;
 using System.Threading.Tasks;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny.Compilers;
 
@@ -26,10 +28,29 @@ public override string TargetBaseDir(string dafnyProgramName) =>
   public override bool SupportsInMemoryCompilation => false;
   public override bool TextualTargetIsExecutable => true;
 
+  public bool PythonModuleMode { get; set; } = true;
+  public string PythonModuleName;
+
+  public static readonly Option<string> PythonModuleNameCliOption = new("--python-module-name",
+    @"This Option is used to specify the Python Module Name for the translated code".TrimStart()) {
+  };
+  public override IEnumerable<Option<string>> SupportedOptions => new List<Option<string>> { PythonModuleNameCliOption };
+
+  static PythonBackend() {
+    TranslationRecord.RegisterLibraryChecks(new Dictionary<Option, OptionCompatibility.OptionCheck> {
+      { PythonModuleNameCliOption, OptionCompatibility.NoOpOptionCheck }
+    });
+  }
+
   public override IReadOnlySet<string> SupportedNativeTypes =>
     new HashSet<string> { "byte", "sbyte", "ushort", "short", "uint", "int", "number", "ulong", "long" };
 
   protected override SinglePassCodeGenerator CreateCodeGenerator() {
+    var pythonModuleName = Options.Get(PythonModuleNameCliOption);
+    PythonModuleMode = pythonModuleName != null;
+    if (PythonModuleMode) {
+      PythonModuleName = pythonModuleName;
+    }
     return new PythonCodeGenerator(Options, Reporter);
   }
 
diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
index 97e947d08a..81e3a5b721 100644
--- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
@@ -4,19 +4,34 @@
 using System.Linq;
 using System.Numerics;
 using DafnyCore.Backends.Python;
+using DafnyCore.Options;
 using JetBrains.Annotations;
 using Microsoft.BaseTypes;
 
 namespace Microsoft.Dafny.Compilers {
 
   class PythonCodeGenerator : SinglePassCodeGenerator {
+
+    private bool PythonModuleMode;
+    private string PythonModuleName;
+
     public PythonCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
+      var pythonModuleName = Options.Get(PythonBackend.PythonModuleNameCliOption);
+      PythonModuleMode = pythonModuleName != null;
+      if (PythonModuleMode) {
+        PythonModuleName = pythonModuleName.ToString();
+      }
+
       if (Options?.CoverageLegendFile != null) {
-        Imports.Add("DafnyProfiling");
+        Imports.Add("DafnyProfiling", "DafnyProfiling");
       }
     }
 
-    private readonly List<string> Imports = new() { DafnyDefaultModule };
+    // Key: Fully-qualified module name with python-module-name/outer-module
+    // Value: Dafny-generated Python module name without python-module-name/outer-module
+    // This separation is used to identify nested extern modules,
+    //   which currently cannot be used with python-module-name/outer-module.
+    private readonly Dictionary<string, string> Imports = new Dictionary<string, string>();
 
     public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
       Feature.SubsetTypeTests,
@@ -28,6 +43,8 @@ public PythonCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(
 
     private const string DafnyRuntimeModule = "_dafny";
     private const string DafnyDefaultModule = "module_";
+    private const string DafnySystemModule = "System_";
+    private static readonly ISet<string> DafnyRuntimeGeneratedModuleNames = new HashSet<string> { DafnySystemModule, };
     const string DafnySetClass = $"{DafnyRuntimeModule}.Set";
     const string DafnyMultiSetClass = $"{DafnyRuntimeModule}.MultiSet";
     const string DafnySeqClass = $"{DafnyRuntimeModule}.Seq";
@@ -56,8 +73,8 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
         EmitRuntimeSource("DafnyStandardLibraries_py", wr);
       }
 
-      Imports.Add(DafnyRuntimeModule);
-      EmitImports(null, wr);
+      Imports.Add(DafnyRuntimeModule, DafnyRuntimeModule);
+      EmitImports(null, null, wr);
       wr.WriteLine();
     }
 
@@ -83,29 +100,111 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
 
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
       string libraryName, ConcreteSyntaxTree wr) {
+      var pythonModuleName = PythonModuleMode ? PythonModuleName + "." : "";
+
       moduleName = PublicModuleIdProtect(moduleName);
-      var file = wr.NewFile($"{moduleName}.py");
-      EmitImports(moduleName, file);
+      // Nested extern modules should be written inside a folder
+      var file = wr.NewFile($"{moduleName.Replace(".", "/")}.py");
+      EmitImports(moduleName, pythonModuleName, file);
       return file;
     }
 
     protected override void DependOnModule(Program program, ModuleDefinition module, ModuleDefinition externModule,
       string libraryName) {
-      var moduleName = IdProtect(module.GetCompileName(Options));
-      Imports.Add(moduleName);
+      var dependencyPythonModuleName = "";
+
+      // If the module being depended on was compiled using module mode,
+      // this module needs to rely on it using the dependency's translation record,
+      // even if this module is not using module mode
+      var translatedRecord = program.Compilation.AlreadyTranslatedRecord;
+      translatedRecord.OptionsByModule.TryGetValue(module.FullDafnyName, out var moduleOptions);
+      object dependencyModuleName = null;
+      moduleOptions?.TryGetValue(PythonBackend.PythonModuleNameCliOption.Name, out dependencyModuleName);
+      if (dependencyModuleName is string && !string.IsNullOrEmpty((string)dependencyModuleName)) {
+        dependencyPythonModuleName = dependencyModuleName is string name ? (string)dependencyModuleName + "." : "";
+        if (String.IsNullOrEmpty(dependencyPythonModuleName)) {
+          Reporter.Warning(MessageSource.Compiler, ResolutionErrors.ErrorId.none, Token.Cli,
+            $"Python Module Name not found for the module {module.GetCompileName(Options)}");
+        }
+      }
+
+      var dependencyCompileName = IdProtect(module.GetCompileName(Options));
+      // Don't import an empty module.
+      // Empty modules aren't generated, so their imports aren't valid.
+      if (!TranslationRecord.ModuleEmptyForCompilation(module)) {
+        Imports.Add(dependencyPythonModuleName + dependencyCompileName, dependencyCompileName);
+      }
     }
 
-    private void EmitImports(string moduleName, ConcreteSyntaxTree wr) {
+    private void EmitImports(string moduleName, string pythonModuleName, ConcreteSyntaxTree wr) {
       wr.WriteLine("import sys");
       wr.WriteLine("from typing import Callable, Any, TypeVar, NamedTuple");
       wr.WriteLine("from math import floor");
       wr.WriteLine("from itertools import count");
       wr.WriteLine();
-      Imports.ForEach(module => wr.WriteLine($"import {module}"));
+      // Don't emit `import module_` for generated modules in the DafnyRuntimePython.
+      // The DafnyRuntimePython doesn't have a module.py file, so the import isn't valid.
+      if (!(DafnyRuntimeGeneratedModuleNames.Contains(moduleName))) {
+        wr.WriteLine($"import {(PythonModuleMode ? PythonModuleName + "." + DafnyDefaultModule : DafnyDefaultModule)} as {DafnyDefaultModule}");
+      }
+      foreach (var module in Imports) {
+        if (module.Value.Contains(".")) {
+          // This code branch only applies to extern modules. (ex. module {:extern "a.b.c"})
+          // If module.Value has `.`s in it, it is a nested extern module.
+          // (Non-extern nested modules with `.`s in their names
+          // will have their `.`s replaced with `_` before this code is executed,
+          // ex. module M.N --> "M_N", and will not hit this branch.)
+          // 
+          // Nested externs currently CANNOT be used with python-module-name:
+          //
+          // 1. (Python behavior; not able to be changed)
+          // Aliased Python modules cannot have `.`s in their name.
+          // ex. with `import X as Y`, `Y` cannot have `.`s.
+          //
+          // 2. (Dafny behavior; able to be changed, but don't need to change)
+          // Inside Dafny-generated Python modules,
+          // references to modules do not contain the python-module-name prefix.
+          // ex. If python-module-name=X.Y, and we have nested extern module "a.b.c",
+          //     code generation ignores the prefix and writes `a.b.c`.
+          //     Similarly, an extern non-nested module `E` is not prefixed and is generated as `E`,
+          //     and a non-extern nested module `M.N` is prefixed and generated as `X.Y.M_N`.
+          // (Similarly, extern modules do not contain the outer-module prefix).
+          // 
+          // 1. and 2. taken together prevent nested extern modules from being used with python-module-name.
+          // The reference to the nested extern inside generated code MUST be `a.b.c` due to 1).
+          // However, the aliased import cannot have `.`s in it due to 2).
+          // So nested externs cannot be aliased.
+          // Nested non-externs can be aliased (since, in 2., any nested `.`s are replaced with `_`s).
+          // Non-nested externs can be aliased (since, in 2., `Y` does not have `.`s).
+          //
+          // There are several possible paths to supporting these features together:
+          // - Modify behavior in 1 to apply prefixe (python-module-name/outer-module) to externs.
+          //   This is out of scope for python-module-name, since the outer-module prefix also does not apply to externs.
+          //   These are both "prefixes", and I expect any solution for python-module-name should also apply to outer-module.
+          // - Modify nested extern behavior to replace `.`s with `_`s, similar to nested non-externs.
+          if (!module.Value.Equals(module.Key)) {
+            throw new NotSupportedException($"Nested extern modules cannot be used with python-module-name. Nested extern: {module.Value}");
+          }
+          // Import the nested extern module directly.
+          // ex. module {:extern "a.b.c"} ==> `import a.b.c`
+          wr.WriteLine($"import {module.Value}");
+        } else {
+          // Here, module.Key == [python-module-name][outer-module][module.Value].
+          // However, in the body of the generated module, Dafny-generated code only references module.Value.
+          // Alias the import to module.Value so generated code can use the module.
+          //
+          // ex. python-module-name `X.Y`, outer-module=`A.B`:
+          // module `M` ==> `import X.Y.A_B_M as M`
+          // module `M.N` ==> `import X.Y.A_B_M_N as M_N`
+          // non-nested extern module `E` ==> `import X.Y.E as E` (outer-module prefix not applied to externs)
+          // nested extern modules not supported with python-module-name/outer-module prefixes.
+          wr.WriteLine($"import {module.Key} as {module.Value}");
+        }
+      }
       if (moduleName != null) {
         wr.WriteLine();
         wr.WriteLine($"# Module: {moduleName}");
-        Imports.Add(moduleName);
+        Imports.Add(pythonModuleName + moduleName, moduleName);
       }
     }
 
diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs
index 9049022003..192f0853c0 100644
--- a/Source/DafnyCore/Options/CommonOptionBag.cs
+++ b/Source/DafnyCore/Options/CommonOptionBag.cs
@@ -5,6 +5,7 @@
 using DafnyCore;
 using DafnyCore.Options;
 using Serilog.Events;
+using Microsoft.Dafny.Compilers;
 
 namespace Microsoft.Dafny;
 
@@ -616,6 +617,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     DooFile.RegisterNoChecksNeeded(ExtractCounterexample, false);
     DooFile.RegisterNoChecksNeeded(ShowProofObligationExpressions, false);
     DooFile.RegisterNoChecksNeeded(GoBackend.GoModuleNameCliOption, false);
+    DooFile.RegisterNoChecksNeeded(PythonBackend.PythonModuleNameCliOption, false);
   }
 }
 
diff --git a/Source/DafnyCore/Options/TranslationRecord.cs b/Source/DafnyCore/Options/TranslationRecord.cs
index 44d08c5dbf..7d422376d1 100644
--- a/Source/DafnyCore/Options/TranslationRecord.cs
+++ b/Source/DafnyCore/Options/TranslationRecord.cs
@@ -48,7 +48,7 @@ public TranslationRecord(Program program) {
     }
   }
 
-  private static bool ModuleEmptyForCompilation(ModuleDefinition module) {
+  public static bool ModuleEmptyForCompilation(ModuleDefinition module) {
     return !(module.DefaultClass?.Members.Any() ?? false)   // DefaultClass is null for _System
            && module.TopLevelDecls.All(d => d is DefaultClassDecl or ModuleDecl);
   }
diff --git a/Source/DafnyRuntime/DafnyRuntimePython/System_.py b/Source/DafnyRuntime/DafnyRuntimePython/System_.py
index 2497b812f4..d70b9c8c45 100644
--- a/Source/DafnyRuntime/DafnyRuntimePython/System_.py
+++ b/Source/DafnyRuntime/DafnyRuntimePython/System_.py
@@ -3,8 +3,7 @@
 from math import floor
 from itertools import count
 
-import module_
-import _dafny
+import _dafny as _dafny
 
 # Module: System_
 
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy
new file mode 100644
index 0000000000..6c6249d642
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy
@@ -0,0 +1,13 @@
+// RUN: %baredafny translate py  --python-module-name=PythonModule2 --library="%S/PythonModule1.doo" --translation-record "%S/PythonModule1-py.dtr" --output "%S/PythonModule2" "%s"
+// RUN: rm -rf "%S/PythonModule2"
+// RUN: mv "%S/PythonModule2-py" "%S/PythonModule2"
+// RUN: pip3 install "%S"
+// RUN: python3 %S/PythonModule2/ > %t
+// RUN: %diff "%s.expect" "%t"
+module DafnyModule3 {
+import DafnyModule1
+
+method Main() {
+        DafnyModule1.HelloWorld();
+}
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy.expect
new file mode 100644
index 0000000000..5e1c309dae
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy.expect
@@ -0,0 +1 @@
+Hello World
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr
new file mode 100644
index 0000000000..62d42175e4
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr
@@ -0,0 +1,4 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module.DafnyModule1]
+python-module-name = "PythonModule1"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo
new file mode 100644
index 0000000000..276201070e
Binary files /dev/null and b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1.doo differ
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/DafnyModule1.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/DafnyModule1.py
new file mode 100644
index 0000000000..e5f622a26f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/DafnyModule1.py
@@ -0,0 +1,19 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import PythonModule1.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+
+# Module: PythonModule1.DafnyModule1
+
+class default__:
+    def  __init__(self):
+        pass
+
+    @staticmethod
+    def HelloWorld():
+        _dafny.print((_dafny.SeqWithoutIsStrInference(map(_dafny.CodePoint, "Hello World"))).VerbatimString(False))
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/__main__.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/__main__.py
new file mode 100644
index 0000000000..9092b7de99
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/__main__.py
@@ -0,0 +1,9 @@
+# Dafny program helloworld.dfy compiled into Python
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import PythonModule1.module_ as module_
+import _dafny as _dafny
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/module_.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/module_.py
new file mode 100644
index 0000000000..25c55c6174
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/module_.py
@@ -0,0 +1,12 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import PythonModule1.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+import PythonModule1.DafnyModule1 as DafnyModule1
+
+# Module: PythonModule1.module_
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/setup.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/setup.py
new file mode 100644
index 0000000000..e8a736e7d1
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/setup.py
@@ -0,0 +1,13 @@
+# setup.py
+# installs the committed PythonModule1 and generated PythonModule2 as a Python module
+from setuptools import setup
+
+setup(
+    name="testpythonmodulemultimodule",
+    version="0.1.0",
+    packages=["PythonModule1", "PythonModule2"],
+    python_requires='>=3.6',
+    install_requires=[
+        'DafnyRuntimePython',
+    ],
+)
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule.doo b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule.doo
new file mode 100644
index 0000000000..48a3b05a68
Binary files /dev/null and b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule.doo differ
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some.py
new file mode 100644
index 0000000000..3b9e9374ae
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some.py
@@ -0,0 +1,13 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import SomeNestedModule.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+import SomeNestedModule.Some_Nested_Module as Some_Nested_Module
+import SomeNestedModule.Some_Nested as Some_Nested
+
+# Module: Some
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr
new file mode 100644
index 0000000000..17ec9a85dc
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr
@@ -0,0 +1,4 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module."Some.Nested.Module"]
+python-module-name = "SomeNestedModule"
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some_Nested.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some_Nested.py
new file mode 100644
index 0000000000..31b5634a41
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some_Nested.py
@@ -0,0 +1,12 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import SomeNestedModule.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+import SomeNestedModule.Some_Nested_Module as Some_Nested_Module
+
+# Module: Some_Nested
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some_Nested_Module.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some_Nested_Module.py
new file mode 100644
index 0000000000..e1bbf36876
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some_Nested_Module.py
@@ -0,0 +1,19 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import SomeNestedModule.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+
+# Module: Some_Nested_Module
+
+class default__:
+    def  __init__(self):
+        pass
+
+    @staticmethod
+    def HelloWorld():
+        _dafny.print((_dafny.SeqWithoutIsStrInference(map(_dafny.CodePoint, "Hello World"))).VerbatimString(False))
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/__main__.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/__main__.py
new file mode 100644
index 0000000000..b88c9409b6
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/__main__.py
@@ -0,0 +1,9 @@
+# Dafny program SomeNestedModule.dfy compiled into Python
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import SomeNestedModule.module_ as module_
+import _dafny as _dafny
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/module_.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/module_.py
new file mode 100644
index 0000000000..a3e2e5c937
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/module_.py
@@ -0,0 +1,14 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import SomeNestedModule.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+import SomeNestedModule.Some_Nested_Module as Some_Nested_Module
+import SomeNestedModule.Some_Nested as Some_Nested
+import SomeNestedModule.Some as Some
+
+# Module: module_
+
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy
new file mode 100644
index 0000000000..063cd71c1f
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy
@@ -0,0 +1,12 @@
+// RUN: pip3 install "%S"
+// RUN: %baredafny translate py --output "%S/SomeTestModule" --library="%S/SomeNestedModule.doo" --translation-record "%S/SomeNestedModule/SomeNestedModule-py.dtr" "%s"
+// RUN: python3 %S/SomeTestModule-py/ > %t
+// RUN: %diff "%s.expect" "%t"
+module SomeTestModule {
+
+    import Other = Some.Nested.Module
+
+    method Main() {
+        Other.HelloWorld();
+    }
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy.expect
new file mode 100644
index 0000000000..5e1c309dae
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeTestModule.dfy.expect
@@ -0,0 +1 @@
+Hello World
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/setup.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/setup.py
new file mode 100644
index 0000000000..7e1a7bf94e
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/setup.py
@@ -0,0 +1,13 @@
+# setup.py
+# installs the committed PythonModule1 and generated PythonModule2 as a Python module
+from setuptools import setup
+
+setup(
+    name="testpythonmodulenestedmodule",
+    version="0.1.0",
+    packages=["SomeNestedModule"],
+    python_requires='>=3.6',
+    install_requires=[
+        'DafnyRuntimePython',
+    ],
+)
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy
new file mode 100644
index 0000000000..d437246e53
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy
@@ -0,0 +1,12 @@
+// RUN: %baredafny translate py  --python-module-name=PythonModule1 "%s" --output "%S/PythonModule1"
+// RUN: rm -rf "%S/PythonModule1"
+// RUN: mv "%S/PythonModule1-py/" "%S/PythonModule1"
+// RUN: pip3 install "%S"
+// RUN: python3 %S/PythonModule1/ > %t
+// RUN: %diff "%s.expect" "%t"
+module DafnyModule1 {
+    
+    method Main() {
+        print "Hello World";
+    }
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy.expect
new file mode 100644
index 0000000000..5e1c309dae
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/helloworld.dfy.expect
@@ -0,0 +1 @@
+Hello World
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/setup.py b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/setup.py
new file mode 100644
index 0000000000..d82f5523ff
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/setup.py
@@ -0,0 +1,13 @@
+# setup.py
+# installs the generated PythonModule1 as a Python module
+from setuptools import setup
+
+setup(
+    name="testpythonmodulesinglemodule",
+    version="0.1.0",
+    packages=["PythonModule1"],
+    python_requires='>=3.6',
+    install_requires=[
+        'DafnyRuntimePython',
+    ],
+)
\ No newline at end of file