diff --git a/src/dafny/BinaryOperations.dfy b/src/dafny/BinaryOperations.dfy
index 8c5d64c2..7cf45705 100644
--- a/src/dafny/BinaryOperations.dfy
+++ b/src/dafny/BinaryOperations.dfy
@@ -5,7 +5,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} BinaryOperations {
+/** Defines a number of (ghost) properties of binary operations */
+module {:options "-functionSyntax:4"} BinaryOperations
+{
 
   ghost predicate IsAssociative<T(!new)>(bop: (T, T) -> T) {
     forall x, y, z :: bop(bop(x, y), z) == bop(x, bop(y, z))
diff --git a/src/dafny/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy b/src/dafny/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy
index 2fb619f4..fbe22882 100644
--- a/src/dafny/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy
+++ b/src/dafny/NonlinearArithmetic/Internals/DivInternalsNonlinear.dfy
@@ -8,7 +8,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} Dafny.DivInternalsNonlinear {
+/** Declares a few helper lemmas for internal use in non-linear arithmetic */
+module {:options "-functionSyntax:4"} Dafny.DivInternalsNonlinear
+{
 
   /* WARNING: Think three times before adding to this file, as nonlinear
   verification is highly unstable! */
diff --git a/src/dafny/NonlinearArithmetic/Internals/GeneralInternals.dfy b/src/dafny/NonlinearArithmetic/Internals/GeneralInternals.dfy
index 5a29febc..7814b30d 100644
--- a/src/dafny/NonlinearArithmetic/Internals/GeneralInternals.dfy
+++ b/src/dafny/NonlinearArithmetic/Internals/GeneralInternals.dfy
@@ -8,7 +8,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} Dafny.GeneralInternals {
+/** Declares helper lemmas and predicates for non-linear arithmetic */
+module {:options "-functionSyntax:4"} Dafny.GeneralInternals
+{
 
   /* this predicate is primarily used as a trigger */
   ghost predicate IsLe(x: int, y: int)
diff --git a/src/dafny/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy b/src/dafny/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy
index 2aac10e4..e0ff4130 100644
--- a/src/dafny/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy
+++ b/src/dafny/NonlinearArithmetic/Internals/ModInternalsNonlinear.dfy
@@ -8,7 +8,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} Dafny.ModInternalsNonlinear {
+/** Declares helper lemmas about the mod operation */
+module {:options "-functionSyntax:4"} Dafny.ModInternalsNonlinear
+{
 
   /* WARNING: Think three times before adding to this file, as nonlinear
   verification is highly unstable! */
diff --git a/src/dafny/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy b/src/dafny/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy
index d21a294e..9aeee623 100644
--- a/src/dafny/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy
+++ b/src/dafny/NonlinearArithmetic/Internals/MulInternalsNonlinear.dfy
@@ -8,7 +8,9 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module {:options "-functionSyntax:4"} Dafny.MulInternalsNonlinear {
+/** Declares some helper lemmas about multiply, for internal use */
+module {:options "-functionSyntax:4"} Dafny.MulInternalsNonlinear
+{
 
   /* WARNING: Think three times before adding to this file, as nonlinear
   verification is highly unstable! */
diff --git a/src/dafny/Unicode/Utf8EncodingForm.dfy b/src/dafny/Unicode/Utf8EncodingForm.dfy
index 0ffc0d00..77bf42f3 100644
--- a/src/dafny/Unicode/Utf8EncodingForm.dfy
+++ b/src/dafny/Unicode/Utf8EncodingForm.dfy
@@ -13,7 +13,7 @@ include "UnicodeEncodingForm.dfy"
 
 /**
   * The Unicode encoding form that assigns each Unicode scalar value to an unsigned byte sequence of one to four bytes
-  * in length, as specified in Table 3-6 and Table 3-7.
+  * in length, as specified in Table 3-6 and Table 3-7 of the Unicode Standard, Version 14.0.
   */
 module {:options "-functionSyntax:4"} Dafny.Utf8EncodingForm refines UnicodeEncodingForm {
   type CodeUnit = bv8