diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
index e5ab45f5425..f17d3e9fedd 100644
--- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
+++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs
@@ -9,7 +9,7 @@ namespace Microsoft.Dafny;
 
 public record PrefixNameModule(IReadOnlyList<IToken> Parts, LiteralModuleDecl Module);
 
-public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable<ModuleDefinition>, IHasSymbolChildren {
+public class  ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable<ModuleDefinition>, IHasSymbolChildren {
 
   public IToken BodyStartTok = Token.NoToken;
   public IToken TokenWithTrailingDocString = Token.NoToken;
diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs
index f67f8f8873a..0af99f0753e 100644
--- a/Source/DafnyCore/CoverageReport/CoverageReport.cs
+++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs
@@ -13,6 +13,7 @@ public class CoverageReport {
 
   private readonly Dictionary<Uri, List<CoverageSpan>> labelsByFile;
   private readonly Dictionary<Uri, HashSet<ModuleDefinition>> modulesByFile;
+  
   public readonly string Name; // the name to assign to this coverage report
   public readonly string Units; // the units of coverage (plural). This will be written in the coverage report table.
   private readonly string suffix; // user-provided suffix to add to filenames that are part of this report
@@ -72,14 +73,14 @@ public void RegisterFile(Uri uri) {
 
   private void RegisterFiles(Node astNode) {
     if (astNode.StartToken.ActualFilename != null) {
-      var uri = astNode.StartToken.Uri;
-      labelsByFile.GetOrCreate(uri, () => new List<CoverageSpan>());
-      
-      if (astNode is LiteralModuleDecl moduleDecl) {
-        modulesByFile.GetOrCreate(uri, () => new HashSet<ModuleDefinition>()).Add(moduleDecl.ModuleDef);
-        
-        RegisterFiles(moduleDecl.ModuleDef);
-      }
+      labelsByFile.GetOrCreate(astNode.StartToken.Uri, () => new List<CoverageSpan>());
+    }
+    
+    if (astNode is LiteralModuleDecl moduleDecl) {
+      // Uri may be null for implicit modules
+      modulesByFile.GetOrCreate(astNode.StartToken.Uri, () => new HashSet<ModuleDefinition>()).Add(moduleDecl.ModuleDef);
+
+      RegisterFiles(moduleDecl.ModuleDef);
     }
     
     foreach (var declaration in astNode.Children.OfType<LiteralModuleDecl>()) {
diff --git a/Source/DafnyDriver/CoverageReporter.cs b/Source/DafnyDriver/CoverageReporter.cs
index b16952967af..62c6cc2a3d0 100644
--- a/Source/DafnyDriver/CoverageReporter.cs
+++ b/Source/DafnyDriver/CoverageReporter.cs
@@ -20,9 +20,12 @@ public class CoverageReporter {
   private static readonly Regex UriRegexInversed = new(@"<h1 hidden>([^\n]*)</h1>");
   private static readonly Regex IndexLinkRegex = new(@"\{\{INDEX_LINK\}\}");
   private static readonly Regex LinksToOtherReportsRegex = new(@"\{\{LINKS_TO_OTHER_REPORTS\}\}");
-  private static readonly Regex TableHeaderRegex = new(@"\{\{TABLE_HEADER\}\}");
-  private static readonly Regex TableFooterRegex = new(@"\{\{TABLE_FOOTER\}\}");
-  private static readonly Regex TableBodyRegex = new(@"\{\{TABLE_BODY\}\}");
+  private static readonly Regex ByFileTableHeaderRegex = new(@"\{\{BY_FILE_TABLE_HEADER\}\}");
+  private static readonly Regex ByFileTableFooterRegex = new(@"\{\{BY_FILE_TABLE_FOOTER\}\}");
+  private static readonly Regex ByFileTableBodyRegex = new(@"\{\{BY_FILE_TABLE_BODY\}\}");
+  private static readonly Regex ByModuleTableHeaderRegex = new(@"\{\{BY_MODULE_TABLE_HEADER\}\}");
+  private static readonly Regex ByModuleTableFooterRegex = new(@"\{\{BY_MODULE_TABLE_FOOTER\}\}");
+  private static readonly Regex ByModuleTableBodyRegex = new(@"\{\{BY_MODULE_TABLE_BODY\}\}");
   private static readonly Regex IndexFileNameRegex = new(@"index(.*)\.html");
   private static readonly Regex PosRegexInverse = new("class=\"([a-z]+)\" id=\"([0-9]+):([0-9]+)\"");
   private const string CoverageReportTemplatePath = "coverage_report_template.html";
@@ -218,7 +221,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
       return;
     }
     var coverageLabels = Enum.GetValues(typeof(CoverageLabel)).Cast<CoverageLabel>().ToList();
-    List<object> header = new() { "File", "Module" };
+    List<object> header = new() { "File" };
     header.AddRange(coverageLabels
       .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
       .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}"));
@@ -229,8 +232,7 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
 
       body.Add(new() {
         $"<a href = \"{relativePath}{report.UniqueSuffix}.html\"" +
-        $"class = \"el_package\">{relativePath}</a>",
-        "All modules"
+        $"class = \"el_package\">{relativePath}</a>"
       });
       
       body.Last().AddRange(coverageLabels
@@ -240,7 +242,6 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
       
       foreach (var module in report.ModulesInFile(sourceFile).OrderBy(m => m.FullName)) {
         body.Add(new() {
-          "",
           module.FullName
         });
 
@@ -255,7 +256,15 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
                                  .Count(span => span.Label == label)).OfType<object>());
       }
     }
+    
+    header = new() { "Module" };
+    header.AddRange(coverageLabels
+      .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+      .Select(label => $"{report.Units} {CoverageLabelExtension.ToString(label)}"));
 
+    body = new();
+    PopulateByModuleTableBody(report, )
+    
     List<object> footer = new() { "Total", "" };
     footer.AddRange(coverageLabels
       .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
@@ -265,12 +274,54 @@ private void CreateIndexFile(CoverageReport report, Dictionary<Uri, string> sour
     var templateText = new StreamReader(templateStream).ReadToEnd();
     templateText = LinksToOtherReportsRegex.Replace(templateText, linksToOtherReports);
     templateText = FileNameRegex.Replace(templateText, report.Name);
-    templateText = TableHeaderRegex.Replace(templateText, MakeIndexFileTableRow(header));
-    templateText = TableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer));
-    templateText = TableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow)));
+    
+    templateText = ByFileTableBodyRegex.Replace(templateText, MakeIndexFileTableRow(header));
+    templateText = ByFileTableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer));
+    templateText = ByFileTableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow)));
+    
+    templateText = ByModuleTableBodyRegex.Replace(templateText, MakeIndexFileTableRow(header));
+    templateText = ByModuleTableFooterRegex.Replace(templateText, MakeIndexFileTableRow(footer));
+    templateText = ByModuleTableBodyRegex.Replace(templateText, string.Join("\n", body.Select(MakeIndexFileTableRow)));
+    
     File.WriteAllText(Path.Combine(baseDirectory, $"index{report.UniqueSuffix}.html"), templateText);
   }
 
