diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 1e926e583..b8e2d2875 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -116,7 +116,7 @@ jobs:
         run: .github/scripts/checkLeanImport.sh
 
   build_doc:
-    name: Build Documentation
+    name: Build documentation
     runs-on: ubuntu-latest
     permissions:
       contents: read
@@ -126,10 +126,10 @@ jobs:
         uses: leanprover/lean-action@v1
         with:
           build-args: '--wfail'
-          lake-package-directory: 'docs/ddm'
-      - name: Build Documentation
-        run: lake exe docs 
-        working-directory: docs/ddm
+          lake-package-directory: 'docs/verso'
+      - name: Build documentation
+        run: ./generate.sh
+        working-directory: docs/verso
 
   build_python:
     name: Build and test Python
diff --git a/Strata/DL/Imperative/Cmd.lean b/Strata/DL/Imperative/Cmd.lean
index 2073321cf..b297bc723 100644
--- a/Strata/DL/Imperative/Cmd.lean
+++ b/Strata/DL/Imperative/Cmd.lean
@@ -28,19 +28,22 @@ variable declaration and assignment, and assertions and assumptions.
 -/
 
 /--
-A command in the Imperative dialect
+A an atomic command in the `Imperative` dialect.
+
+Commands don't create local control flow, and are typically used as a parameter
+to `Imperative.Stmt` or other similar types.
 -/
 inductive Cmd (P : PureExpr) : Type where
-  /-- `init` defines a variable called `name` with type `ty` and
-    initial value `e`. -/
+  /-- Define a variable called `name` with type `ty` and initial value `e`.
+  Note: we may make the initial value optional. -/
   | init     (name : P.Ident) (ty : P.Ty) (e : P.Expr) (md : (MetaData P) := .empty)
-  /-- `set` assigns `e` to a pre-existing variable `name`. -/
+  /-- Assign `e` to a pre-existing variable `name`. -/
   | set      (name : P.Ident) (e : P.Expr) (md : (MetaData P) := .empty)
-  /-- `havoc` assigns a pre-existing variable `name` a random value. -/
+  /-- Assigns an arbitrary value to an existing variable `name`. -/
   | havoc    (name : P.Ident) (md : (MetaData P) := .empty)
-  /-- `assert` checks whether condition `b` is true. -/
+  /-- Check whether condition `b` is true, failing if not. -/
   | assert   (label : String) (b : P.Expr) (md : (MetaData P) := .empty)
-  /-- `assume` constrains execution by adding assumption `b`. -/
+  /-- Ignore any execution state in which `b` is not true. -/
   | assume   (label : String) (b : P.Expr) (md : (MetaData P) := .empty)
 
 abbrev Cmds (P : PureExpr) := List (Cmd P)
diff --git a/Strata/DL/Imperative/CmdSemantics.lean b/Strata/DL/Imperative/CmdSemantics.lean
index d29c3725c..bf39e1ecd 100644
--- a/Strata/DL/Imperative/CmdSemantics.lean
+++ b/Strata/DL/Imperative/CmdSemantics.lean
@@ -234,10 +234,15 @@ def WellFormedSemanticEvalVar {P : PureExpr} [HasFvar P] (δ : SemanticEval P)
 
 def WellFormedSemanticEvalExprCongr {P : PureExpr} [HasVarsPure P P.Expr] (δ : SemanticEval P)
     : Prop := ∀ e σ σ', (∀ x ∈ HasVarsPure.getVars e, σ x = σ' x) → δ σ e = δ σ' e
+
 /--
-An inductive rule for state update.
+Abstract variable update.
+
+This does not specify how `σ` is represented, only what it maps each variable to.
 -/
 inductive UpdateState : SemanticStore P → P.Ident → P.Expr → SemanticStore P → Prop where
+  /-- The state `σ'` is be equivalent to `σ` except at `x`, where it maps to
+  `v`. Requires that `x` mapped to something beforehand. -/
   | update :
     σ x = .some v' →
     σ' x = .some v →
@@ -246,9 +251,13 @@ inductive UpdateState : SemanticStore P → P.Ident → P.Expr → SemanticStore
     UpdateState σ x v σ'
 
 /--
-An inductive rule for state init.
+Abtract variable initialization.
+
+This does not specify how `σ` is represented, only what it maps each variable to.
 -/
 inductive InitState : SemanticStore P → P.Ident → P.Expr → SemanticStore P → Prop where
+  /-- The state `σ'` is be equivalent to `σ` except at `x`, where it maps to
+  `v`. Requires that `x` mapped to nothing beforehand. -/
   | init :
     σ x = none →
     σ' x = .some v →
@@ -257,11 +266,12 @@ inductive InitState : SemanticStore P → P.Ident → P.Expr → SemanticStore P
     InitState σ x v σ'
 
 /--
-An inductively-defined operational semantics that depends on
-environment lookup and evaluation functions for expressions.
+An inductively-defined operational semantics for `Cmd` that depends on variable
+lookup (`σ`) and expression evaluation (`δ`) functions.
 -/
 inductive EvalCmd [HasFvar P] [HasBool P] [HasNot P] :
   SemanticEval P → SemanticStore P → Cmd P → SemanticStore P → Prop where
+  /-- If `e` evaluates to a value `v`, initialize `x` according to `InitState`. -/
   | eval_init :
     δ σ e = .some v →
     InitState P σ x v σ' →
@@ -269,6 +279,7 @@ inductive EvalCmd [HasFvar P] [HasBool P] [HasNot P] :
     ---
     EvalCmd δ σ (.init x _ e _) σ'
 
+  /-- If `e` evaluates to a value `v`, assign `x` according to `UpdateState`. -/
   | eval_set :
     δ σ e = .some v →
     UpdateState P σ x v σ' →
@@ -276,18 +287,22 @@ inductive EvalCmd [HasFvar P] [HasBool P] [HasNot P] :
     ----
     EvalCmd δ σ (.set x e _) σ'
 
+  /-- Assign `x` an arbitrary value `v` according to `UpdateState`. -/
   | eval_havoc :
     UpdateState P σ x v σ' →
     WellFormedSemanticEvalVar δ →
     ----
     EvalCmd δ σ (.havoc x _) σ'
 
+  /-- If `e` evaluates to true in `σ`, evaluate to the same `σ`. This semantics
+  does not have a concept of an erroneous execution. -/
   | eval_assert :
     δ σ e = .some HasBool.tt →
     WellFormedSemanticEvalBool δ →
     ----
     EvalCmd δ σ (.assert _ e _) σ
 
+  /-- If `e` evaluates to true in `σ`, evaluate to the same `σ`. -/
   | eval_assume :
     δ σ e = .some HasBool.tt →
     WellFormedSemanticEvalBool δ →
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index e27866997..45ed2ff09 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -24,13 +24,15 @@ open Std (ToFormat Format format)
 
 variable {Identifier : Type} [DecidableEq Identifier] [ToFormat Identifier] [Inhabited Identifier]
 
-/-- A metadata field.
+/-- A metadata field, which can be either a variable or an arbitrary string label.
 
 For now, we only track the variables modified by a construct, but we will expand
 this in the future.
 -/
 inductive MetaDataElem.Field (P : PureExpr) where
+  /-- Metadata indexed by a Strata variable. -/
   | var (v : P.Ident)
+  /-- Metadata indexed by an arbitrary label. -/
   | label (l : String)
 
 @[grind]
@@ -61,9 +63,11 @@ instance [Repr P.Ident] : Repr (MetaDataElem.Field P) where
       | .label s => f!"MetaDataElem.Field.label {s}"
     Repr.addAppParen res prec
 
-/-- A metadata value. -/
+/-- A metadata value, which can be either an expression or a message. -/
 inductive MetaDataElem.Value (P : PureExpr) where
+  /-- Metadata value in the form of a structured expression. -/
   | expr (e : P.Expr)
+  /-- Metadata value in the form of an arbitrary string. -/
   | msg (s : String)
 
 instance [ToFormat P.Expr] : ToFormat (MetaDataElem.Value P) where
