diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
index 4cc71114cc..d865e0b72d 100644
--- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs
@@ -2961,6 +2961,12 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod
       AddUnsupportedFeature(e.Tok, Feature.ExactBoundedPool);
     }
 
+    protected override void OrganizeModules(Program program, out List<ModuleDefinition> modules) {
+      modules = program.CompileModules.ToList();
+      modules.Sort((a, b) =>
+        String.Compare(a.FullDafnyName, b.FullDafnyName, StringComparison.Ordinal));
+    }
+
     protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageVarName, Statement recoveryBody, ConcreteSyntaxTree wr) {
       TrStmt(body, wr);
     }
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/moduleordering.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/moduleordering.dfy
new file mode 100644
index 0000000000..543a05b0e4
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/moduleordering.dfy
@@ -0,0 +1,20 @@
+// NONUNIFORM: Test of the Rust compiler to ensure it emits modules in a deterministic order.
+// RUN: %baredafny translate rs "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%S/moduleordering-rust/src/moduleordering.rs" "%s"
+// CHECK-L: pub mod A {
+// CHECK-L: pub mod B {
+// CHECK-L: pub mod C {
+// CHECK-L: pub mod D {
+// CHECK-L: pub mod E {
+// CHECK-L: pub mod F {
+// CHECK-L: pub mod G {
+// CHECK-L: pub mod H {
+
+module B { const X := "B" }
+module D { import B const X := B.X }
+module C { import A const X := A.X }
+module E { import C const X := C.X }
+module A { import G const X := G.X }
+module G { const X := "G" }
+module F { const X := "F" }
+module H { const X := "H" }
\ No newline at end of file