+  private static void PopulateByModuleTableBody(CoverageReport report, ModuleDefinition module, List<CoverageLabel> coverageLabels, List<List<object>> body) {
+    body.Add(CountsForModule(report, module, coverageLabels).OfType<object>().ToList());
+    
+    foreach (var child in module.TopLevelDecls.OrderBy(decl => decl.Name)) {
+      if (child is LiteralModuleDecl moduleDecl) {
+        PopulateByModuleTableBody(report, moduleDecl.ModuleDef, coverageLabels, body);
+      }
+    }
+  }
+  
+  private static List<int> CountsForModule(CoverageReport report, ModuleDefinition module, List<CoverageLabel> coverageLabels) {
+    if (module.StartToken.Uri != null) {
+      var moduleRange = module.RangeToken.ToDafnyRange();
+      return coverageLabels
+        .Where(label => label != CoverageLabel.None && label != CoverageLabel.NotApplicable)
+        .Select(label => report.CoverageSpansForFile(module.StartToken.Uri)
+          // span.Span.Intersects(module.RangeToken) would be cleaner,
+          // but unfortunately coverage span tokens don't currently always
+          // have Token.pos set correctly. :(
+          .Where(span => moduleRange.Contains(span.Span.ToDafnyRange().Start))
+          .Count(span => span.Label == label)).ToList();
+    } else {
+      var sums = new int[coverageLabels.Count];
+      foreach (var child in module.TopLevelDecls) {
+        if (child is LiteralModuleDecl moduleDecl) {
+          var childModuleCounts = CountsForModule(report, moduleDecl.ModuleDef, coverageLabels);
+          for (var labelIndex = 0; labelIndex < coverageLabels.Count; labelIndex++) {
+            sums[labelIndex] += childModuleCounts[labelIndex];
+          }
+        }
+      }
+
+      return sums.ToList();
+    }
+  }
+
   /// <summary>
   /// Creates a set of links to be inserted in <param name="thisReport"></param> that point to corresponding
   /// report files for the same <param name="sourceFileName"></param>
diff --git a/Source/DafnyDriver/assets/coverage_report_index_template.html b/Source/DafnyDriver/assets/coverage_report_index_template.html
index bbba468d06d..0061f94dca2 100644
--- a/Source/DafnyDriver/assets/coverage_report_index_template.html
+++ b/Source/DafnyDriver/assets/coverage_report_index_template.html
@@ -14,13 +14,24 @@
 <h1>{{FILENAME}}</h1>
 <table class="coverage" cellspacing="0" id="coveragetable">
     <thead>
-    {{TABLE_HEADER}}
+    {{BY_FILE_TABLE_HEADER}}
     </thead>
     <tfoot>
-    {{TABLE_FOOTER}}
+    {{BY_FILE_TABLE_FOOTER}}
     </tfoot>
     <tbody>
-    {{TABLE_BODY}}
+    {{BY_FILE_TABLE_BODY}}
+    </tbody>
+</table>
+<table class="coverage" cellspacing="0" id="coveragetable">
+    <thead>
+    {{BY_MODULE_TABLE_HEADER}}
+    </thead>
+    <tfoot>
+    {{BY_MODULE_TABLE_FOOTER}}
+    </tfoot>
+    <tbody>
+    {{BY_MODULE_TABLE_BODY}}
     </tbody>
 </table>
 <div class="footer">