@@ -103,7 +107,9 @@ instance [DecidableEq P.Expr] : DecidableEq (MetaDataElem.Value P) :=
 
 /-- A metadata element -/
 structure MetaDataElem (P : PureExpr) where
+  /-- The field or key used to identify the metadata. -/
   fld   : MetaDataElem.Field P
+  /-- The value of the metadata. -/
   value : MetaDataElem.Value P
 
 /-- Metadata is an array of tagged elements. -/
diff --git a/Strata/DL/Imperative/NondetStmt.lean b/Strata/DL/Imperative/NondetStmt.lean
index 2eb88f87e..8b22aec85 100644
--- a/Strata/DL/Imperative/NondetStmt.lean
+++ b/Strata/DL/Imperative/NondetStmt.lean
@@ -22,10 +22,23 @@ Comamnds](https://en.wikipedia.org/wiki/Guarded_Command_Language), and in
 [Kleene Algebra with Tests](https://www.cs.cornell.edu/~kozen/Papers/kat.pdf).
 -/
 
+/--
+A non-deterministic statement, parameterized by a type of pure expressions (`P`)
+and a type of commands (`Cmd`).
+
+This encodes the same types of control flow as `Stmt`, but using only
+non-deterministic choices: arbitrarily choosing one of two sub-statements to
+execute or executing a sub-statement an arbitrary number of times. Conditions
+can be encoded if the command type includes assumptions.
+-/
 inductive NondetStmt (P : PureExpr) (Cmd : Type) : Type where
+  /-- An atomic command, of an arbitrary type. -/
   | cmd      (cmd : Cmd)
+  /-- Execute `s1` followed by `s2`. -/
   | seq      (s1 s2 : NondetStmt P Cmd)
+  /-- Execute either `s1` or `s2`, arbitrarily. -/
   | choice   (s1 s2 : NondetStmt P Cmd)
+  /-- Execute `s` an arbitrary number of times (possibly zero). -/
   | loop     (s : NondetStmt P Cmd)
   deriving Inhabited
 
diff --git a/Strata/DL/Imperative/NondetStmtSemantics.lean b/Strata/DL/Imperative/NondetStmtSemantics.lean
index 929d60819..78a402926 100644
--- a/Strata/DL/Imperative/NondetStmtSemantics.lean
+++ b/Strata/DL/Imperative/NondetStmtSemantics.lean
@@ -14,8 +14,9 @@ namespace Imperative
 mutual
 
 /-- An inductively-defined operational semantics for non-deterministic
-statements that depends on environment lookup and evaluation functions
-for expressions.  -/
+statements that depends on environment lookup and evaluation functions for
+expressions.  **NOTE:** This will probably be replaced with a small-step
+semantics. -/
 inductive EvalNondetStmt (P : PureExpr) (Cmd : Type) (EvalCmd : EvalCmdParam P Cmd)
   [HasVarsImp P (List (Stmt P Cmd))] [HasVarsImp P Cmd] [HasFvar P] [HasBool P] [HasNot P] :
   SemanticEval P → SemanticStore P → NondetStmt P Cmd → SemanticStore P → Prop where
diff --git a/Strata/DL/Imperative/Stmt.lean b/Strata/DL/Imperative/Stmt.lean
index 3bc8eae32..0e1ffafdb 100644
--- a/Strata/DL/Imperative/Stmt.lean
+++ b/Strata/DL/Imperative/Stmt.lean
@@ -17,17 +17,30 @@ Imperative's Statements include commands and add constructs like structured and
 unstructured control-flow.
 -/
 
+/-- Imperative statements focused on control flow.
+
+The `P` parameter specifies the type of expressions that appear in conditional
+and loop guards.  The `Cmd` parameter specifies the type of atomic command
+contained within the `.cmd` constructor.
+-/
 inductive Stmt (P : PureExpr) (Cmd : Type) : Type where
+  /-- An atomic command. -/
   | cmd      (cmd : Cmd)
+  /-- An block containing a `List` of `Stmt`. -/
   | block    (label : String) (b : List (Stmt P Cmd)) (md : MetaData P := .empty)
-  /-- `ite` (if-then-else) statement provides structured control flow. -/
+  /-- A conditional execution statement. -/
   | ite      (cond : P.Expr)  (thenb : List (Stmt P Cmd)) (elseb : List (Stmt P Cmd)) (md : MetaData P := .empty)
-  /-- `loop` Loop statement with optional measure (for termination) and invariant. -/
+  /-- An iterated execution statement. Includes an optional measure (for
+  termination) and invariant. -/
   | loop     (guard : P.Expr) (measure : Option P.Expr) (invariant : Option P.Expr) (body : List (Stmt P Cmd)) (md : MetaData P := .empty)
-  /-- `goto` provides unstructured control flow. -/
+  /-- A semi-structured control flow statement transferring control to the given
+  label. The control flow induced by `goto` must not create cycles. **NOTE:**
+  This will likely be removed, in favor of an alternative view of imperative
+  programs that is purely untructured. -/
   | goto     (label : String) (md : MetaData P := .empty)
   deriving Inhabited
 
+/-- A block is simply an abbreviation for a list of commands. -/
 abbrev Block (P : PureExpr) (Cmd : Type) := List (Stmt P Cmd)
 
 def Stmt.isCmd {P : PureExpr} {Cmd : Type} (s : Stmt P Cmd) : Bool :=
diff --git a/Strata/DL/Imperative/StmtSemanticsSmallStep.lean b/Strata/DL/Imperative/StmtSemanticsSmallStep.lean
index 7fe49797d..5cb908987 100644
--- a/Strata/DL/Imperative/StmtSemanticsSmallStep.lean
+++ b/Strata/DL/Imperative/StmtSemanticsSmallStep.lean
@@ -20,12 +20,15 @@ dialect's statement constructs.
 /--
 Configuration for small-step semantics, representing the current execution
 state. A configuration consists of:
-- The current statement being executed
+- The current statement (or list of statements) being executed
 - The current store
 -/
 inductive Config (P : PureExpr) (CmdT : Type) : Type where
+  /-- A single statement to execute next. -/
   | stmt : Stmt P CmdT → SemanticStore P → Config P CmdT
+  /-- A list of statements to execute next, in order. -/
   | stmts : List (Stmt P CmdT) → SemanticStore P → Config P CmdT
+  /-- A terminal configuration, indicating that execution has finished. -/
   | terminal : SemanticStore P → Config P CmdT
 
 /--
@@ -41,8 +44,7 @@ inductive StepStmt
   [HasBool P] [HasNot P] :
   SemanticEval P → SemanticStore P → Config P CmdT → Config P CmdT → Prop where
 
-  /-- Command: a command steps to terminal configuration if it
-  evaluates successfully -/
+  /-- A command steps to terminal configuration if it evaluates successfully -/
   | step_cmd :
     EvalCmd δ σ c σ' →
     ----
@@ -50,13 +52,14 @@ inductive StepStmt
       (.stmt (.cmd c) σ)
       (.terminal σ')
 
-  /-- Block: a labeled block steps to its statement list -/
+  /-- A labeled block steps to its statement list. -/
   | step_block :
     StepStmt P EvalCmd δ σ
       (.stmt (.block _ ss _) σ)
       (.stmts ss σ)
 
-  /-- Conditional (true): if condition evaluates to true, step to then-branch -/
+  /-- If the condition of an `ite` statement evaluates to true, step to the then
+  branch. -/
   | step_ite_true :
     δ σ c = .some HasBool.tt →
     WellFormedSemanticEvalBool δ →
@@ -65,7 +68,8 @@ inductive StepStmt
       (.stmt (.ite c tss ess _) σ)
       (.stmts tss σ)
 
-  /-- Conditional (false): if condition evaluates to false, step to else-branch -/
+  /-- If the condition of an `ite` statement evaluates to false, step to the else
+  branch. -/
   | step_ite_false :
     δ σ c = .some HasBool.ff →
     WellFormedSemanticEvalBool δ →
@@ -74,7 +78,7 @@ inductive StepStmt
       (.stmt (.ite c tss ess _) σ)
       (.stmts ess σ)
 
-  /-- Loop (guard true): if guard is true, execute body then loop again -/
+  /-- If a loop guard is true, execute the body and then loop again. -/
   | step_loop_enter :
     δ σ g = .some HasBool.tt →
     WellFormedSemanticEvalBool δ →
@@ -83,7 +87,7 @@ inductive StepStmt
       (.stmt (.loop g m inv body md) σ)
       (.stmts (body ++ [.loop g m inv body md]) σ)
 
-  /-- Loop (guard false): if guard is false, terminate the loop -/
+  /-- If a loop guard is false, terminate the loop. -/
   | step_loop_exit :
     δ σ g = .some HasBool.ff →
     WellFormedSemanticEvalBool δ →
@@ -94,14 +98,14 @@ inductive StepStmt
 
   /- Goto: not implemented, because we plan to remove it. -/
 
-  /-- Empty statement list: no statements left to execute -/
+  /-- An empty list of statements steps to `.terminal` with no state changes. -/
   | step_stmts_nil :
     StepStmt P EvalCmd δ σ
       (.stmts [] σ)
       (.terminal σ)
 
-  /-- Statement composition: after executing a statement, continue with
-  remaining statements -/
+  /-- To evaluate a sequence of statements, evaluate the first statement and
+  then evaluate the remaining statements in the resulting state. -/
   | step_stmt_cons :
     StepStmt P EvalCmd δ σ (.stmt s σ) (.terminal σ') →
     ----
diff --git a/Strata/DL/Lambda/Identifiers.lean b/Strata/DL/Lambda/Identifiers.lean
index 3f1b24354..82944ec1c 100644
--- a/Strata/DL/Lambda/Identifiers.lean
+++ b/Strata/DL/Lambda/Identifiers.lean
@@ -20,7 +20,10 @@ section Identifiers
 Identifiers with a name and additional metadata
 -/
 structure Identifier (IDMeta : Type) : Type where
+  /-- A unique name. -/
   name : String
+  /-- Any additional metadata that it would be useful to attach to an
+  identifier. -/
   metadata : IDMeta
 deriving Repr, DecidableEq, Inhabited
 
diff --git a/Strata/DL/Lambda/LExpr.lean b/Strata/DL/Lambda/LExpr.lean
index 19bc6939c..ee45f8827 100644
--- a/Strata/DL/Lambda/LExpr.lean
+++ b/Strata/DL/Lambda/LExpr.lean
@@ -42,7 +42,9 @@ Expected interface for pure expressions that can be used to specialize the
 Imperative dialect.
 -/
 structure LExprParams : Type 1 where
+  /-- The type of metadata allowed on expressions. -/
   Metadata: Type
+  /-- The type of metadata allowed on identifiers. -/
   IDMeta : Type
   deriving Inhabited
 
@@ -50,7 +52,9 @@ structure LExprParams : Type 1 where
 Extended LExprParams that includes TypeType parameter.
 -/
 structure LExprParamsT : Type 1 where
+  /-- The base parameters, with the types for expression and identifier metadata. -/
   base : LExprParams
+  /-- The type of types used to annotate expressions. -/
   TypeType : Type
   deriving Inhabited
 
@@ -73,16 +77,32 @@ abbrev LExprParams.typed (T: LExprParams): LExprParams :=
 abbrev LExprParamsT.typed (T: LExprParamsT): LExprParamsT :=
   ⟨T.base.typed, LMonoTy⟩
 
+/--
+Lambda constants.
+
+Constants are integers, strings, reals, bitvectors of a fixed length, or
+booleans.
+-/
 inductive LConst : Type where
+  /-- An unbounded integer constant. -/
   | intConst (i: Int)
+
+  /-- A string constant, using Lean's `String` type for a sequence of Unicode
+  code points encoded with UTF-8. -/
   | strConst (s: String)
+
+  /-- A real constant, represented as a rational number. -/
   | realConst (r: Rat)
+
+  /-- A bit vector constant, represented using Lean's `BitVec` type. -/
   | bitvecConst (n: Nat) (b: BitVec n)
+
+  /-- A Boolean constant. -/
   | boolConst (b: Bool)
 deriving Repr, DecidableEq
 
 /--
-Lambda Expressions with Quantifiers.
+Lambda expressions with quantifiers.
 
 Like Lean's own expressions, we use the locally nameless
 representation for this abstract syntax.
@@ -93,29 +113,32 @@ We leave placeholders for type annotations only for constants
 (`.const`), operations (`.op`), binders (`.abs`, `.quant`), and free
 variables (`.fvar`).
 
-LExpr is parameterized by `TypeType`, which represents
-user-allowed type annotations (optional), and `Identifier` for allowed
-identifiers. For a fully annotated AST, see `LExprT` that is created after the
-type inference transform.
+LExpr is parameterized by `LExprParamsT`, which includes arbitrary metadata,
+user-allowed type annotations (optional), and special metadata to attach to
+`Identifier`s. Type inference adds any missing type annotations.
 -/
 inductive LExpr (T : LExprParamsT) : Type where
-  /-- `.const c ty`: constants (in the sense of literals). -/
+  /-- A constant (in the sense of literals). -/
   | const   (m: T.base.Metadata) (c: LConst)
-  /-- `.op c ty`: operation names. -/
+  /-- A built-in operation, referred to by name. -/
   | op      (m: T.base.Metadata) (o : Identifier T.base.IDMeta) (ty : Option T.TypeType)
-  /-- `.bvar deBruijnIndex`: bound variable. -/
+  /-- A bound variable, in de Bruijn form. -/
   | bvar    (m: T.base.Metadata) (deBruijnIndex : Nat)
-  /-- `.fvar name ty`: free variable, with an option (mono)type annotation. -/
+  /-- A free variable, with an optional type annotation. -/
   | fvar    (m: T.base.Metadata) (name : Identifier T.base.IDMeta) (ty : Option T.TypeType)
-  /-- `.abs ty e`: abstractions; `ty` the is type of bound variable. -/
+  /-- An abstraction, where `ty` the is (optional) type of bound variable. -/
   | abs     (m: T.base.Metadata) (ty : Option T.TypeType) (e : LExpr T)
-  /-- `.quant k ty tr e`: quantified expressions; `ty` the is type of bound variable, and `tr` the trigger. -/
+  /-- A quantified expression, where `k` indicates whether it is universally or
+  existentially quantified, `ty` is the type of bound variable, and `trigger` is
+  a trigger pattern (primarily for use with SMT). -/
   | quant   (m: T.base.Metadata) (k : QuantifierKind) (ty : Option T.TypeType) (trigger: LExpr T) (e : LExpr T)
-  /-- `.app fn e`: function application. -/
+  /-- A function application. -/
   | app     (m: T.base.Metadata) (fn e : LExpr T)
-  /-- `.ite c t e`: if-then-else expression. -/
+  /-- A conditional expression. This is a constructor rather than a built-in
+  operation because it occurs so frequently. -/
   | ite     (m: T.base.Metadata) (c t e : LExpr T)
-  /-- `.eq e1 e2`: equality expression. -/
+  /-- An equality expression. This is a constructor rather than a built-in
+  operation because it occurs so frequently. -/
   | eq      (m: T.base.Metadata) (e1 e2 : LExpr T)
 
 instance [Repr T.base.Metadata] [Repr T.TypeType] [Repr T.base.IDMeta] : Repr (LExpr T) where
diff --git a/Strata/DL/Lambda/LExprTypeEnv.lean b/Strata/DL/Lambda/LExprTypeEnv.lean
index d6ee8f505..5545774c2 100644
--- a/Strata/DL/Lambda/LExprTypeEnv.lean
+++ b/Strata/DL/Lambda/LExprTypeEnv.lean
@@ -55,18 +55,20 @@ instance : ToFormat TypeAlias where
 variable {T: LExprParams} [DecidableEq T.IDMeta] [ToFormat T.Metadata] [ToFormat T.IDMeta]
 
 /--
-A type context contains two maps: `types` and `aliases`.
-
-The `types` field maps free variables in expressions (i.e., `LExpr.fvar`s) to
-their type schemes. This is essentially a stack to account for variable scopes.
-
-The `aliases` field maps type synonyms to their corresponding type definitions.
-We expect these type definitions to not be aliases themselves, to avoid any
-cycles in the map (see `TEnv.addTypeAlias`).
+A type context describing the types of free variables and the mappings of type
+aliases.
 -/
 structure TContext (IDMeta : Type) where
+
+  /-- A map from free variables in expressions (i.e., `LExpr.fvar`s) to their
+  type schemes. This is essentially a stack to account for variable scopes.  -/
   types   :  Maps (Identifier IDMeta) LTy := []
+
+  /-- A map from type synonym names to their corresponding type definitions.  We
+  expect these type definitions to not be aliases themselves, to avoid any
+  cycles in the map (see `TEnv.addTypeAlias`).  -/
   aliases :  List TypeAlias := []
+
   deriving DecidableEq, Repr, Inhabited
 
 instance {IDMeta} [ToFormat IDMeta] : ToFormat (TContext IDMeta) where
@@ -240,9 +242,13 @@ Invariant: all functions defined in `TypeFactory.genFactory`
 for `datatypes` should be in `functions`.
 -/
 structure LContext (T: LExprParams) where
+  /-- Descriptions of all built-in functions. -/
   functions : @Factory T
+  /-- Descriptions of all built-in datatypes. -/
   datatypes : @TypeFactory T.IDMeta
+  /-- A list of known built-in types. -/
   knownTypes : KnownTypes
+  /-- The set of identifiers that have been seen or generated so far. -/
   idents : Identifiers T.IDMeta
 deriving Inhabited
 
diff --git a/Strata/DL/Lambda/LExprTypeSpec.lean b/Strata/DL/Lambda/LExprTypeSpec.lean
index c48cc2313..289a40ac1 100644
--- a/Strata/DL/Lambda/LExprTypeSpec.lean
+++ b/Strata/DL/Lambda/LExprTypeSpec.lean
@@ -58,31 +58,51 @@ def LTy.openFull (ty: LTy) (tys: List LMonoTy) : LMonoTy :=
   LMonoTy.subst [(List.zip (LTy.boundVars ty) tys)] (LTy.toMonoTypeUnsafe ty)
 
 /--
-Typing relation for `LExpr`s.
+Typing relation for `LExpr`s with respect to `LTy`.
+
+The typing relation is parameterized by two contexts. An `LContext` contains
+known types and functions while a `TContext` associates free variables with
+their types.
 -/
 inductive HasType {T: LExprParams} [DecidableEq T.IDMeta] (C: LContext T):
   (TContext T.IDMeta) → LExpr T.mono → LTy → Prop where
+
+  /-- A boolean constant has type `.bool` if `bool` is a known type in this
+  context. -/
   | tbool_const : ∀ Γ m b,
             C.knownTypes.containsName "bool" →
             HasType C Γ (.boolConst m b) (.forAll [] .bool)
+
+  /-- An integer constant has type `.int` if `int` is a known type in this
+  context. -/
   | tint_const : ∀ Γ m n,
             C.knownTypes.containsName "int" →
             HasType C Γ (.intConst m n) (.forAll [] .int)
+
+  /-- A real constant has type `.real` if `real` is a known type in this
+  context. -/
   | treal_const : ∀ Γ m r,
             C.knownTypes.containsName "real" →
             HasType C Γ (.realConst m r) (.forAll [] .real)
+
+  /-- A string constant has type `.string` if `string` is a known type in this
+  context. -/
   | tstr_const : ∀ Γ m s,
             C.knownTypes.containsName "string" →
             HasType C Γ (.strConst m s) (.forAll [] .string)
+
+  /-- A bit vector constant of size `n` has type `.bitvec n` if `bitvec` is a
+  known type in this context. -/
   | tbitvec_const : ∀ Γ m n b,
             C.knownTypes.containsName "bitvec" →
             HasType C Γ (.bitvecConst m n b) (.forAll [] (.bitvec n))
+
+  /-- An un-annotated variable has the type recorded for it in `Γ`, if any. -/
   | tvar : ∀ Γ m x ty, Γ.types.find? x = some ty → HasType C Γ (.fvar m x none) ty
-  /-
-  For an annotated free variable (or operator, see `top_annotated`), it must be
-  the case that the claimed type `ty_s` is an instantiation of the general type
-  `ty_o`. It suffices to show the existence of a list `tys` that, when
-  substituted for the bound variables in `ty_o`, results in `ty_s`.
+
+  /--
+  An annotated free variable has its claimed type `ty_s` if `ty_s` is an
+  instantiation of the type `ty_o` recorded for it in `Γ`.
   -/
   | tvar_annotated : ∀ Γ m x ty_o ty_s tys,
             Γ.types.find? x = some ty_o →
@@ -90,6 +110,11 @@ inductive HasType {T: LExprParams} [DecidableEq T.IDMeta] (C: LContext T):
             LTy.openFull ty_o tys = ty_s →
             HasType C Γ (.fvar m x (some ty_s)) (.forAll [] ty_s)
 
+  /--
+  An abstraction `λ x.e` has type `x_ty → e_ty` if the claimed type of `x` is
+  `x_ty` or None and if `e` has type `e_ty` when `Γ` is extended with the
+  binding `(x → x_ty)`.
+  -/
   | tabs : ∀ Γ m x x_ty e e_ty o,
             LExpr.fresh x e →
             (hx : LTy.isMonoType x_ty) →
@@ -99,6 +124,11 @@ inductive HasType {T: LExprParams} [DecidableEq T.IDMeta] (C: LContext T):
             HasType C Γ (.abs m o e)
                       (.forAll [] (.tcons "arrow" [(LTy.toMonoType x_ty hx),
                                                    (LTy.toMonoType e_ty he)]))
+
+  /--
+  An application `e₁e₂` has type `t1` if `e₁` has type `t2 → t1` and `e₂` has
+  type `t2`.
+  -/
   | tapp : ∀ Γ m e1 e2 t1 t2,
             (h1 : LTy.isMonoType t1) →
             (h2 : LTy.isMonoType t2) →
@@ -107,32 +137,46 @@ inductive HasType {T: LExprParams} [DecidableEq T.IDMeta] (C: LContext T):
             HasType C Γ e2 t2 →
             HasType C Γ (.app m e1 e2) t1
 
-  -- `ty` is more general than `e_ty`, so we can instantiate `ty` with `e_ty`.
+  /--
+  If expression `e` has type `ty` and `ty` is more general than `e_ty`,
+  then `e` has type `e_ty` (i.e. we can instantiate `ty` with `e_ty`).
+  -/
   | tinst : ∀ Γ e ty e_ty x x_ty,
             HasType C Γ e ty →
             e_ty = LTy.open x x_ty ty →
             HasType C Γ e e_ty
 
-  -- The generalization rule will let us do things like the following:
-  -- `(·ftvar "a") → (.ftvar "a")` (or `a → a`) will be generalized to
-  -- `(.btvar 0) → (.btvar 0)` (or `∀a. a → a`), assuming `a` is not in the
-  -- context.
+  /--
+  If `e` has type `ty`, it also has type `∀ a. ty` as long as `a` is fresh.
+  For instance, `(·ftvar "a") → (.ftvar "a")` (or `a → a`)
+  can be generalized to `(.btvar 0) → (.btvar 0)` (or `∀a. a → a`), assuming
+ `a` is not in the context.
+  -/
   | tgen : ∀ Γ e a ty,
             HasType C Γ e ty →
             TContext.isFresh a Γ →
             HasType C Γ e (LTy.close a ty)
 
+  /-- If `e1` and `e2` have the same type `ty`, and `c` has type `.bool`, then
+  `.ite c e1 e2` has type `ty`. -/
   | tif : ∀ Γ m c e1 e2 ty,
           HasType C Γ c (.forAll [] .bool) →
           HasType C Γ e1 ty →
           HasType C Γ e2 ty →
           HasType C Γ (.ite m c e1 e2) ty
 
+  /-- If `e1` and `e2` have the same type `ty`, then `.eq e1 e2` has type
+  `.bool`. -/
   | teq : ∀ Γ m e1 e2 ty,
           HasType C Γ e1 ty →
           HasType C Γ e2 ty →
           HasType C Γ (.eq m e1 e2) (.forAll [] .bool)
 
+  /--
+  A quantifier `∀/∃ {x: tr}.e` has type `bool` if the claimed type of `x` is
+  `x_ty` or None, and if, when `Γ` is extended with the binding `(x → x_ty)`,
+  `e` has type `bool` and `tr` is well-typed.
+  -/
   | tquant: ∀ Γ m k tr tr_ty x x_ty e o,
             LExpr.fresh x e →
             (hx : LTy.isMonoType x_ty) →
@@ -140,12 +184,17 @@ inductive HasType {T: LExprParams} [DecidableEq T.IDMeta] (C: LContext T):
             HasType C {Γ with types := Γ.types.insert x.fst x_ty} (LExpr.varOpen 0 x tr) tr_ty →
             o = none ∨ o = some (x_ty.toMonoType hx) →
             HasType C Γ (.quant m k o tr e) (.forAll [] .bool)
+
+  /--
+  An un-annotated operator has the type recorded for it in `C.functions`, if any.
+  -/
   | top: ∀ Γ m f op ty,
             C.functions.find? (fun fn => fn.name == op) = some f →
             f.type = .ok ty →
             HasType C Γ (.op m op none) ty
-  /-
-  See comments in `tvar_annotated`.
+  /--
+  Similarly to free variables, an annotated operator has its claimed type `ty_s` if `ty_s` is an
+  instantiation of the type `ty_o` recorded for it in `C.functions`.
   -/
   | top_annotated: ∀ Γ m f op ty_o ty_s tys,
             C.functions.find? (fun fn => fn.name == op) = some f →
diff --git a/Strata/DL/Lambda/LTy.lean b/Strata/DL/Lambda/LTy.lean
index ea047d6db..296644d1a 100644
--- a/Strata/DL/Lambda/LTy.lean
+++ b/Strata/DL/Lambda/LTy.lean
@@ -20,21 +20,21 @@ namespace Lambda
 open Std (ToFormat Format format)
 
 
+/-- Type identifiers. For now, these are just strings. -/
 abbrev TyIdentifier := String
 
 instance : Coe String TyIdentifier where
   coe := id
 
-/--
-Types in Lambda: these are mono-types. Note that all free type variables
-(`.ftvar`) are implicitly universally quantified.
--/
+/-- Monomorphic types in Lambda. Note that all free type variables (`.ftvar`)
+are implicitly universally quantified.  -/
 inductive LMonoTy : Type where
-  /-- Type variable. -/
+  /-- A type variable. -/
   | ftvar (name : TyIdentifier)
-  /-- Type constructor. -/
+  /-- A type constructor. -/
   | tcons (name : String) (args : List LMonoTy)
-  /-- Special support for bitvector types of every size. -/
+  /-- A bit vector type. This is a special case so that it can be parameterized
+  by a size. -/
   | bitvec (size : Nat)
   deriving Inhabited, Repr
 
@@ -120,9 +120,10 @@ def LMonoTy.getArrowArgs (t: LMonoTy) : List LMonoTy :=
   | _ => []
 
 /--
-Type schemes (poly-types) in Lambda.
+Polymorphic type schemes in Lambda.
 -/
 inductive LTy : Type where
+  /-- A type containing universally quantified type variables. -/
   | forAll (vars : List TyIdentifier) (ty : LMonoTy)
   deriving Inhabited, Repr
 
diff --git a/Strata/DL/Lambda/Semantics.lean b/Strata/DL/Lambda/Semantics.lean
index 41d5b0907..bb7261f68 100644
--- a/Strata/DL/Lambda/Semantics.lean
+++ b/Strata/DL/Lambda/Semantics.lean
@@ -28,63 +28,72 @@ def Scopes.toEnv (s:Scopes Tbase) : Env Tbase :=
   fun t => (s.find? t).map (·.snd)
 
 /--
-A small-step semantics of LExpr.
-Currently only defined for LMonoTy, but it will be expanded to an arbitrary
-type in the future.
+A small-step semantics for `LExpr`.
+
+Currently only defined for expressions paremeterized by `LMonoTy`, but it will
+be expanded to an arbitrary type in the future.
+
 The order of constructors matter because the `constructor` tactic will rely on
 it.
-This small-step definitions faithfully follows the behavior of LExpr.eval,
-except that
-(1) This inductive definition may stuck early when there is no
-assignment to a free variable available.
-(2) This semantics does not describe how the metadata must change, because
-metadata must not affect evaluation semantics. Different concrete evaluators
-like LExpr.eval can use different strategy for updating metadata.
+
+This small-step definitions faithfully follows the behavior of `LExpr.eval`,
+except that:
+1. This inductive definition may get stuck early when there is no
+   assignment to a free variable available.
+
+2. This semantics does not describe how metadata must change, because
+   metadata must not affect evaluation semantics. Different concrete evaluators
+   like `LExpr.eval` can have different strategy for updating metadata.
 -/
 inductive Step (F:@Factory Tbase) (rf:Env Tbase)
   : LExpr Tbase.mono → LExpr Tbase.mono → Prop where
--- A free variable. Stuck if fvar does not exist in FreeVarMap.
+/-- A free variable. Stuck if `fvar` does not exist in `FreeVarMap`. -/
 | expand_fvar:
   ∀ (x:Tbase.Identifier) (e:LExpr Tbase.mono),
     rf x = .some e →
     Step F rf (.fvar m x ty) e
 
--- Beta reduction for lambda; Call-by-value semantics.
+/-- Call-by-value semantics: beta reduction. -/
 | beta:
   ∀ (e1 v2 eres:LExpr Tbase.mono),
     LExpr.isCanonicalValue F v2 →
     eres = LExpr.subst (fun _ => v2) e1 →
     Step F rf (.app m1 (.abs m2 ty e1) v2) eres
 
--- Call-by-value semantics.
+/-- Call-by-value semantics: argument evaluation. -/
 | reduce_2:
   ∀ (v1 e2 e2':LExpr Tbase.mono),
     LExpr.isCanonicalValue F v1 →
     Step F rf e2 e2' →
     Step F rf (.app m v1 e2) (.app m' v1 e2')
 
+/-- Call-by-value semantics: function evaluation. -/
 | reduce_1:
   ∀ (e1 e1' e2:LExpr Tbase.mono),
     Step F rf e1 e1' →
     Step F rf (.app m e1 e2) (.app m' e1' e2)
 
--- For ite x e1 e2, do not eagerly evaluate e1 and e2.
--- For the reduction order, ite x e1 e2 is interpreted as
--- 'ite x (λ.e1) (λ.e2)'.
+/-- Lazy evaluation of `ite`: condition is true. To evaluate `ite x e1 e2`, do
+not first evaluate `e1` and `e2`. In other words, `ite x e1 e2` is interpreted
+as `ite x (λ.e1) (λ.e2)`.  -/
 | ite_reduce_then:
   ∀ (ethen eelse:LExpr Tbase.mono),
     Step F rf (.ite m (.const mc (.boolConst true)) ethen eelse) ethen
 
+/-- Lazy evaluation of `ite`: condition is false. To evaluate `ite x e1 e2`, do
+not first evaluate `e1` and `e2`. In other words, `ite x e1 e2` is interpreted
+as `ite x (λ.e1) (λ.e2)`.  -/
 | ite_reduce_else:
   ∀ (ethen eelse:LExpr Tbase.mono),
     Step F rf (.ite m (.const mc (.boolConst false)) ethen eelse) eelse
 
+/-- Evaluation of `ite` condition. -/
 | ite_reduce_cond:
   ∀ (econd econd' ethen eelse:LExpr Tbase.mono),
     Step F rf econd econd' →
     Step F rf (.ite m econd ethen eelse) (.ite m' econd' ethen eelse)
 
--- Equality. Reduce after both operands evaluate to values.
+/-- Evaluation of equality. Reduce after both operands evaluate to values. -/
 | eq_reduce:
   ∀ (e1 e2 eres:LExpr Tbase.mono)
     (H1:LExpr.isCanonicalValue F e1)
@@ -92,21 +101,24 @@ inductive Step (F:@Factory Tbase) (rf:Env Tbase)
     eres = .const mc (.boolConst (LExpr.eql F e1 e2 H1 H2)) →
     Step F rf (.eq m e1 e2) eres
 
+/-- Evaluation of the left-hand side of an equality. -/
 | eq_reduce_lhs:
   ∀ (e1 e1' e2:LExpr Tbase.mono),
     Step F rf e1 e1' →
     Step F rf (.eq m e1 e2) (.eq m' e1' e2)
 
+/-- Evaluation of the right-hand side of an equality. -/
 | eq_reduce_rhs:
   ∀ (v1 e2 e2':LExpr Tbase.mono),
     LExpr.isCanonicalValue F v1 →
     Step F rf e2 e2' →
     Step F rf (.eq m v1 e2) (.eq m' v1 e2')
 
--- Expand functions and free variables when they are evaluated.
--- If the function body is unknown, concreteEval can be instead used. Look at
--- the eval_fn constructor below.
--- This is consistent with what LExpr.eval does (modulo the "inline" flag).
+/-- Evaluate a built-in function when a body expression is available in the
+`Factory` argument `F`. This is consistent with what `LExpr.eval` does (modulo
+the `inline` flag). Note that it might also be possible to evaluate with
+`eval_fn`. A key correctnes property is that doing so will yield the same
+result. -/
 | expand_fn:
   ∀ (e callee fnbody new_body:LExpr Tbase.mono) args fn,
     F.callOfLFunc e = .some (callee,args,fn) →
@@ -115,9 +127,10 @@ inductive Step (F:@Factory Tbase) (rf:Env Tbase)
     new_body = LExpr.substFvars fnbody (fn.inputs.keys.zip args) →
     Step F rf e new_body
 
--- The second way of evaluating a function call.
--- If LFunc has a concrete evaluator, this can be used to 'jump' to the final
--- result of the function.
+/-- Evaluate a built-in function when a concrete evaluation function is
+available in the `Factory` argument `F`.  Note that it might also be possible to
+evaluate with `expand_fn`. A key correctnes property is that doing so will yield
+the same result. -/
 | eval_fn:
   ∀ (e callee e':LExpr Tbase.mono) args fn denotefn,
     F.callOfLFunc e = .some (callee,args,fn) →
diff --git a/Tools/Python/test_results/dialects/Python.dialect.st.ion b/Tools/Python/test_results/dialects/Python.dialect.st.ion
index 17a74a977..7f0f7d798 100644
Binary files a/Tools/Python/test_results/dialects/Python.dialect.st.ion and b/Tools/Python/test_results/dialects/Python.dialect.st.ion differ
diff --git a/docs/ddm/README.md b/docs/ddm/README.md
deleted file mode 100644
index 10e48290e..000000000
--- a/docs/ddm/README.md
+++ /dev/null
@@ -1,23 +0,0 @@
-# DDM User Manual
-
-Strata dialects are defined in their own domain-specific language that
-can be embededed in Lean or used externally.
-
-This Verso package provides HTML documentation of the Strata dialect
-definition language.  The documentation can be generated by the command
-
-```
-lake exe docs
-```
-
-The output will be written to `_out/single-page`.  Links in Verso
-documentation do not work if the file is opened in the browser directly.
-Instead, we recommend launching a local web server to view the
-documentation.
-If Python is available, then this can be done with the command
-
-```
-python -m http.server 1080 -d _out/html-single
-```
-
-This will print out a URL that can be opened in a browser to view the documentation.
diff --git a/docs/ddm/generate.sh b/docs/ddm/generate.sh
deleted file mode 100755
index f458bbe3d..000000000
--- a/docs/ddm/generate.sh
+++ /dev/null
@@ -1,3 +0,0 @@
-set -ex
-
-lake exe docs --with-html-single --output _out/html
diff --git a/docs/ddm/lakefile.toml b/docs/ddm/lakefile.toml
deleted file mode 100644
index ed849e325..000000000
--- a/docs/ddm/lakefile.toml
+++ /dev/null
@@ -1,14 +0,0 @@
-name = "StrataDoc"
-defaultTargets = ["docs"]
-
-[[require]]
-name = "verso"
-git = "https://github.com/leanprover/verso"
-rev = "nightly-testing"
-
-[[lean_lib]]
-name = "StrataDoc"
-
-[[lean_exe]]
-name = "docs"
-root = "StrataDocMain"
\ No newline at end of file
diff --git a/docs/ddm/lean-toolchain b/docs/ddm/lean-toolchain
deleted file mode 100644
index 27770b571..000000000
--- a/docs/ddm/lean-toolchain
+++ /dev/null
@@ -1 +0,0 @@
-leanprover/lean4:v4.23.0-rc2
\ No newline at end of file
diff --git a/docs/ddm/.gitignore b/docs/verso/.gitignore
similarity index 100%
rename from docs/ddm/.gitignore
rename to docs/verso/.gitignore
diff --git a/docs/ddm/StrataDoc.lean b/docs/verso/DDMDoc.lean
similarity index 99%
rename from docs/ddm/StrataDoc.lean
rename to docs/verso/DDMDoc.lean
index 28b380cb6..d271d823f 100644
--- a/docs/ddm/StrataDoc.lean
+++ b/docs/verso/DDMDoc.lean
@@ -18,7 +18,7 @@ set_option pp.rawOnError true
 #doc (Manual) "The Strata DDM Manual" =>
 %%%
 authors := ["Joe Hendrix"]
-shortTitle := "Strata"
+shortTitle := "Strata DDM"
 %%%
 
 The Strata Dialect Definition Mechanism (DDM) is a set of tools for defining
diff --git a/docs/ddm/StrataDocMain.lean b/docs/verso/DDMDocMain.lean
similarity index 76%
rename from docs/ddm/StrataDocMain.lean
rename to docs/verso/DDMDocMain.lean
index 5d5786f7b..2c2ed861f 100644
--- a/docs/ddm/StrataDocMain.lean
+++ b/docs/verso/DDMDocMain.lean
@@ -6,7 +6,7 @@
 
 
 
-import StrataDoc
+import DDMDoc
 open Verso.Genre.Manual (Config manualMain)
 
 def config : Config where
@@ -15,4 +15,4 @@ def config : Config where
   emitHtmlMulti := false
   htmlDepth := 2
 
-def main := manualMain (%doc StrataDoc) (config := config)
+def main := manualMain (%doc DDMDoc) (config := config)
diff --git a/docs/verso/LangDefDoc.lean b/docs/verso/LangDefDoc.lean
new file mode 100644
index 000000000..ceadf0b66
--- /dev/null
+++ b/docs/verso/LangDefDoc.lean
@@ -0,0 +1,327 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import VersoManual
+
+import Strata.DL.Imperative.Cmd
+import Strata.DL.Imperative.CmdSemantics
+import Strata.DL.Imperative.Stmt
+import Strata.DL.Imperative.StmtSemanticsSmallStep
+import Strata.DL.Imperative.NondetStmt
+import Strata.DL.Imperative.NondetStmtSemantics
+import Strata.DL.Imperative.MetaData
+import Strata.DL.Lambda.LExpr
+import Strata.DL.Lambda.Semantics
+import Strata.DL.Lambda.LExprTypeSpec
+
+open Lambda
+open Imperative
+
+-- This gets access to most of the manual genre
+open Verso.Genre Manual
+
+-- This gets access to Lean code that's in code blocks, elaborated in
+-- the same process and environment as Verso
+open Verso.Genre.Manual.InlineLean
+
+set_option pp.rawOnError true
+set_option verso.docstring.allowMissing false
+
+#doc (Manual) "The Strata Language Definition" =>
+%%%
+shortTitle := "The Strata Language"
+%%%
+
+# Introduction
+
+Strata aims to provide a foundation for representing the semantics of programs,
+specifications, protocols, architectures, and other aspects of large-scale
+distributed systems and their components. It achieves this through languages of
+two types. The first type, consisting of the single Strata Core language,
+provides a central hub that can serve as a connection point between multiple
+types of input artifact and multiple types of analysis, reducing the cost of
+implementing N analyses for M languages from N\*M to N+M.
+
+The second type consists of numerous Strata _dialects_.  The Dialect Definition
+Mechanism, described
+[here](https://github.com/strata-org/Strata/tree/main/docs/verso/DDMDoc.lean),
+provides a way to define the syntax and a simple type system for a dialect.  At
+the moment, dialects do not directly have semantics (though we may add a
+mechanism for defining their semantics in the future) but instead are defined by
+translation to or from Strata Core. Said another way, each of these dialects is
+a different concrete way to write Strata programs, but all of these dialects are
+ultimately represented internally using the same Core language.
+
+Dialects are used to describe both the initial artifacts being analyzed by
+Strata and more low-level representations of those artifacts used to communicate
+with external reasoning tools such as model checkers or SMT solvers. In both
+situations, Strata uses dialects as a mechanism for communicating with external
+tools (either language front ends or generic automated reasoning tools like SMT
+solvers).
+
+The following "hourglass" diagram illustrates how various existing (blue) or
+potential (gray) input dialects could be translated into Strata Core and then
+into the input language for various back end tools. Solid lines indicate
+translation paths that exist (though experimentally in the connection between
+Strata Core and CBMC), and dotted lines indicate translations that illustrate
+the sorts of use cases we expect Strata to support but that haven't yet been
+implemented.
+
+![Strata hourglass diagram](strata-hourglass.png)
+
+The Strata Core language is constructed using a few building blocks that can be
+combined in different ways. This allows concrete dialects to systematically use
+different combinations that still share the majority of their implementation. In
+Lean (and in principle in most other source languages that could be used to
+process Strata programs), the type system can enforce various structural
+constraints, ensuring that only expected language constructs show up. The Strata
+Core language itself consists of an imperative statement type parameterized by
+an expression type, with various more fine-grained adjustments of other
+parameters.
+
+The two fundamental building blocks of Strata Core are a representation of
+functional programs (`Lambda`), and a representation of imperative programs
+(`Imperative`). The `Lambda` language is parameterized by a type system and a
+set of built-in types and functions. The `Imperative` language is then
+parameterized by the type of expressions it allows in conditions, assignments,
+and so on. Currently, those expressions will almost always be some
+instantiation of `Lambda`. Both Core building blocks are parameterized by a
+metadata type, which by default is instantiated with a map from keys to
+structured values that can contain expressions (typically from `Lambda`).
+
+The remainder of this document describes the current abstract syntax and
+semantics of `Lambda` and `Imperative` in detail, with direct reference to the
+Lean source code that defines these languages. We do not consider the Core
+language set in stone. It may evolve over time, particularly to add new
+fundamental constructs, and this document will be updated as it does. We intend
+for Strata Core to be close to a superset of [B3](https://b3-lang.org/), but it
+may at times make different choices to support its goal of being useful for a
+wide range of analyses, rather than being optimized for deductive verification.
+In particular, Strata aims to make it possible to encode most input artifacts
+without the need for axioms.
+
+# Lambda
+
+The `Lambda` language is a standard but generic implementation of the lambda
+calculus. It is parameterized by a type for metadata and the type of types
+(which may be `Unit`, to describe the untyped lambda calculus). It includes the
+standard constructs for constants, free and bound variables, abstractions, and
+applications. In addition, it includes a special type of constant, an operator,
+to represent built-in functions. It extends the standard lambda calculus by
+allowing quantifiers (since a key use of the language is to write logical
+predicates) and includes a constructor for if-then-else to allow it to have lazy
+semantics.
+
+Although `Lambda` can be parameterized by an arbitrary type system, the Strata
+code base includes a
+[formalization](https://github.com/strata-org/Strata/blob/main/Strata/DL/Lambda/LExprTypeSpec.lean)
+of a polymorphic Hindley-Milner type system and an
+[implementation](https://github.com/strata-org/Strata/blob/main/Strata/DL/Lambda/LTyUnify.lean)
+of an inference algorithm over the type `LTy` (described below). This allows
+universal quantification over types and the use of arbitrary named type
+constructors (as well as special support for bit vector types, to allow them to
+be parameterized by size).
+
+## Syntax
+
+The syntax of lambda expressions is provided by the {name LExpr}`LExpr` type.
+
+{docstring Lambda.LExpr}
+
+Identifiers in lambda expressions, using the {name Identifier}`Identifier` type,
+can be annotated with metadata.
+
+{docstring Lambda.Identifier}
+
+Specific constructors exist for constants of various scalar types, including
+booleans, bit vectors, integers, reals, and strings.
+
+{docstring Lambda.LConst}
+
+The {name LExpr}`LExpr` type can be parameterized by the type used to represent
+normal metadata and the type used to represent identifier metadata, as well as
+the type of types.
+
+{docstring Lambda.LExprParams}
+
+{docstring Lambda.LExprParamsT}
+
+## Type System
+
+Although {name LExpr}`LExpr` can be parameterized by an arbitrary type system,
+Strata currently implements one, based on the types {name LMonoTy}`LMonoTy` and
+{name LTy}`LTy`.
+
+The first, {name LMonoTy}`LMonoTy`, represents monomorphic types. It's a
+separate type because some contexts allow only monomorphic types.
+
+{docstring Lambda.LMonoTy}
+
+Type variables in {name LMonoTy}`LMonoTy` use the {name TyIdentifier}`TyIdentifier` type.
+
+{docstring Lambda.TyIdentifier}
+
+The {name LTy}`LTy` type allows monomorphic types to be wrapped in universal type
+quantifiers that bind these type variables, creating polymorphic types.
+
+{docstring Lambda.LTy}
+
+An expression {name LExpr}`LExpr` parameterized by {name LTy}`LTy` is
+well-typed according to the {name LExpr.HasType}`HasType` relation.
+This relation depends on two types of context.
+
+The first of these, {name LContext}`LContext`, contains information that does
+not change throughout the type checking process. This includes information about
+built-in functions, using the {name Factory}`Factory` type, and built-in types,
+using the {name TypeFactory}`TypeFactory` type. Built-in functions optionally
+include concrete evaluation functions, which can be used in the operational
+semantics described below.
+
+{docstring Lambda.LContext}
+
+The second context includes two pieces of data that change throughout the type
+checking process: a map from free variables in expressions to types, and a list
+of type aliases including the name and definition of each alias.
+
+{docstring Lambda.TContext}
+
+Given these two pieces of context, the {name LExpr.HasType}`HasType` relation
+describes the valid type of each expression form.
+
+{docstring Lambda.LExpr.HasType}
+
+## Operational Semantics
+
+The semantics of the {name LExpr}`LExpr` type are specified in a standard way
+using the small-step inductive relation {name Lambda.Step}`Lambda.Step`.
+This relation is parameterized by a `Factory`, which describes built-in
+functions via an optional body and/or evaluation function.
+
+{docstring Lambda.Step}
+
+Typically we will want to talk about arbitrarily long sequences of steps, such
+as from an initial expression to a value. The
+{name Lambda.StepStar}`Lambda.StepStar` relation describes the reflexive,
+transitive closure of the {name Lambda.Step}`Lambda.Step` relation.
+
+{docstring Lambda.StepStar}
+
+# Imperative
+
+The `Imperative` language is a standard core imperative calculus, parameterized
+by a type of expressions and divided into two pieces: commands and statements.
+Commands represent atomic operations that do not induce control flow (except
+possibly in the form of procedure calls that follow a stack discipline, though
+the current core set of commands does not include calls). Statements are
+parameterized by a command type and describe the control flow surrounding those
+commands. Currently, `Imperative` has structured, deterministic statements, each
+of which can be: a command, a sequence of statements in a block, a deterministic
+conditional, a deterministic loop with a condition, or a forward `goto`
+statement. (Note: we plan to replace `goto` with a block exit statement, and
+have a separate unstructured CFG representation.)
+
+We plan to add non-deterministic statements, as in [Kleene Algebra with
+Tests](https://www.cs.cornell.edu/~kozen/Papers/kat.pdf), and support a
+translation from structured deterministic statements into structured
+non-deterministic statements.
+
+We also expect to add unstructured control-flow graphs where each basic block
+consists of a sequence of commands followed by a terminator command. A
+terminator command can be: a conditional jump to one of two blocks, termination
+of execution, or a non-deterministic jump to any one of an arbitrary number of
+successor blocks.
+
+## Command Syntax
+
+The core built-in set of commands includes variable initializations,
+deterministic assignments, non-deterministic assignments ("havoc"), assertions,
+and assumptions.
+
+{docstring Imperative.Cmd}
+
+## Command Operational Semantics
+
+The semantics of commands are specified in terms of how they interact with a
+program state, written `σ`. A state can be applied to a variable to obtain its
+current value. And an expression `e` can be evaluated using the evaluation
+function in a given state: `δ σ e` gives the result of evaluating `e` in state
+`σ`. This generic description allows the details of the program state
+representation to vary, as long as it supports these operations.
+
+Given a state `σ`, the {name InitState}`InitState` relation describes how a
+variable obtains its initial value.
+
+{docstring Imperative.InitState}
+
+The {name UpdateState}`UpdateState` relation then describes how a variable's
+value can change.
+
+{docstring Imperative.UpdateState}
+
+Given these two state relations, the semantics of each command is specified in
+a standard way.
+
+{docstring Imperative.EvalCmd}
+
+## Structured Deterministic Statement Syntax
+
+Statements allow commands to be organized into standard control flow
+arrangements, including sequencing, alternation, and iteration. Sequencing
+statements occurs by grouping them into blocks. Loops can be annotated with
+optional invariants and decreasing measures, which can be used for deductive
+verification.
+
+{docstring Imperative.Stmt}
+
+{docstring Imperative.Block}
+
+## Structured Deterministic Statement Operational Semantics
+
+The semantics of the {name Stmt}`Stmt` type is defined in terms of
+*configurations*, represented by the {name Imperative.Config}`Config` type. A
+configuration pairs the statement(s) remaining to be executed with a state, and
+each step of execution goes from an initial configuration to a final configuration.
+
+{docstring Imperative.Config}
+
+The {name StepStmt}`StepStmt` type describes how each type of statement
+transforms configurations. Like with the other components of Strata, the rules
+follow standard conventions.
+
+{docstring Imperative.StepStmt}
+
+Like with `Lambda`, we typically want to talk about arbitrarily long sequences
+of steps.  The {name StepStmtStar}`Imperative.StepStmtStar` relation describes
+the reflexive, transitive closure of the {name StepStmt}`Imperative.StepStmt`
+relation.
+
+{docstring Imperative.StepStmtStar}
+
+# Metadata
+
+Metadata allows additional information to be attached to nodes in the Strata
+AST. This may include information such as the provenance of specific AST nodes
+(_e.g._, the locations in source code that gave rise to them), facts inferred by
+specific analyses, or indications of the goal of a specific analysis, among many
+other possibilities.
+
+Each metadata element maps a field to a value. A field can be named with a
+variable or an arbitrary string.
+
+{docstring Imperative.MetaDataElem.Field}
+
+A value can take the form of an expression or an arbitrary string.
+
+{docstring Imperative.MetaDataElem.Value}
+
+A metadata element pairs a field with a value.
+
+{docstring Imperative.MetaDataElem}
+
+And, finally, the metadata attached to an AST node consists of an array of
+metadata elements.
+
+{docstring Imperative.MetaData}
diff --git a/docs/verso/LangDefDocMain.lean b/docs/verso/LangDefDocMain.lean
new file mode 100644
index 000000000..9423ab6d1
--- /dev/null
+++ b/docs/verso/LangDefDocMain.lean
@@ -0,0 +1,18 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+
+
+import LangDefDoc
+open Verso.Genre.Manual (Config manualMain)
+
+def config : Config where
+  emitTeX := false
+  emitHtmlSingle := true
+  emitHtmlMulti := false
+  htmlDepth := 2
+
+def main := manualMain (%doc LangDefDoc) (config := config)
diff --git a/docs/verso/README.md b/docs/verso/README.md
new file mode 100644
index 000000000..05c34a620
--- /dev/null
+++ b/docs/verso/README.md
@@ -0,0 +1,37 @@
+# Strata documents created in Verso
+
+This Verso package provides documentation of the core Strata language
+and the Dialect Definition Mechanism (DDM). The documentation can be
+generated by the command
+
+```
+./generate.sh
+```
+
+The output will be written to `_out/{document name}`. Links in Verso
+documentation do not work if the file is opened in the browser directly.
+Instead, we recommend launching a local web server to view the
+documentation. If Python is available, then this can be done with the
+command
+
+```
+python3 -m http.server 1080 -d _out/langdef/html-single
+```
+
+or
+
+```
+python3 -m http.server 1080 -d _out/ddm/html-single
+```
+
+This will print out a URL that can be opened in a browser to view the documentation.
+
+# Strata Language Definition
+
+TODO
+
+# DDM User Manual
+
+New Strata dialects are defined in their own domain-specific language
+that can be embededed in Lean or imported from external files. This
+document provides a guide to using that DSL.
diff --git a/docs/verso/generate.sh b/docs/verso/generate.sh
new file mode 100755
index 000000000..92a4ba4d9
--- /dev/null
+++ b/docs/verso/generate.sh
@@ -0,0 +1,5 @@
+set -ex
+
+lake exe ddm --with-html-single --output _out/ddm
+lake exe langdef --with-html-single --output _out/langdef
+cp strata-hourglass.png _out/langdef/html-single/
diff --git a/docs/ddm/lake-manifest.json b/docs/verso/lake-manifest.json
similarity index 54%
rename from docs/ddm/lake-manifest.json
rename to docs/verso/lake-manifest.json
index edaee8c6e..aac17d200 100644
--- a/docs/ddm/lake-manifest.json
+++ b/docs/verso/lake-manifest.json
@@ -5,17 +5,34 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "590eac5d96f04c5a75214b3b501afe389c333720",
+   "rev": "8ba8c1ee844cd4a4ef1957801780c6e99e469897",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "v4.25.1",
    "inherited": false,
    "configFile": "lakefile.lean"},
+  {"type": "path",
+   "scope": "",
+   "name": "Strata",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "../..",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "8864a73bf79aad549e34eff972c606343935106d",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "aaee7fa4a1a158bd814d76f642df8a1d19db9f49",
+   "rev": "66aefec2852d3e229517694e642659f316576591",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "dd7c477cb8b1898c3ace7bf66a47462eef7ac52c",
+   "rev": "7347ddaca36e59238bf1fc210a6bf71dd0bccdd6",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/docs/verso/lakefile.toml b/docs/verso/lakefile.toml
new file mode 100644
index 000000000..11162158d
--- /dev/null
+++ b/docs/verso/lakefile.toml
@@ -0,0 +1,25 @@
+name = "StrataDoc"
+defaultTargets = ["ddm", "langdef"]
+
+[[require]]
+name = "Strata"
+path = "../.."
+
+[[require]]
+name = "verso"
+git = "https://github.com/leanprover/verso"
+rev = "v4.25.1"
+
+[[lean_lib]]
+name = "DDMDoc"
+
+[[lean_lib]]
+name = "LangDefDoc"
+
+[[lean_exe]]
+name = "ddm"
+root = "DDMDocMain"
+
+[[lean_exe]]
+name = "langdef"
+root = "LangDefDocMain"
diff --git a/docs/verso/lean-toolchain b/docs/verso/lean-toolchain
new file mode 100644
index 000000000..370b26d9c
--- /dev/null
+++ b/docs/verso/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.25.2
diff --git a/docs/verso/strata-hourglass.png b/docs/verso/strata-hourglass.png
new file mode 100644
index 000000000..44d7261ac
Binary files /dev/null and b/docs/verso/strata-hourglass.png differ