diff --git a/.gitignore b/.gitignore
index fa980dfaa..113f59ecc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,3 +29,4 @@ _build
 /simulation/docs/_minted-sim-realism/
 /data/simulation/*.trace.json
 /data/simulation/*.array.schema.json
+node_modules/
diff --git a/analysis/markov/ReadMe.md b/analysis/markov/ReadMe.md
index c7c26dd88..03ccb9860 100644
--- a/analysis/markov/ReadMe.md
+++ b/analysis/markov/ReadMe.md
@@ -54,7 +54,7 @@ Provided that a quorum of votes have endorsed the EB, the following conditions a
 Provided that an honest RB exists, an EB can be forged if the node has received the previous EB and computed the ledger state.
 
 - Because of their membership in the previous vote, a fraction $n_\text{comm} / n_\text{pools}$ of the pools have already updated their ledger state.
-- Of the pools not having voted on the block we define $p_\text{late}$ as the probability that the EB has arrived too late to compute the ledger state needed to produce the next EB.
+- We define $p_\text{late}$ as the probability that the EB has arrived too late to compute the ledger state needed to produce the next EB.
 
 
 ### Substep 4: Vote
diff --git a/analysis/markov/lake-manifest.json b/analysis/markov/lake-manifest.json
index e8e8006b8..9ce246de9 100644
--- a/analysis/markov/lake-manifest.json
+++ b/analysis/markov/lake-manifest.json
@@ -21,10 +21,20 @@
    "inputRev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad",
    "inherited": false,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/argumentcomputer/LSpec",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "24cceb69c20fadca0fd3acabe39fa9270dfb47e6",
+   "name": "LSpec",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "24cceb69c20fadca0fd3acabe39fa9270dfb47e6",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "scope": "leanprover-community",
+   "scope": "",
    "rev": "c211948581bde9846a99e32d97a03f0d5307c31e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
diff --git a/analysis/markov/lakefile.lean b/analysis/markov/lakefile.lean
new file mode 100644
index 000000000..130e4e351
--- /dev/null
+++ b/analysis/markov/lakefile.lean
@@ -0,0 +1,43 @@
+import Lake
+
+open Lake DSL
+
+package «linleios» where
+  version := StdVer.mk (SemVerCore.mk 0 1 0) ""
+  testDriver := "linleios_test"
+  leanOptions := #[
+    -- pretty-prints `fun a ↦ b`
+    ⟨`pp.unicode.fun, true⟩,
+    -- disables automatic implicit arguments
+    ⟨`autoImplicit, false⟩,
+    -- suppresses the checkBinderAnnotations error/warning
+    ⟨`checkBinderAnnotations, false⟩,
+  ]
+  moreServerOptions := #[
+    ⟨`trace.debug, true⟩,
+  ]
+
+lean_lib «Linleios» where
+  srcDir := "src"
+
+@[default_target]
+lean_exe «linleios» where
+  root := `Main
+  srcDir := "src"
+  supportInterpreter := false
+
+lean_exe «linleios_test» where
+  root := `LinleiosTest
+  srcDir := "src"
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4" @ "v4.20.0"
+
+require LSpec from git
+  "https://github.com/argumentcomputer/LSpec" @ "24cceb69c20fadca0fd3acabe39fa9270dfb47e6"
+
+require Parser from git
+  "https://github.com/fgdorais/lean4-parser" @ "26d5ce4d60195a869b1fdb100b442794ea63e1ad"
+
+require Cli from git
+  "https://github.com/mhuisi/lean4-cli" @ "v4.20.0"
diff --git a/analysis/markov/lakefile.toml b/analysis/markov/lakefile.toml
deleted file mode 100644
index b2a3c08ff..000000000
--- a/analysis/markov/lakefile.toml
+++ /dev/null
@@ -1,36 +0,0 @@
-name = "linleios"
-version = "0.1.0"
-keywords = ["math"]
-defaultTargets = ["linleios"]
-
-[[lean_lib]]
-name = "Linleios"
-
-[[lean_exe]]
-name = "linleios"
-root = "Main"
-
-[leanOptions]
-pp.unicode.fun = true # pretty-prints `fun a ↦ b`
-autoImplicit = false
-
-[[require]]
-name = "mathlib"
-scope = "leanprover-community"
-version = "git#v4.20.0"
-
-[[require]]
-name = "Parser"
-git = "https://github.com/fgdorais/lean4-parser"
-rev = "26d5ce4d60195a869b1fdb100b442794ea63e1ad"
-
-[[require]]
-name = "Cli"
-git = "https://github.com/mhuisi/lean4-cli"
-rev = "v4.20.0"
-
-[lean]
-server-options = [
-  ["checkBinderAnnotations", "false"],
-  ["diagnostics", "true"]
-]
diff --git a/analysis/markov/Linleios.lean b/analysis/markov/src/Linleios.lean
similarity index 76%
rename from analysis/markov/Linleios.lean
rename to analysis/markov/src/Linleios.lean
index c48d5238b..1ca2b148b 100644
--- a/analysis/markov/Linleios.lean
+++ b/analysis/markov/src/Linleios.lean
@@ -1,4 +1,5 @@
 import Linleios.Evolve
+import Linleios.Metrics
 
 /-!
 # Linleios: a Markovian model of Linear Leios
diff --git a/analysis/markov/Linleios/Evolve.lean b/analysis/markov/src/Linleios/Evolve.lean
similarity index 62%
rename from analysis/markov/Linleios/Evolve.lean
rename to analysis/markov/src/Linleios/Evolve.lean
index 39e25d049..62cf2b4e0 100644
--- a/analysis/markov/Linleios/Evolve.lean
+++ b/analysis/markov/src/Linleios/Evolve.lean
@@ -1,13 +1,9 @@
 
 import Std.Data.HashMap
-import Batteries.Lean.HashMap
-import Lean.Data.Json.FromToJson
 
 import Linleios.Types
 
 
-open Lean (Json)
-open Lean.ToJson (toJson)
 open Std (HashMap)
 
 
@@ -104,67 +100,3 @@ def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat →
 | 0     => start
 | n + 1 => let state' := prune ε $ chain (@step env) start
            simulate env state' ε n
-
-
-/--
-Compute the total probabilities of a set of states.
--/
-def totalProbability (states : Probabilities) : Probability :=
-  states.values.sum
-
-/--
-Compute the distribution of EB counts.
--/
-def ebDistribution : Probabilities → HashMap Nat Probability :=
-  HashMap.fold
-    (
-      fun acc state p =>
-        HashMap.mergeWith (fun _ => Add.add) acc
-          $ singleton ⟨ state.ebCount , p ⟩
-    )
-    ∅
-
-/--
-Format the distribution of EB counts as JSON.
--/
-def ebDistributionJson : Probabilities → Json :=
-  Json.mkObj
-    ∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩)
-    ∘ (fun z => z.mergeSort (by exact fun x y => x.fst ≤ y.fst))
-    ∘ HashMap.toList
-    ∘ ebDistribution
-
-/--
-Compute the RB efficiency, given a set of states.
--/
-def rbEfficiency (states : Probabilities) : Float :=
-  let clock := states.keys.head!.clock
-  let rbCount :=
-    HashMap.fold
-      (fun acc state p =>acc + state.rbCount.toFloat * p)
-      0
-      states
-  rbCount / clock.toFloat
-
-/--
-Compute the EB efficiency, given a set of states.
--/
-def ebEfficiency (states : Probabilities) : Float :=
-  let clock := states.keys.head!.clock
-  let ebCount :=
-    HashMap.fold
-      (fun acc state p =>acc + state.ebCount.toFloat * p)
-      0
-      states
-  ebCount / (clock.toFloat - 1)
-
-/--
-Compute the overall efficiency, give a set of states.
--/
-def efficiency (states : Probabilities) : Float :=
-  let rb := rbEfficiency states
-  let eb := ebEfficiency states
-  let rbSize := 0.9
-  let ebSize := 12.0
-  let ρ := ebSize / rbSize
-  (rb * (1 - eb) + ρ * eb) / (1 + ρ)
diff --git a/analysis/markov/src/Linleios/Metrics.lean b/analysis/markov/src/Linleios/Metrics.lean
new file mode 100644
index 000000000..6056b01e8
--- /dev/null
+++ b/analysis/markov/src/Linleios/Metrics.lean
@@ -0,0 +1,74 @@
+import Std.Data.HashMap
+import Batteries.Lean.HashMap
+import Lean.Data.Json.FromToJson
+
+import Linleios.Types
+
+open Lean (Json)
+open Lean.ToJson (toJson)
+open Std (HashMap)
+
+
+/--
+Compute the total probabilities of a set of states.
+-/
+def totalProbability (states : Probabilities) : Probability :=
+  states.fold (Function.const State ∘ Add.add) 0
+
+/--
+Compute the distribution of EB counts.
+-/
+def ebDistribution : Probabilities → HashMap Nat Probability :=
+  HashMap.fold
+    (
+      fun acc state p =>
+        -- FIXME: Rewrite using `Function.const`.
+        HashMap.mergeWith (fun _ => Add.add) acc
+          $ singleton ⟨ state.ebCount , p ⟩
+    )
+    ∅
+
+/--
+Format the distribution of EB counts as JSON.
+-/
+def ebDistributionJson : Probabilities → Json :=
+  Json.mkObj
+    ∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩)
+    ∘ (fun z => z.mergeSort (by exact fun x y => x.fst ≤ y.fst))
+    ∘ HashMap.toList
+    ∘ ebDistribution
+
+/--
+Compute the RB efficiency, given a set of states.
+-/
+def rbEfficiency (states : Probabilities) : Float :=
+  let clock := states.keys.head!.clock
+  let rbCount :=
+    HashMap.fold
+      (fun acc state p =>acc + state.rbCount.toFloat * p)
+      0
+      states
+  rbCount / clock.toFloat
+
+/--
+Compute the EB efficiency, given a set of states.
+-/
+def ebEfficiency (states : Probabilities) : Float :=
+  let clock := states.keys.head!.clock
+  let ebCount :=
+    HashMap.fold
+      (fun acc state p =>acc + state.ebCount.toFloat * p)
+      0
+      states
+  ebCount / (clock.toFloat - 1)
+
+/--
+Compute the overall efficiency, give a set of states.
+-/
+def efficiency (states : Probabilities) : Float :=
+  let rb := rbEfficiency states
+  let eb := ebEfficiency states
+  let rbSize := 0.9
+  let ebSize := 12.0
+  let ρ := ebSize / rbSize
+  (rb * (1 - eb) + ρ * eb) / (1 + ρ)
diff --git a/analysis/markov/Linleios/Probability.lean b/analysis/markov/src/Linleios/Probability.lean
similarity index 100%
rename from analysis/markov/Linleios/Probability.lean
rename to analysis/markov/src/Linleios/Probability.lean
diff --git a/analysis/markov/Linleios/Types.lean b/analysis/markov/src/Linleios/Types.lean
similarity index 92%
rename from analysis/markov/Linleios/Types.lean
rename to analysis/markov/src/Linleios/Types.lean
index 0cc4df299..c8503672e 100644
--- a/analysis/markov/Linleios/Types.lean
+++ b/analysis/markov/src/Linleios/Types.lean
@@ -57,6 +57,12 @@ def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committee
     fAdversary := fAdversary
   }
 
+/--
+A perfect honest environment with the recommended protocol parameters.
+-/
+instance : Inhabited Environment where
+  default := makeEnvironment 1 4 7 0.05 600 0.75 1 1 0 0
+
 
 /--
 The state of the chain's evolution.
@@ -74,17 +80,6 @@ structure State where
   canCertify : Bool
 deriving Repr, BEq, Hashable, Inhabited
 
-/--
-The genesis state starts when zero counts.
--/
-theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by
-  constructor
-  rfl
-  constructor
-  rfl
-  rfl
-
-
 /--
 The active states and their probabilities.
 -/
@@ -92,6 +87,7 @@ def Probabilities := HashMap State Probability
 deriving Repr, EmptyCollection
 
 instance : Inhabited Probabilities where
+  -- TODO: Rewrite using `Singleton.singleton`.
   default := (∅ : Probabilities).insert Inhabited.default 1
 
 
diff --git a/analysis/markov/Linleios/Util.lean b/analysis/markov/src/Linleios/Util.lean
similarity index 100%
rename from analysis/markov/Linleios/Util.lean
rename to analysis/markov/src/Linleios/Util.lean
diff --git a/analysis/markov/src/LinleiosTest.lean b/analysis/markov/src/LinleiosTest.lean
new file mode 100644
index 000000000..e811d6071
--- /dev/null
+++ b/analysis/markov/src/LinleiosTest.lean
@@ -0,0 +1,220 @@
+import Linleios
+import LSpec
+import Std.Data.HashMap
+
+open LSpec
+open Std.HashMap (singleton_eq_insert)
+
+
+-- Lemmas, in lieu of tests
+
+/--
+The genesis state starts with zero counts.
+-/
+theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by
+  constructor
+  rfl
+  constructor
+  rfl
+  rfl
+
+
+-- Generators
+
+structure RangedNat (lo hi : Nat) where
+  value: Nat
+deriving Repr
+
+instance {lo hi : Nat} : SlimCheck.Shrinkable (RangedNat lo hi) where
+  shrink _ := []
+
+instance {lo hi : Nat} : SlimCheck.SampleableExt (RangedNat lo hi) :=
+  SlimCheck.SampleableExt.mkSelfContained $
+    RangedNat.mk <$> SlimCheck.Gen.choose Nat lo hi
+
+instance : SlimCheck.Random Float where
+  randomR lo hi :=
+    do
+      let res := 1000
+      let lo' := (lo * res).ceil.toUInt16.toNat
+      let hi' := (hi * res).floor.toUInt16.toNat
+      let i ← SlimCheck.Random.randomR lo' hi'
+      pure $ i.toFloat / res
+
+structure RangedFloat (lo hi : Float) where
+  value: Float
+deriving Repr
+
+instance {lo hi : Float} : SlimCheck.Shrinkable (RangedFloat lo hi) where
+  shrink _ := []
+
+instance {lo hi : Float} : SlimCheck.SampleableExt (RangedFloat lo hi) :=
+  SlimCheck.SampleableExt.mkSelfContained $
+    RangedFloat.mk <$> SlimCheck.Gen.choose Float lo hi
+
+instance : SlimCheck.Shrinkable Environment where
+  shrink _ := []
+
+instance : SlimCheck.SampleableExt Environment :=
+  SlimCheck.SampleableExt.mkSelfContained $
+    do
+      let Lheader : Nat ← SlimCheck.Gen.choose Nat 1 3
+      let Lvote ← SlimCheck.Gen.choose Nat 2 6
+      let Ldiff ← SlimCheck.Gen.choose Nat 0 8
+      let activeSlotCoefficient : Float ← SlimCheck.Gen.choose Float 0.01 0.05
+      let committeeSize ← SlimCheck.Gen.choose Nat 100 800
+      let τ ← SlimCheck.Gen.choose Float 0.51 0.99
+      let pRbHeaderArrives ← SlimCheck.Gen.choose Float 0.90 1.00
+      let pEbValidates ← SlimCheck.Gen.choose Float 0.85 1.00
+      let pEbUnvalidated ← SlimCheck.Gen.choose Float 0.00 0.15
+      let fAdversary ← SlimCheck.Gen.choose Float 0.00 0.49
+      pure $
+        makeEnvironment
+          Lheader Lvote Ldiff
+          activeSlotCoefficient
+          committeeSize.toFloat τ
+          pRbHeaderArrives pEbValidates pEbUnvalidated
+          fAdversary
+
+instance : SlimCheck.Shrinkable State where
+  shrink _ := []
+
+instance : SlimCheck.SampleableExt State :=
+  SlimCheck.SampleableExt.mkSelfContained $
+    do
+      let clock ← SlimCheck.Gen.choose Nat 0 1000
+      let rbCount ← SlimCheck.Gen.choose Nat 0 clock
+      let ebCount ← SlimCheck.Gen.choose Nat 0 rbCount
+      let hasRb ← SlimCheck.Gen.chooseAny Bool
+      let canCertify ← Bool.and hasRb <$> SlimCheck.Gen.chooseAny Bool
+      pure $ State.mk clock rbCount ebCount hasRb canCertify
+
+
+-- Property-based tests.
+
+/--
+Tolerance for floating-point operations.
+-/
+private def ε := 1e-6
+
+/--
+Check that a probability is near a specified value.
+-/
+private def nearValue (value x : Float) : Bool := (x - value).abs < ε
+
+/--
+Check that a probability is close to unity.
+-/
+private def nearUnity : Float → Bool := nearValue 1
+
+/--
+Check that the total outcome is near unity.
+-/
+private def outcomeNearUnity (os : Outcomes) : Bool :=
+  nearUnity $  os.foldl (fun acc sp ↦ acc + sp.snd) 0
+
+#lspec
+    group "Probabilities" (
+      test "Initial probability is unity" (
+        totalProbability (default : Probabilities) == 1
+      )
+    )
+  $ group "Stake distribution" (
+      check "Stake fractions are positive" (
+        ∀ nPools : RangedNat 500 5000,
+        ((stakeDistribution nPools.value).map (fun x ↦ decide $ x > 0)).and
+      )
+    $ check "Stake fractions sum to unity" (
+        ∀ nPools : RangedNat 500 5000,
+        nearUnity $ (stakeDistribution nPools.value).sum
+      )
+    )
+  $ group "Quorum" (
+      check "All voters vote and all votes are received" (
+        ∀ τ : RangedFloat 0.51 0.80,
+        ∀ committeeSize : RangedNat 100 800,
+        nearUnity $ pQuorum 1 committeeSize.value.toFloat τ.value
+      )
+    )
+  $ group "Conservation of probability" (
+      check "Forging RB" (
+        ∀ env : Environment,
+        ∀ state : State,
+        outcomeNearUnity $ @forgeRb env state
+      )
+    $ check "Certifying" (
+        ∀ env : Environment,
+        ∀ state : State,
+        outcomeNearUnity $ @certify env state
+      )
+    $ check "Forging EB" (
+        ∀ env : Environment,
+        ∀ state : State,
+        outcomeNearUnity $ @forgeEb env state
+      )
+    $ check "Voting" (
+        ∀ env : Environment,
+        ∀ state : State,
+        outcomeNearUnity $ @vote env state
+      )
+    $ check "Simulation" (
+        ∀ env : Environment,
+        ∀ steps : RangedNat 0 30,
+        nearUnity ∘ totalProbability $ simulate env default 0 steps.value
+      )
+    )
+  $ group "EB distribution" (
+      check "Total probability is unity" (
+        ∀ env : Environment,
+        ∀ steps : RangedNat 0 30,
+        let states := simulate env default 0 steps.value
+        let ebDist := ebDistribution states
+        nearUnity $ ebDist.values.sum
+      )
+    )
+  $ group "Efficiency" (
+      group "RB efficiency" (
+        check "Honest environment" (
+          ∀ steps : RangedNat 1 30,
+          let states := simulate default default 0 steps.value
+          nearUnity $ rbEfficiency states
+        )
+      $ check "Adversarial environment" (
+          ∀ fAdversary : RangedFloat 0.01 0.49,
+          let env := {(default : Environment) with fAdversary := fAdversary.value}
+          let states := simulate env default 0 30
+          nearValue (1 - fAdversary.value) $ rbEfficiency states
+        )
+      )
+    $ group "EB efficiency" (
+        check "Ideal environment" (
+          let states := simulate default default 0 30
+          nearValue (0.95^13) $ ebEfficiency states
+        )
+      $ check "Quorum failure" (
+          ∀ τ : RangedFloat 0.90 1.00,
+          let env := makeEnvironment 1 4 7 0.05 600 τ.value 1 1 0 0
+          let states := simulate env default 0 30
+          nearValue (0.95^13 * env.pQuorum) $ ebEfficiency states
+        )
+      $ check "Late EB validation" (
+          ∀ pLate : RangedFloat 0.01 0.99,
+          let env := {(default : Environment) with pLate := pLate.value}
+          let states := simulate env default 0 30
+          nearValue (0.95^13 * (1 - pLate.value)) $ ebEfficiency states
+        )
+      $ check "Adversarial environment" (
+          ∀ fAdversary : RangedFloat 0.01 0.49,
+          let env := {(default : Environment) with fAdversary := fAdversary.value}
+          let states := simulate env default 0 30
+          nearValue (0.95^13 * (1 - fAdversary.value)^2) $ ebEfficiency states
+        )
+      )
+    )
+
+
+/--
+Testing is done elsewhere in this file.
+-/
+def main : IO Unit :=
+  pure ()
diff --git a/analysis/markov/Main.lean b/analysis/markov/src/Main.lean
similarity index 100%
rename from analysis/markov/Main.lean
rename to analysis/markov/src/Main.lean