diff --git a/lang/spec.html b/lang/spec.html
index 3d7a4bed..1d47f775 100644
--- a/lang/spec.html
+++ b/lang/spec.html
@@ -8305,6 +8305,19 @@ <h3>Module and program execution</h3>
 becomes the new root module.
 </p>
 <p>
+A configuration is supplied as input to program execution. A
+<em>configuration</em> consists of mapping from names of configurable
+module-level variables to values. The values in a configuration always belong to
+the type <code>anydata&amp;readonly</code>. The value for a variable in the
+configuration is used during module initialization to initialize the variable
+instead of the value specified in the module. A configurable module-level
+variable may require that a configuration include a value for it. Except for
+this requirement, a configuration may be empty. Before initializing any module,
+the initialization phase must check that there is a value of the correct type
+supplied for every configurable module-level variable that requires
+configuration. If not, the module initialization phase terminates unsuccessfull.
+</p>
+<p>
 If the initialization phase of program execution completes successfully, then
 execution proceeds to the listening phase, which is described in the next
 section. The termination of the listening phase, which may be successful or
@@ -8609,29 +8622,50 @@ <h3>Module variable declaration</h3>
 
 <pre
 class="grammar">module-var-decl := module-init-var-decl | module-no-init-var-decl
-module-init-var-decl := metadata isolated-final-quals typed-binding-pattern <code>=</code> expression <code>;</code>
-isolated-final-quals :=
-  <code>final</code> [isolated-qual]
-  | [isolated-qual [<code>final</code>]]
 </pre>
 <p>
-The scope of variables declared in a module-var-decl is the entire module. Note
-that module variables are not allowed to be public. If final is specified, then
-it is not allowed to assign to the variable. If the typed-binding-pattern uses
-<code>var</code>, then the type of the variable is inferred from the static type
-of <code>expression</code>; if the module-var-decl includes <code>final</code>,
-the precise type is used, and otherwise the broad type is used. If the
-typed-binding-pattern specifies a type-descriptor, then that type-descriptor
-provides the contextually expected type for action-or-expr.
+A module-var-decl declares a variable. The scope of variables declared in a
+module-var-decl is the entire module. Module variables are not allowed to be
+public. The variable may be initialized in the declaration or within the
+module's <code>init</code> function. If <code>final</code> is specified, then it
+is not allowed to assign to the variable after it is initialized.
+</p>
+<pre
+class="grammar">
+module-init-var-decl := metadata module-init-var-quals typed-binding-pattern <code>=</code> module-var-init <code>;</code>
+module-init-var-quals := (<code>final</code> | isolated-qual | <code>configurable</code>)*
+module-var-init := expression | <code>?</code>
+</pre>
+<p>
+A module-init-var-decl declares and initializes a variable. It is an error for a
+keyword to appear more than once in <code>module-init-var-quals</code>. If the
+typed-binding-pattern uses <code>var</code>, then the type of the variable is
+inferred from the static type of <code>expression</code>; if the module-var-decl
+includes <code>final</code>, the precise type is used, and otherwise the broad
+type is used. If the typed-binding-pattern specifies a type-descriptor, then
+that type-descriptor provides the contextually expected type for action-or-expr.
 </p>
 <p>
 If a module-init-var-decl includes an isolated-qual, then the variable declared
 is isolated. In this case, the binding-pattern in the typed-binding-pattern must
 be just a variable-name, and the expression must be an isolated expression. A
 variable declared as an isolated variable can be accessed only within a
-lock-stmt. The keyword <code>isolated</code> occurring immediately before
-the typed-binding-pattern is parsed as part of isolated-final-quals
-rather than as part of typed-binding-pattern.
+lock-stmt. When an isolated-qual occurs in a position where the grammar would
+allow it to be parsed as part of module-init-var-quals or typed-binding-pattern,
+the former parse is used.
+</p>
+<p>
+If <code>configurable</code> is specified, then the initializer specified in the
+module-var-init may be overridden at the time of module initialization by a
+value supplied when the program is run. If such a value is supplied, then the
+expression in the module-var-init is not evaluated and the variable is
+initialized with the supplied value instead. A module-var-init of <code>?</code>
+is allowed only when <code>configurable</code> is specified and means that a
+configurable value must be supplied for this variable. If
+<code>configurable</code> is specified, then the typed-binding-pattern must use
+an explicit type-descriptor rather than <code>var</code> and the binding-pattern
+must be just a variable-name. The type specified by the type-descriptor must be
+a subtype of <code>anydata</code>.
 </p>
 
 <pre
@@ -9336,6 +9370,9 @@ <h3>Summary of changes from 2020R1 to Swan Lake</h3>
 fail</code> clause for compound statements. If a <code>check</code> expression
 or action fails, it behaves like a <code>fail</code> statement rather than a
 <code>return</code> statement.</li>
+<li>The language has a concept of configurability: module level variables can be
+specified to be <code>configurable</code>, which allows their initial values to
+be specified at runtime.</li>
 </ol>
 </section>
 <section>