diff --git a/Benchmarks/Compile/CompileFLT.lean b/Benchmarks/Compile/CompileFLT.lean
index 0b3e4b4d..c236c663 100644
--- a/Benchmarks/Compile/CompileFLT.lean
+++ b/Benchmarks/Compile/CompileFLT.lean
@@ -1,2 +1 @@
 import FLT
-
diff --git a/Ix.lean b/Ix.lean
index 55a400b6..72e3a116 100644
--- a/Ix.lean
+++ b/Ix.lean
@@ -1,14 +1,15 @@
 -- This module serves as the root of the `Ix` library.
 -- Import modules here that should be built as part of the library.
-import Ix.Environment
-import Ix.CanonM
-import Ix.Ixon
-import Ix.Sharing
-import Ix.Meta
-import Ix.GraphM
-import Ix.CondenseM
-import Ix.CompileM
-import Ix.DecompileM
-import Ix.Claim
-import Ix.Commit
-import Ix.Benchmark.Bench
+module
+public import Ix.Environment
+public import Ix.CanonM
+public import Ix.Ixon
+public import Ix.Sharing
+public import Ix.Meta
+public import Ix.GraphM
+public import Ix.CondenseM
+public import Ix.CompileM
+public import Ix.DecompileM
+public import Ix.Claim
+public import Ix.Commit
+public import Ix.Benchmark.Bench
diff --git a/Ix/Address.lean b/Ix/Address.lean
index ee11eb85..e6530497 100644
--- a/Ix/Address.lean
+++ b/Ix/Address.lean
@@ -1,7 +1,10 @@
-import Lean
-import Ix.ByteArray
-import Ix.Common
-import Blake3
+module
+public import Lean.ToExpr
+public import Ix.ByteArray
+public import Ix.Common
+public import Blake3
+
+public section
 
 deriving instance Lean.ToExpr for ByteArray
 deriving instance Repr for ByteArray
@@ -117,3 +120,4 @@ def Address.fromUniqueName (name: Lean.Name) : Option Address :=
   | .str (.str (.str .anonymous "Ix") "_#") s => Address.fromString s
   | _ => .none
 
+end
diff --git a/Ix/Aiur/Bytecode.lean b/Ix/Aiur/Bytecode.lean
index 7fbbec8e..78abfc95 100644
--- a/Ix/Aiur/Bytecode.lean
+++ b/Ix/Aiur/Bytecode.lean
@@ -1,4 +1,7 @@
-import Ix.Aiur.Goldilocks
+module
+public import Ix.Aiur.Goldilocks
+
+public section
 
 namespace Aiur
 
@@ -76,3 +79,5 @@ structure Toplevel where
 end Bytecode
 
 end Aiur
+
+end
diff --git a/Ix/Aiur/Check.lean b/Ix/Aiur/Check.lean
index 0b76c57d..8a560e25 100644
--- a/Ix/Aiur/Check.lean
+++ b/Ix/Aiur/Check.lean
@@ -1,5 +1,8 @@
-import Ix.Aiur.Term
-import Std.Data.HashSet
+module
+public import Ix.Aiur.Term
+public import Std.Data.HashSet
+
+public section
 
 namespace Aiur
 
@@ -473,3 +476,5 @@ def checkFunction (function : Function) : CheckM TypedFunction := do
   pure ⟨function.name, function.inputs, function.output, body, function.unconstrained⟩
 
 end Aiur
+
+end
diff --git a/Ix/Aiur/Compile.lean b/Ix/Aiur/Compile.lean
index 3d6d5f5b..db6ae047 100644
--- a/Ix/Aiur/Compile.lean
+++ b/Ix/Aiur/Compile.lean
@@ -1,7 +1,10 @@
-import Std.Data.HashMap
-import Lean.Data.RBTree
-import Ix.Aiur.Term
-import Ix.Aiur.Bytecode
+module
+public import Std.Data.HashMap
+public import Lean.Data.RBTree
+public import Ix.Aiur.Term
+public import Ix.Aiur.Bytecode
+
+public section
 
 namespace Aiur
 
@@ -643,3 +646,5 @@ def TypedDecls.compile (decls : TypedDecls) : Except String Bytecode.Toplevel :=
   pure ⟨functions, memSizes.toArray⟩
 
 end Aiur
+
+end
diff --git a/Ix/Aiur/Goldilocks.lean b/Ix/Aiur/Goldilocks.lean
index 533452d6..d997400e 100644
--- a/Ix/Aiur/Goldilocks.lean
+++ b/Ix/Aiur/Goldilocks.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 namespace Aiur
 
 abbrev gSize : UInt64 := 1 - 2 ^ 32
@@ -19,3 +23,5 @@ instance : OfNat G n := ⟨G.ofNat n⟩
   ⟨u64, h⟩
 
 end Aiur
+
+end
diff --git a/Ix/Aiur/Match.lean b/Ix/Aiur/Match.lean
index 510f17dd..9a7e8685 100644
--- a/Ix/Aiur/Match.lean
+++ b/Ix/Aiur/Match.lean
@@ -1,5 +1,8 @@
-import Ix.Aiur.Term
-import Ix.SmallMap
+module
+public import Ix.Aiur.Term
+public import Ix.SmallMap
+
+public section
 
 namespace Aiur
 
@@ -236,3 +239,5 @@ partial def decisionToTerm : Decision → Option Term
 end
 
 end Aiur
+
+end
diff --git a/Ix/Aiur/Meta.lean b/Ix/Aiur/Meta.lean
index c68470b2..6281075a 100644
--- a/Ix/Aiur/Meta.lean
+++ b/Ix/Aiur/Meta.lean
@@ -1,5 +1,9 @@
-import Lean
-import Ix.Aiur.Term
+module
+public import Lean.Elab
+public import Lean.Elab.Term.TermElabM
+public import Ix.Aiur.Term
+
+public meta section
 
 namespace Aiur
 
@@ -492,3 +496,5 @@ def elabToplevel : ElabStxCat `toplevel
 elab "⟦" t:toplevel "⟧" : term => elabToplevel t
 
 end Aiur
+
+end
diff --git a/Ix/Aiur/Protocol.lean b/Ix/Aiur/Protocol.lean
index 357608d8..36482f90 100644
--- a/Ix/Aiur/Protocol.lean
+++ b/Ix/Aiur/Protocol.lean
@@ -1,5 +1,8 @@
-import Ix.Aiur.Bytecode
-import Std.Data.HashMap
+module
+public import Ix.Aiur.Bytecode
+public import Std.Data.HashMap
+
+public section
 
 namespace Aiur
 
@@ -76,3 +79,5 @@ def buildClaim (funIdx : Bytecode.FunIdx) (input output : Array G) :=
   #[functionChannel, .ofNat funIdx] ++ input ++ output
 
 end Aiur
+
+end
diff --git a/Ix/Aiur/Simple.lean b/Ix/Aiur/Simple.lean
index 5a930545..aadf71e8 100644
--- a/Ix/Aiur/Simple.lean
+++ b/Ix/Aiur/Simple.lean
@@ -1,5 +1,8 @@
-import Ix.Aiur.Match
-import Ix.Aiur.Check
+module
+public import Ix.Aiur.Match
+public import Ix.Aiur.Check
+
+public section
 
 namespace Aiur
 
@@ -47,3 +50,5 @@ def Toplevel.checkAndSimplify (toplevel : Toplevel) : Except CheckError TypedDec
       pure $ typedDecls.insert name (.function f)
 
 end Aiur
+
+end
diff --git a/Ix/Aiur/Term.lean b/Ix/Aiur/Term.lean
index d3ca942a..e6cb8e3d 100644
--- a/Ix/Aiur/Term.lean
+++ b/Ix/Aiur/Term.lean
@@ -1,6 +1,9 @@
-import Std.Data.HashSet.Basic
-import Ix.Aiur.Goldilocks
-import Ix.IndexMap
+module
+public import Std.Data.HashSet.Basic
+public import Ix.Aiur.Goldilocks
+public import Ix.IndexMap
+
+public section
 
 namespace Aiur
 
@@ -272,3 +275,5 @@ partial def DataType.size (dt : DataType) (decls : TypedDecls)
 end
 
 end Aiur
+
+end
diff --git a/Ix/Benchmark/Bench.lean b/Ix/Benchmark/Bench.lean
index 3cbd24db..b9f36757 100644
--- a/Ix/Benchmark/Bench.lean
+++ b/Ix/Benchmark/Bench.lean
@@ -1,11 +1,14 @@
-import Ix.Address
-import Ix.Meta
-import Ix.Cronos
-import Ix.Address
-import Batteries
+module
+public import Ix.Address
+public import Ix.Meta
+public import Ix.Cronos
+public import Ix.Address
+public import Batteries
 
-import Ix.Benchmark.Serde
-import Ix.Benchmark.Tukey
+public import Ix.Benchmark.Serde
+public import Ix.Benchmark.Tukey
+
+public section
 
 open Batteries (RBMap)
 
@@ -329,7 +332,7 @@ def getColumnWidths (report : Array BenchReport) : ColumnWidths :=
 
 -- Centers a string with padded whitespace given the total width
 def padWhitespace (input : String) (width : Nat) : String :=
-  let padWidth := width - input.length 
+  let padWidth := width - input.length
   let leftPad := padWidth / 2
   let rightPad := padWidth - leftPad
   String.ofList (List.replicate leftPad ' ') ++ input ++ (String.ofList (List.replicate rightPad ' '))
@@ -449,3 +452,4 @@ def bgroup {α β : Type} (name: String) (benches : List (Benchmarkable α β))
     IO.FS.writeFile (System.mkFilePath [".", s!"benchmark-report-{name}.md"]) table
   return reports
 
+end
diff --git a/Ix/Benchmark/Change.lean b/Ix/Benchmark/Change.lean
index 8f152160..dbb876b9 100644
--- a/Ix/Benchmark/Change.lean
+++ b/Ix/Benchmark/Change.lean
@@ -1,4 +1,7 @@
-import Ix.Benchmark.Data
+module
+public import Ix.Benchmark.Data
+
+public section
 
 -- TODO: Use in `MeasurementData` and save outliers in `tukey.json`
 structure LabeledSample where
@@ -83,3 +86,5 @@ def changeEstimates (newAvgTimes baseAvgTimes : Distribution) (config : Config)
   let (mean, median) := changeStats newAvgTimes baseAvgTimes
   let changeEstimates := buildChangeEstimates changeDistributions mean median config.confidenceLevel
   (changeEstimates, changeDistributions)
+
+end
diff --git a/Ix/Benchmark/Common.lean b/Ix/Benchmark/Common.lean
index 809b7fda..f72d32d9 100644
--- a/Ix/Benchmark/Common.lean
+++ b/Ix/Benchmark/Common.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 inductive SamplingMode where
   | flat : SamplingMode
   | linear : SamplingMode
@@ -106,3 +110,5 @@ def Float.formatNanos (f : Float) : String :=
     (f / 10 ^ 3).floatPretty 2 ++ "µs"
   else
     f.floatPretty 2  ++ "ns"
+
+end
diff --git a/Ix/Benchmark/Data.lean b/Ix/Benchmark/Data.lean
index d56ad469..b5aa8572 100644
--- a/Ix/Benchmark/Data.lean
+++ b/Ix/Benchmark/Data.lean
@@ -1,4 +1,7 @@
-import Ix.Benchmark.Distribution
+module
+public import Ix.Benchmark.Distribution
+
+public section
 
 structure Data where
   d : Array (Nat × Nat)
@@ -50,3 +53,5 @@ def Data.regression (data : Data) (config : Config) (gen : StdGen) : (Distributi
   let stdErr := distribution.stdDev mean
   let estimate : Estimate := { confidenceInterval, pointEstimate, stdErr }
   (distribution, estimate)
+
+end
diff --git a/Ix/Benchmark/Distribution.lean b/Ix/Benchmark/Distribution.lean
index a4a1e45a..a8da003d 100644
--- a/Ix/Benchmark/Distribution.lean
+++ b/Ix/Benchmark/Distribution.lean
@@ -1,5 +1,8 @@
-import Ix.Benchmark.Common
-import Ix.Benchmark.Estimate
+module
+public import Ix.Benchmark.Common
+public import Ix.Benchmark.Estimate
+
+public section
 
 -- TODO: Ensure all array instances are used linearly for optimal performance
 structure Distribution where
@@ -117,3 +120,5 @@ def Distribution.estimates (avgTimes : Distribution) (config : Config) (gen : St
   let dists := ((avgTimes.bootstrap config.numSamples config.bootstrapSamples).run gen).fst
   let est := dists.buildEstimates points config.confidenceLevel
   (dists, est)
+
+end
diff --git a/Ix/Benchmark/Estimate.lean b/Ix/Benchmark/Estimate.lean
index 1bb5e0e5..1a8748f7 100644
--- a/Ix/Benchmark/Estimate.lean
+++ b/Ix/Benchmark/Estimate.lean
@@ -1,4 +1,7 @@
-import Lean.Data.Json
+module
+public import Lean.Data.Json
+
+public section
 
 structure ConfidenceInterval where
   confidenceLevel : Float
@@ -26,3 +29,4 @@ structure PointEstimates where
   medianAbsDev : Float
   stdDev : Float
 
+end
diff --git a/Ix/Benchmark/OneShot.lean b/Ix/Benchmark/OneShot.lean
index ceb189c0..30ee8340 100644
--- a/Ix/Benchmark/OneShot.lean
+++ b/Ix/Benchmark/OneShot.lean
@@ -1,6 +1,10 @@
-import Lean.Data.Json.FromToJson
+module
+public import Lean.Data.Json.FromToJson
+
+public section
 
 structure OneShot where
   benchTime : Nat
   deriving Lean.ToJson, Lean.FromJson, Repr
 
+end
diff --git a/Ix/Benchmark/Serde.lean b/Ix/Benchmark/Serde.lean
index 3937f3ff..b3fe3730 100644
--- a/Ix/Benchmark/Serde.lean
+++ b/Ix/Benchmark/Serde.lean
@@ -1,6 +1,9 @@
-import Ix.Ixon
-import Ix.Benchmark.Change
-import Ix.Benchmark.OneShot
+module
+public import Ix.Ixon
+public import Ix.Benchmark.Change
+public import Ix.Benchmark.OneShot
+
+public section
 
 open Ixon
 
@@ -154,3 +157,5 @@ def loadFile [Lean.FromJson α] [Serialize α] (format : SerdeFormat) (path : Sy
   match format with
   | .json => loadJson path
   | .ixon => loadIxon path
+
+end
diff --git a/Ix/Benchmark/Tukey.lean b/Ix/Benchmark/Tukey.lean
index b841ac7e..80a38e27 100644
--- a/Ix/Benchmark/Tukey.lean
+++ b/Ix/Benchmark/Tukey.lean
@@ -1,4 +1,7 @@
-import Ix.Benchmark.Distribution
+module
+public import Ix.Benchmark.Distribution
+
+public section
 
 /-- Outliers are classified per https://bheisler.github.io/criterion.rs/book/analysis.html#outlier-classification -/
 structure Outliers where
@@ -47,3 +50,5 @@ def Distribution.tukey (data : Distribution) : IO Unit := do
     if out.highSevere > 0 then
       let pct := Float.ofNat out.highSevere / (Float.ofNat samples) * 100
       IO.println s!"  {out.highSevere} ({pct.floatPretty 2}%) high severe"
+
+end
diff --git a/Ix/ByteArray.lean b/Ix/ByteArray.lean
index be672e80..06f56e2b 100644
--- a/Ix/ByteArray.lean
+++ b/Ix/ByteArray.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 namespace ByteArray
 
 def beqNoFFI (a b : ByteArray) : Bool :=
@@ -10,3 +14,5 @@ def beq : @& ByteArray → @& ByteArray → Bool :=
 instance : BEq ByteArray := ⟨ByteArray.beq⟩
 
 end ByteArray
+
+end
diff --git a/Ix/CanonM.lean b/Ix/CanonM.lean
index b7462b12..19246409 100644
--- a/Ix/CanonM.lean
+++ b/Ix/CanonM.lean
@@ -1,3 +1,4 @@
+module
 /-
   # CanonM: Canonicalize Lean types to Ix types with content-addressed hashing
 
@@ -16,12 +17,11 @@
   - `compareEnvsParallel`: parallel structural equality check between environments
 -/
 
-import Lean
-import Blake3
-import Std.Data.HashMap
-import Ix.Common
-import Ix.Environment
-import Ix.Address
+public import Ix.Common
+public import Ix.Environment
+public import Ix.Address
+
+public section
 
 namespace Ix.CanonM
 
@@ -772,3 +772,4 @@ def uncanonEnvParallel (consts : HashMap Ix.Name Ix.ConstantInfo) (numWorkers :
 
 end Ix.CanonM
 
+end
diff --git a/Ix/Claim.lean b/Ix/Claim.lean
index 3f7eb8c9..4d180bc5 100644
--- a/Ix/Claim.lean
+++ b/Ix/Claim.lean
@@ -11,7 +11,10 @@
   exposing the full constant.
 -/
 
-import Ix.Ixon
+module
+public import Ix.Ixon
+
+public section
 
 namespace Ix
 
@@ -470,3 +473,5 @@ instance : ToString Claim where
 end Claim
 
 end Ix
+
+end
diff --git a/Ix/Cli/CompileCmd.lean b/Ix/Cli/CompileCmd.lean
index 44701a36..792010b7 100644
--- a/Ix/Cli/CompileCmd.lean
+++ b/Ix/Cli/CompileCmd.lean
@@ -1,8 +1,11 @@
-import Cli
-import Ix.Common
-import Ix.CompileM
-import Ix.Meta
-import Lean
+module
+public import Cli
+public import Ix.Common
+public import Ix.CompileM
+public import Ix.Meta
+public import Batteries.Data.String
+
+public section
 
 open System (FilePath)
 
@@ -67,7 +70,7 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
   -- Machine-readable line for CI benchmark tracking
   IO.println s!"##benchmark## {elapsed} {bytes.size} {totalConsts}"
   return 0
-    
+
 
 def compileCmd : Cli.Cmd := `[Cli|
   compile VIA runCompileCmd;
@@ -76,3 +79,5 @@ def compileCmd : Cli.Cmd := `[Cli|
   FLAGS:
     path : String; "Path to file to compile"
 ]
+
+end
diff --git a/Ix/Cli/ConnectCmd.lean b/Ix/Cli/ConnectCmd.lean
index e8214347..2d26aa64 100644
--- a/Ix/Cli/ConnectCmd.lean
+++ b/Ix/Cli/ConnectCmd.lean
@@ -1,5 +1,8 @@
-import Cli
-import Ix.Iroh.Connect
+module
+public import Cli
+public import Ix.Iroh.Connect
+
+public section
 
 open Iroh.Connect
 
@@ -71,3 +74,5 @@ def connectCmd : Cli.Cmd := `[Cli|
     put;
     get
 ]
+
+end
diff --git a/Ix/Cli/HashCmd.lean b/Ix/Cli/HashCmd.lean
index 3efbd27e..b9c5be45 100644
--- a/Ix/Cli/HashCmd.lean
+++ b/Ix/Cli/HashCmd.lean
@@ -1,3 +1,7 @@
+--module
+--
+--public section
+--
 --import Cli
 --import Ix.Cronos
 --import Ix.Common
@@ -46,3 +50,5 @@
 --  ARGS:
 --    input  : String; "Source file input"
 --]
+--
+--end
diff --git a/Ix/Cli/ProveCmd.lean b/Ix/Cli/ProveCmd.lean
index 82801509..bb9ce6de 100644
--- a/Ix/Cli/ProveCmd.lean
+++ b/Ix/Cli/ProveCmd.lean
@@ -1,3 +1,7 @@
+-- module
+--
+-- public section
+--
 --import Cli
 --import Ix.Cronos
 --import Ix.Common
@@ -99,3 +103,5 @@
 --   input  : String; "Source file input"
 --   const  : String; "constant name"
 --]
+--
+-- end
diff --git a/Ix/Cli/ServeCmd.lean b/Ix/Cli/ServeCmd.lean
index 7ceaab41..896a88f9 100644
--- a/Ix/Cli/ServeCmd.lean
+++ b/Ix/Cli/ServeCmd.lean
@@ -1,5 +1,8 @@
-import Cli
-import Ix.Iroh.Serve
+module
+public import Cli
+public import Ix.Iroh.Serve
+
+public section
 
 open Iroh.Serve
 
@@ -12,3 +15,5 @@ def serveCmd : Cli.Cmd := `[Cli|
   serve VIA runServe;
   "Start an Iroh byte storage server"
 ]
+
+end
diff --git a/Ix/Cli/StoreCmd.lean b/Ix/Cli/StoreCmd.lean
index 174e36f1..3686a878 100644
--- a/Ix/Cli/StoreCmd.lean
+++ b/Ix/Cli/StoreCmd.lean
@@ -1,3 +1,7 @@
+-- module
+--
+-- public section
+--
 --import Cli
 --import Ix.Cronos
 --import Ix.Common
@@ -93,3 +97,5 @@
 --    storeGetCmd;
 --    storeRematCmd
 --]
+--
+-- end
diff --git a/Ix/Commit.lean b/Ix/Commit.lean
index c437e4dd..6133ed75 100644
--- a/Ix/Commit.lean
+++ b/Ix/Commit.lean
@@ -7,10 +7,12 @@
   - Building evaluation, check, and reveal claims
   - Opening committed constants for selective field revelation
 -/
+module
+public import Ix.Claim
+public import Ix.CompileM
+public import Ix.CanonM
 
-import Ix.Claim
-import Ix.CompileM
-import Ix.CanonM
+public section
 
 namespace Ix.Commit
 
@@ -261,3 +263,5 @@ def openCommitment (compileEnv : CompileM.CompileEnv) (commitAddr : Address)
   return openConstantInfo constant.info
 
 end Ix.Commit
+
+end
diff --git a/Ix/Common.lean b/Ix/Common.lean
index 2a38f40f..2aedc497 100644
--- a/Ix/Common.lean
+++ b/Ix/Common.lean
@@ -1,6 +1,11 @@
-import Lean
-import Batteries
-import Batteries.Data.RBMap
+module
+public import Lean.Data.Name
+public import Lean.Expr
+public import Lean.Declaration
+public import Lean.Environment
+public import Lean.Elab.Frontend
+
+public section
 
 def compareList [Ord α] : List α -> List α -> Ordering
 | a::as, b::bs => match compare a b with
@@ -63,7 +68,6 @@ deriving instance BEq, Repr, Ord, Hashable, Inhabited, Nonempty for Lean.Recurso
 deriving instance BEq, Repr, Ord, Hashable, Inhabited, Nonempty for Lean.ConstructorVal
 deriving instance BEq, Repr, Ord, Hashable, Inhabited, Nonempty for Lean.InductiveVal
 deriving instance BEq, Repr, Ord, Hashable, Inhabited, Nonempty for Lean.ConstantInfo
-deriving instance Nonempty for Lean.Environment
 
 def UInt8.MAX : UInt64 := 0xFF
 def UInt16.MAX : UInt64 := 0xFFFF
@@ -333,3 +337,5 @@ def fmtBytes (n : Nat) : String :=
   else
     let gb := n * 10 / (1024 * 1024 * 1024)
     s!"{gb / 10}.{gb % 10} GB"
+
+end
diff --git a/Ix/CompileM.lean b/Ix/CompileM.lean
index e527f62c..2f172b92 100644
--- a/Ix/CompileM.lean
+++ b/Ix/CompileM.lean
@@ -11,20 +11,21 @@
   For performance, use the Rust implementation.
 -/
 
-import Std.Data.HashMap
+module
 import Std.Sync
-import Ix.Ixon
-import Ix.Environment
-import Ix.Sharing
-import Ix.Common
-import Ix.Store
-import Ix.Mutual
-import Ix.GraphM
-import Ix.CondenseM
-import Ix.SOrder
-import Ix.CanonM
+public import Ix.Ixon
+public import Ix.Environment
+public import Ix.Sharing
+public import Ix.Common
+public import Ix.Store
+public import Ix.Mutual
+public import Ix.GraphM
+public import Ix.CondenseM
+public import Ix.SOrder
+public import Ix.CanonM
 
 namespace Ix.CompileM
+public section
 
 -- Need Nonempty for partial function compilation
 instance : Nonempty SOrder := ⟨⟨true, .eq⟩⟩
@@ -1980,4 +1981,5 @@ def rsCompileEnv (leanEnv : Lean.Environment) : IO Ixon.Env := do
   let rawEnv ← rsCompileEnvFFI constList
   pure rawEnv.toEnv
 
+end
 end Ix.CompileM
diff --git a/Ix/CondenseM.lean b/Ix/CondenseM.lean
index 8a1188df..4b662b73 100644
--- a/Ix/CondenseM.lean
+++ b/Ix/CondenseM.lean
@@ -1,3 +1,4 @@
+module
 /-
   # CondenseM: Strongly Connected Component Condensation
 
@@ -16,9 +17,10 @@
   - `blockRefs`: maps each SCC representative to its external references
 -/
 
-import Lean
-import Ix.Common
-import Ix.Environment
+public import Ix.Common
+public import Ix.Environment
+
+public section
 
 namespace Ix
 
@@ -168,3 +170,5 @@ def RustCondensedBlocks.toCondensedBlocks (rust : RustCondensedBlocks) : Condens
   { lowLinks, blocks, blockRefs }
 
 end Ix
+
+end
diff --git a/Ix/Cronos.lean b/Ix/Cronos.lean
index 4b09d3b8..490d8de4 100644
--- a/Ix/Cronos.lean
+++ b/Ix/Cronos.lean
@@ -1,4 +1,7 @@
-import Std.Data.HashMap
+module
+public import Std.Data.HashMap
+
+public section
 
 structure Cronos where
   refs : Std.HashMap String Nat
@@ -43,3 +46,5 @@ def mean (c : Cronos) : Float := Id.run do
   Float.ofNat sum / Float.ofNat c.data.size
 
 end Cronos
+
+end
diff --git a/Ix/DecompileM.lean b/Ix/DecompileM.lean
index d22fb8f7..23b80f6e 100644
--- a/Ix/DecompileM.lean
+++ b/Ix/DecompileM.lean
@@ -1,3 +1,4 @@
+module
 /-
   DecompileM: Decompilation from the Ixon format to Ix types.
 
@@ -10,11 +11,12 @@
   This design enables cheap hash-based comparison of decompiled results.
 -/
 
-import Std.Data.HashMap
-import Ix.Ixon
-import Ix.Address
-import Ix.Environment
-import Ix.Common
+public import Ix.Ixon
+public import Ix.Address
+public import Ix.Environment
+public import Ix.Common
+
+public section
 
 namespace Ix.DecompileM
 
@@ -812,3 +814,5 @@ def rsDecompileEnv (env : Ixon.Env) : Except DecompileError (Std.HashMap Ix.Name
   return arr.foldl (init := {}) fun m (name, info) => m.insert name info
 
 end Ix.DecompileM
+
+end
diff --git a/Ix/Environment.lean b/Ix/Environment.lean
index 7a6aa6b7..6e0beeb7 100644
--- a/Ix/Environment.lean
+++ b/Ix/Environment.lean
@@ -4,12 +4,14 @@
   Ix types mirror Lean's core types but include a Blake3 hash at each node,
   enabling O(1) equality checks and content-addressed storage.
 -/
+module
 
-import Lean
-import Blake3
-import Std.Data.HashMap
-import Batteries.Data.RBMap
-import Ix.Address
+public import Blake3
+public import Std.Data.HashMap
+public import Batteries.Data.RBMap
+public import Ix.Address
+
+public section
 
 namespace Ix
 
@@ -617,3 +619,5 @@ instance : Ord MutCtx where
 abbrev NameSet := Batteries.RBSet Name nameCompare
 
 end Ix
+
+end
diff --git a/Ix/GraphM.lean b/Ix/GraphM.lean
index 74e9fcf1..5e77f4af 100644
--- a/Ix/GraphM.lean
+++ b/Ix/GraphM.lean
@@ -1,7 +1,9 @@
+module
 
-import Lean
-import Ix.Common
-import Ix.Environment
+public import Ix.Common
+public import Ix.Environment
+
+public section
 
 namespace Ix
 
@@ -113,3 +115,5 @@ def GraphM.envSerial (env: Ix.Environment) : Map Ix.Name (Set Ix.Name) := Id.run
   return refs
 
 end Ix
+
+end
diff --git a/Ix/IndexMap.lean b/Ix/IndexMap.lean
index c7f7c238..27ecc8d1 100644
--- a/Ix/IndexMap.lean
+++ b/Ix/IndexMap.lean
@@ -1,4 +1,7 @@
-import Std.Data.HashMap
+module
+public import Std.Data.HashMap
+
+public section
 
 structure IndexMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
   pairs : Array (α × β)
@@ -67,3 +70,5 @@ def map (f : β → β) : IndexMap α β := by
   m.pairs.foldrM f init
 
 end IndexMap
+
+end
diff --git a/Ix/Iroh/Connect.lean b/Ix/Iroh/Connect.lean
index b6af7749..ec770855 100644
--- a/Ix/Iroh/Connect.lean
+++ b/Ix/Iroh/Connect.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 namespace Iroh.Connect
 
 structure PutResponse where
@@ -33,3 +37,5 @@ def getBytes (nodeId : @& String) (addrs : @& Array String) (relayUrl : @& Strin
   | .error e => throw (IO.userError e)
 
 end Iroh.Connect
+
+end
diff --git a/Ix/Iroh/Serve.lean b/Ix/Iroh/Serve.lean
index f91802c3..6a098a63 100644
--- a/Ix/Iroh/Serve.lean
+++ b/Ix/Iroh/Serve.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 namespace Iroh.Serve
 
 @[never_extract, extern "c_rs_iroh_serve"]
@@ -9,3 +13,5 @@ def serve : IO Unit :=
   | .error e => throw (IO.userError e)
 
 end Iroh.Serve
+
+end
diff --git a/Ix/IxVM.lean b/Ix/IxVM.lean
index 8cab2964..005838ff 100644
--- a/Ix/IxVM.lean
+++ b/Ix/IxVM.lean
@@ -1,9 +1,12 @@
-import Ix.Aiur.Meta
-import Ix.IxVM.ByteStream
-import Ix.IxVM.Blake3
-import Ix.IxVM.Ixon
-import Ix.IxVM.IxonSerialize
-import Ix.IxVM.IxonDeserialize
+module
+public import Ix.Aiur.Meta
+public import Ix.IxVM.ByteStream
+public import Ix.IxVM.Blake3
+public import Ix.IxVM.Ixon
+public import Ix.IxVM.IxonSerialize
+public import Ix.IxVM.IxonDeserialize
+
+public section
 
 namespace IxVM
 
@@ -40,3 +43,5 @@ def ixVM : Except Aiur.Global Aiur.Toplevel := do
   vm.merge entrypoints
 
 end IxVM
+
+end
diff --git a/Ix/IxVM/Blake3.lean b/Ix/IxVM/Blake3.lean
index 219d0560..0603a4e0 100644
--- a/Ix/IxVM/Blake3.lean
+++ b/Ix/IxVM/Blake3.lean
@@ -1,4 +1,7 @@
-import Ix.Aiur.Meta
+module
+public import Ix.Aiur.Meta
+
+public section
 
 namespace IxVM
 
@@ -439,3 +442,5 @@ def blake3 := ⟦
 ⟧
 
 end IxVM
+
+end
diff --git a/Ix/IxVM/ByteStream.lean b/Ix/IxVM/ByteStream.lean
index fec0658b..c63e27d6 100644
--- a/Ix/IxVM/ByteStream.lean
+++ b/Ix/IxVM/ByteStream.lean
@@ -1,4 +1,7 @@
-import Ix.Aiur.Meta
+module
+public import Ix.Aiur.Meta
+
+public section
 
 namespace IxVM
 
@@ -195,3 +198,5 @@ def byteStream := ⟦
 ⟧
 
 end IxVM
+
+end
diff --git a/Ix/IxVM/Ixon.lean b/Ix/IxVM/Ixon.lean
index e568ba6c..a7e07976 100644
--- a/Ix/IxVM/Ixon.lean
+++ b/Ix/IxVM/Ixon.lean
@@ -1,4 +1,7 @@
-import Ix.Aiur.Meta
+module
+public import Ix.Aiur.Meta
+
+public section
 
 namespace IxVM
 
@@ -162,3 +165,5 @@ def ixon := ⟦
 ⟧
 
 end IxVM
+
+end
diff --git a/Ix/IxVM/IxonDeserialize.lean b/Ix/IxVM/IxonDeserialize.lean
index c71f1a79..618e9b01 100644
--- a/Ix/IxVM/IxonDeserialize.lean
+++ b/Ix/IxVM/IxonDeserialize.lean
@@ -1,4 +1,7 @@
-import Ix.Aiur.Meta
+module
+public import Ix.Aiur.Meta
+
+public section
 
 namespace IxVM
 
@@ -6,3 +9,5 @@ def ixonDeserialize := ⟦
 ⟧
 
 end IxVM
+
+end
diff --git a/Ix/IxVM/IxonSerialize.lean b/Ix/IxVM/IxonSerialize.lean
index df959386..583844e8 100644
--- a/Ix/IxVM/IxonSerialize.lean
+++ b/Ix/IxVM/IxonSerialize.lean
@@ -1,4 +1,7 @@
-import Ix.Aiur.Meta
+module
+public import Ix.Aiur.Meta
+
+public section
 
 namespace IxVM
 
@@ -556,3 +559,5 @@ def ixonSerialize := ⟦
 ⟧
 
 end IxVM
+
+end
diff --git a/Ix/IxVM/Sha256.lean b/Ix/IxVM/Sha256.lean
index 26edc3e9..09e6528e 100644
--- a/Ix/IxVM/Sha256.lean
+++ b/Ix/IxVM/Sha256.lean
@@ -1,4 +1,7 @@
-import Ix.Aiur.Meta
+module
+public import Ix.Aiur.Meta
+
+public section
 
 namespace IxVM
 
@@ -808,3 +811,7 @@ def sha256 := ⟦
     u32_be_add(«W_i-16», u32_be_add(«W_i_s0», u32_be_add(«W_i-7», «W_i_s1»)))
   }
 ⟧
+
+end IxVM
+
+end
diff --git a/Ix/Ixon.lean b/Ix/Ixon.lean
index 5432d12c..dd3f1113 100644
--- a/Ix/Ixon.lean
+++ b/Ix/Ixon.lean
@@ -7,9 +7,12 @@
   - Expr, Univ, and Constant types matching Rust exactly
   - All numeric fields use UInt64 (matching Rust's u64)
 -/
-import Ix.Address
-import Ix.Common
-import Ix.Environment
+module
+public import Ix.Address
+public import Ix.Common
+public import Ix.Environment
+
+public section
 
 namespace Ixon
 
@@ -1830,3 +1833,5 @@ def rsDesEnv (bytes : ByteArray) : Except String Env :=
   return (← rsDesEnvFFI bytes).toEnv
 
 end Ixon
+
+end
diff --git a/Ix/Keccak.lean b/Ix/Keccak.lean
index b49b8f00..f6107fea 100644
--- a/Ix/Keccak.lean
+++ b/Ix/Keccak.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 namespace Keccak
 
 private opaque GenericNonempty : NonemptyType
@@ -25,3 +29,5 @@ def hash (input : @& ByteArray) : ByteArray :=
   hasher.finalize
 
 end Keccak
+
+end
diff --git a/Ix/Meta.lean b/Ix/Meta.lean
index 3aec1d65..b0a83169 100644
--- a/Ix/Meta.lean
+++ b/Ix/Meta.lean
@@ -1,6 +1,9 @@
-import Lean
-import Ix.Address
-import Ix.CompileM
+module
+public import Lean.Meta.Reduce
+public import Ix.Address
+public import Ix.CompileM
+
+public section
 
 open Lean
 
@@ -60,3 +63,4 @@ def metaMakeEvalClaim (func: Lean.Name) (args : List Lean.Expr)
   let lvls := (Lean.collectLevelParams default input).params.toList
   return (lvls, input, output, type, sort)
 
+end
diff --git a/Ix/Mutual.lean b/Ix/Mutual.lean
index 92019815..2259a073 100644
--- a/Ix/Mutual.lean
+++ b/Ix/Mutual.lean
@@ -1,7 +1,8 @@
-import Ix.Common
-import Ix.Address
-import Ix.Environment
-import Lean
+module
+public import Ix.Common
+public import Ix.Address
+public import Ix.Environment
+public section
 
 namespace Ix
 
@@ -120,3 +121,5 @@ def MutConst.ctx (classes: List (List MutConst)) : Ix.MutCtx
   return mutCtx
 
 end Ix
+
+end
diff --git a/Ix/SOrder.lean b/Ix/SOrder.lean
index 661fbdf2..a56dce3c 100644
--- a/Ix/SOrder.lean
+++ b/Ix/SOrder.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 /-- an Ordering with a boolean strength --/
 structure SOrder where
   strong: Bool
@@ -39,7 +43,7 @@ def zip (f: α -> α -> SOrder) : List α -> List α -> SOrder
 | [] , [] => ⟨true, .eq⟩
 | [], _ => ⟨true, .lt⟩
 | _, [] => ⟨true, .gt⟩
-| x::xs, y::ys => 
+| x::xs, y::ys =>
   match f x y with
   | a@⟨_, .eq⟩ => cmp a (zip f xs ys)
   | a => a
@@ -55,3 +59,5 @@ def zipM [Monad μ] (f: α -> α -> μ SOrder)
     | a => pure a
 
 end SOrder
+
+end
diff --git a/Ix/ShardMap.lean b/Ix/ShardMap.lean
index c918031e..ef1eca26 100644
--- a/Ix/ShardMap.lean
+++ b/Ix/ShardMap.lean
@@ -35,9 +35,12 @@
     -- Atomic read-modify-write
     let result? ← map.modifyGet key fun v => (computeResult v, updateValue v)
 -/
+module
 
-import Std.Data.HashMap
-import Std.Sync.SharedMutex
+public import Std.Data.HashMap
+public import Std.Sync.SharedMutex
+
+public section
 
 namespace Ix
 
@@ -444,3 +447,5 @@ def newWithCapacity (shardBits : Nat := 8) (capacityPerShard : Nat := 64)
 end ShardMap
 
 end Ix
+
+end
diff --git a/Ix/Sharing.lean b/Ix/Sharing.lean
index ddffb72f..c0eec6b9 100644
--- a/Ix/Sharing.lean
+++ b/Ix/Sharing.lean
@@ -12,12 +12,15 @@
   4. Build sharing vector in topological order (leaves first)
   5. Rewrite expressions with Share(idx) references
 -/
+module
 
-import Ix.Ixon
-import Ix.Address
-import Ix.Common
-import Std.Data.HashMap
-import Blake3
+public import Ix.Ixon
+public import Ix.Address
+public import Ix.Common
+public import Std.Data.HashMap
+public import Blake3
+
+public section
 
 namespace Ix.Sharing
 
@@ -507,3 +510,5 @@ def applySharing (exprs : Array Ixon.Expr) (dbg : Bool := false)
     return buildSharingVec exprs sharedHashes result.infoMap result.ptrToHash
 
 end Ix.Sharing
+
+end
diff --git a/Ix/SmallMap.lean b/Ix/SmallMap.lean
index 57675198..e9b87a27 100644
--- a/Ix/SmallMap.lean
+++ b/Ix/SmallMap.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 /-- A map meant for very few entries, preserving insertion order. -/
 structure SmallMap (α : Type u) (β : Type v) where
   pairs : Array (α × β)
@@ -30,3 +34,5 @@ def update (f : β → β) : SmallMap α β :=
   m.pairs.toList
 
 end SmallMap
+
+end
diff --git a/Ix/Store.lean b/Ix/Store.lean
index dbde4657..c5b0092f 100644
--- a/Ix/Store.lean
+++ b/Ix/Store.lean
@@ -1,8 +1,8 @@
-import Ix.Address
+module
 
-import Init.System.FilePath
-import Init.System.IO
-import Init.System.IOError
+public import Ix.Address
+
+public section
 
 open System
 
@@ -62,3 +62,5 @@ def read (a: Address) : StoreIO ByteArray := do
   IO.toEIO .ioError (IO.FS.readBinFile path)
 
 end Store
+
+end
diff --git a/Ix/UnionFind.lean b/Ix/UnionFind.lean
index 4c2c087a..83c2631e 100644
--- a/Ix/UnionFind.lean
+++ b/Ix/UnionFind.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 structure UnionFind where
   parent : IO.Ref (Array Nat)
   rank : IO.Ref (Array Nat)
@@ -39,3 +43,4 @@ def unionMany (uf: UnionFind) (pairs: Array (Nat × Nat)) : IO Unit := do
 
 end UnionFind
 
+end
diff --git a/Ix/Unsigned.lean b/Ix/Unsigned.lean
index 2fe1f70e..6249b70b 100644
--- a/Ix/Unsigned.lean
+++ b/Ix/Unsigned.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 @[extern "c_u16_to_le_bytes"]
 opaque UInt16.toLEBytes : UInt16 → ByteArray
 
@@ -9,3 +13,5 @@ opaque UInt64.toLEBytes : UInt64 → ByteArray
 
 @[extern "c_usize_to_le_bytes"]
 opaque USize.toLEBytes : USize → ByteArray
+
+end
diff --git a/Tests/Aiur.lean b/Tests/Aiur.lean
index 6dc81075..043a2ae0 100644
--- a/Tests/Aiur.lean
+++ b/Tests/Aiur.lean
@@ -1,3 +1,5 @@
-import Tests.Aiur.Common
-import Tests.Aiur.Aiur
-import Tests.Aiur.Hashes
+module
+
+public import Tests.Aiur.Common
+public import Tests.Aiur.Aiur
+public import Tests.Aiur.Hashes
diff --git a/Tests/Aiur/Aiur.lean b/Tests/Aiur/Aiur.lean
index 50e07246..f49afee8 100644
--- a/Tests/Aiur/Aiur.lean
+++ b/Tests/Aiur/Aiur.lean
@@ -1,5 +1,9 @@
-import Tests.Aiur.Common
-import Ix.Aiur.Meta
+module
+
+public import Tests.Aiur.Common
+public import Ix.Aiur.Meta
+
+public section
 
 open LSpec
 
@@ -268,3 +272,4 @@ def aiurTestCases : List AiurTestCase := [
     .noIO `fold_matrix_sum #[1, 2, 3, 4] #[10],
   ]
 
+end
diff --git a/Tests/Aiur/Common.lean b/Tests/Aiur/Common.lean
index 990cc316..7d55676e 100644
--- a/Tests/Aiur/Common.lean
+++ b/Tests/Aiur/Common.lean
@@ -1,10 +1,14 @@
-import LSpec
-import Tests.Gen.Basic
-import Ix.Unsigned
-import Ix.Aiur.Goldilocks
-import Ix.Aiur.Protocol
-import Ix.Aiur.Simple
-import Ix.Aiur.Compile
+module
+
+public import LSpec
+public import Tests.Gen.Basic
+public import Ix.Unsigned
+public import Ix.Aiur.Goldilocks
+public import Ix.Aiur.Protocol
+public import Ix.Aiur.Simple
+public import Ix.Aiur.Compile
+
+public section
 
 open LSpec SlimCheck Gen
 
@@ -65,3 +69,5 @@ def mkAiurTests (toplevelFn : Except Aiur.Global Aiur.Toplevel)
         let env : AiurTestEnv := ⟨toplevel, aiurSystem⟩
         cases.foldl (init := .done) fun tSeq testCase =>
           tSeq ++ env.runTestCase testCase
+
+end
diff --git a/Tests/Aiur/Hashes.lean b/Tests/Aiur/Hashes.lean
index 1dd0a11e..63d53b9b 100644
--- a/Tests/Aiur/Hashes.lean
+++ b/Tests/Aiur/Hashes.lean
@@ -1,8 +1,10 @@
-import Tests.Aiur.Common
-import Ix.IxVM.ByteStream
-import Ix.IxVM.Blake3
-import Ix.IxVM.Sha256
-import Blake3
+module
+
+public import Tests.Aiur.Common
+public import Ix.IxVM.ByteStream
+public import Ix.IxVM.Blake3
+public import Ix.IxVM.Sha256
+public import Blake3
 
 @[extern "rs_sha256"]
 opaque rsSha256 : @&ByteArray → ByteArray
@@ -23,7 +25,7 @@ def mkSha256HashTestCase (size : Nat) : AiurTestCase :=
   let buffer := ⟨input, .ofList [(#[0], ⟨0, size⟩)]⟩ -- key is fixed as #[0]
   ⟨`sha256_test, s!"sha256 (size={size})", #[], output, buffer, buffer⟩
 
-def blake3TestCases : List AiurTestCase := [
+public def blake3TestCases : List AiurTestCase := [
   mkBlake3HashTestCase 0,
   mkBlake3HashTestCase 32,
   mkBlake3HashTestCase 64,
@@ -42,7 +44,7 @@ def blake3TestCases : List AiurTestCase := [
   mkBlake3HashTestCase 3168,
 ]
 
-def sha256TestCases : List AiurTestCase := [
+public def sha256TestCases : List AiurTestCase := [
   mkSha256HashTestCase 0,
   mkSha256HashTestCase 1,
   mkSha256HashTestCase 14,
@@ -57,4 +59,3 @@ def sha256TestCases : List AiurTestCase := [
   mkSha256HashTestCase 120,
   mkSha256HashTestCase 1200,
 ]
-
diff --git a/Tests/ByteArray.lean b/Tests/ByteArray.lean
index c5a519bf..92be1a47 100644
--- a/Tests/ByteArray.lean
+++ b/Tests/ByteArray.lean
@@ -1,5 +1,7 @@
-import LSpec
-import Ix.ByteArray
+module
+
+public import LSpec
+public import Ix.ByteArray
 
 def arrays : List ByteArray := [
   ⟨#[]⟩, ⟨#[1]⟩, ⟨#[0, 3]⟩, ⟨#[1, 1, 1]⟩, ⟨#[3, 3, 3, 3]⟩, ⟨#[13]⟩
@@ -19,4 +21,4 @@ def neq : TestSeq :=
   arrays.zip arrays' |>.foldl (init := .done) fun tSeq (x, y) =>
     tSeq ++ (test s!"{x} != {y}" $ !x.beq y && !x.beqNoFFI y && !y.beq x && !y.beqNoFFI x)
 
-def Tests.ByteArray.suite := [beq, neq]
+public def Tests.ByteArray.suite := [beq, neq]
diff --git a/Tests/Cli.lean b/Tests/Cli.lean
index 26170235..58c60e13 100644
--- a/Tests/Cli.lean
+++ b/Tests/Cli.lean
@@ -1,3 +1,5 @@
+module
+
 /- Integration tests for the Ix CLI -/
 
 def Tests.Cli.run (buildCmd: String) (buildArgs : Array String) (buildDir : Option System.FilePath) : IO Unit := do
@@ -12,7 +14,7 @@ def Tests.Cli.run (buildCmd: String) (buildArgs : Array String) (buildDir : Opti
   else
     IO.println out.stdout
 
-def Tests.Cli.suite : IO UInt32 := do
+public def Tests.Cli.suite : IO UInt32 := do
   Tests.Cli.run "lake" (#["exe", "ix", "--help"]) none
   --Tests.Cli.run "ix" (#["store", "ix_test/IxTest.lean"]) none
   --Tests.Cli.run "ix" (#["prove", "ix_test/IxTest.lean", "one"]) none
diff --git a/Tests/FFI.lean b/Tests/FFI.lean
index 9950e931..6c98b2e1 100644
--- a/Tests/FFI.lean
+++ b/Tests/FFI.lean
@@ -2,14 +2,15 @@
   FFI test suite aggregator.
   Imports all Tests.FFI.* modules and exports a combined suite.
 -/
+module
 
-import Tests.FFI.Basic
-import Tests.FFI.Ix
-import Tests.FFI.Ixon
+public import Tests.FFI.Basic
+public import Tests.FFI.Ix
+public import Tests.FFI.Ixon
 
 namespace Tests.FFI
 
-def suite : List LSpec.TestSeq :=
+public def suite : List LSpec.TestSeq :=
   Tests.FFI.Basic.suite ++ Tests.FFI.Ix.suite ++ Tests.FFI.Ixon.suite
 
 end Tests.FFI
diff --git a/Tests/FFI/Basic.lean b/Tests/FFI/Basic.lean
index aac3d543..37462f6d 100644
--- a/Tests/FFI/Basic.lean
+++ b/Tests/FFI/Basic.lean
@@ -2,10 +2,11 @@
   Basic type FFI roundtrip tests.
   Pattern: Lean value → Rust (decode) → Rust (re-encode via C API) → Lean value → compare
 -/
+module
 
-import LSpec
-import Tests.Gen.Basic
-import Std.Data.HashMap
+public import LSpec
+public import Tests.Gen.Basic
+public import Std.Data.HashMap
 
 open LSpec SlimCheck Gen
 
@@ -116,7 +117,7 @@ def boolTests : TestSeq :=
 
 /-! ## Test Suite -/
 
-def suite : List TestSeq := [
+public def suite : List TestSeq := [
   simpleTests,
   largeNatTests,
   assocListTests,
diff --git a/Tests/FFI/Ix.lean b/Tests/FFI/Ix.lean
index a103fc61..3a13de6a 100644
--- a/Tests/FFI/Ix.lean
+++ b/Tests/FFI/Ix.lean
@@ -2,17 +2,18 @@
   Ix.* type FFI roundtrip tests.
   Pattern: Lean value → Rust (decode) → Rust (re-encode via C API) → Lean value → compare
 -/
-
-import LSpec
-import Tests.Gen.Basic
-import Tests.Gen.Ix
-import Tests.Gen.Ixon
-import Ix.Environment
-import Ix.Address
-import Ix.CompileM
-import Ix.DecompileM
-import Ix.Ixon
-import Tests.FFI.Ixon
+module
+
+public import LSpec
+public import Tests.Gen.Basic
+public import Tests.Gen.Ix
+public import Tests.Gen.Ixon
+public import Ix.Environment
+public import Ix.Address
+public import Ix.CompileM
+public import Ix.DecompileM
+public import Ix.Ixon
+public import Tests.FFI.Ixon
 
 open LSpec SlimCheck Gen
 open Tests.Gen.Ix
@@ -253,7 +254,7 @@ def compileErrorTests : TestSeq :=
 
 /-! ## Test Suite -/
 
-def suite : List TestSeq := [
+public def suite : List TestSeq := [
   -- Block comparison types
   blockCompareResultTests,
   blockCompareDetailTests,
diff --git a/Tests/FFI/Ixon.lean b/Tests/FFI/Ixon.lean
index 64b828f3..1e18e3cb 100644
--- a/Tests/FFI/Ixon.lean
+++ b/Tests/FFI/Ixon.lean
@@ -2,10 +2,13 @@
   Ixon.* type FFI roundtrip tests.
   Pattern: Lean value → Rust (decode) → Rust (re-encode via C API) → Lean value → compare
 -/
+module
 
-import LSpec
-import Tests.Gen.Ixon
-import Ix.Ixon
+public import LSpec
+public import Tests.Gen.Ixon
+public import Ix.Ixon
+
+public section
 
 open LSpec SlimCheck Gen Ixon
 open Ix (DefKind DefinitionSafety QuotKind)
@@ -307,3 +310,5 @@ def suite : List TestSeq := [
 ]
 
 end Tests.FFI.Ixon
+
+end
diff --git a/Tests/Gen/Basic.lean b/Tests/Gen/Basic.lean
index 4c146f37..c0019f73 100644
--- a/Tests/Gen/Basic.lean
+++ b/Tests/Gen/Basic.lean
@@ -2,9 +2,12 @@
   Basic type generators for testing.
   Generators and test types for property-based FFI roundtrip tests.
 -/
+module
 
-import LSpec
-import Std.Data.HashMap
+public import LSpec
+public import Std.Data.HashMap
+
+public section
 
 open LSpec SlimCheck Gen
 
@@ -180,3 +183,5 @@ instance : SampleableExt Point := SampleableExt.mkSelfContained genPoint
 instance : SampleableExt NatTree := SampleableExt.mkSelfContained (genNatTree 4)
 
 instance : SampleableExt (Std.HashMap Nat Nat) := SampleableExt.mkSelfContained genHashMapNatNat
+
+end
diff --git a/Tests/Gen/Claim.lean b/Tests/Gen/Claim.lean
index 303cb6c9..f9230fc8 100644
--- a/Tests/Gen/Claim.lean
+++ b/Tests/Gen/Claim.lean
@@ -1,10 +1,13 @@
 /-
   Generators for Ix.Claim types (RevealConstructorInfo, RevealRecursorRule, etc.).
 -/
+module
 
-import LSpec
-import Tests.Gen.Ixon
-import Ix.Claim
+public import LSpec
+public import Tests.Gen.Ixon
+public import Ix.Claim
+
+public section
 
 open LSpec SlimCheck Gen
 open Ix (RevealConstructorInfo RevealRecursorRule RevealMutConstInfo RevealConstantInfo Claim
@@ -128,3 +131,5 @@ instance : SampleableExt RevealConstantInfo := SampleableExt.mkSelfContained gen
 instance : SampleableExt Claim := SampleableExt.mkSelfContained genClaim
 
 end Tests.Gen.Claim
+
+end
diff --git a/Tests/Gen/Ix.lean b/Tests/Gen/Ix.lean
index a4e8532a..013af41e 100644
--- a/Tests/Gen/Ix.lean
+++ b/Tests/Gen/Ix.lean
@@ -2,15 +2,18 @@
   Generators for Ix.* types (canonical Lean types with Blake3 hashes).
   Generators for property-based FFI roundtrip tests.
 -/
+module
 
-import LSpec
-import Tests.Gen.Basic
-import Tests.Gen.Ixon
-import Ix.Address
-import Ix.Environment
-import Ix.CondenseM
-import Ix.CompileM
-import Ix.DecompileM
+public import LSpec
+public import Tests.Gen.Basic
+public import Tests.Gen.Ixon
+public import Ix.Address
+public import Ix.Environment
+public import Ix.CondenseM
+public import Ix.CompileM
+public import Ix.DecompileM
+
+public section
 
 open LSpec SlimCheck Gen
 
@@ -676,3 +679,5 @@ instance : SampleableExt Ix.CompileM.CompileError :=
   SampleableExt.mkSelfContained genCompileError
 
 end Tests.Gen.Ix
+
+end
diff --git a/Tests/Gen/Ixon.lean b/Tests/Gen/Ixon.lean
index e74b1eac..71bf9afe 100644
--- a/Tests/Gen/Ixon.lean
+++ b/Tests/Gen/Ixon.lean
@@ -2,11 +2,14 @@
   Generators for Ixon.* types (alpha-invariant serialization format).
   Extracted from Tests/Ix/Ixon.lean.
 -/
+module
 
-import LSpec
-import Tests.Gen.Basic
-import Ix.Ixon
-import Ix.Address
+public import LSpec
+public import Tests.Gen.Basic
+public import Ix.Ixon
+public import Ix.Address
+
+public section
 
 open LSpec SlimCheck Gen Ixon
 open Ix (DefKind DefinitionSafety QuotKind)
@@ -489,3 +492,5 @@ instance : SampleableExt RawComm := SampleableExt.mkSelfContained genRawComm
 instance : SampleableExt RawEnv := SampleableExt.mkSelfContained genRawEnv
 
 end Tests.Gen.Ixon
+
+end
diff --git a/Tests/Ix/CanonM.lean b/Tests/Ix/CanonM.lean
index 9201f9bb..09aaa2cc 100644
--- a/Tests/Ix/CanonM.lean
+++ b/Tests/Ix/CanonM.lean
@@ -2,10 +2,11 @@
   Unit tests for CanonM module - verifies canonicalization roundtrips.
 -/
 
-import Ix.CanonM
-import Ix.Environment
-import Ix.Meta
-import LSpec
+module
+public import Ix.CanonM
+public import Ix.Environment
+public import Ix.Meta
+public import LSpec
 
 open LSpec Ix.CanonM
 
@@ -111,7 +112,7 @@ def testInterning : TestSeq :=
 
 /-! ## Full suite -/
 
-def suite : TestSeq :=
+public def suite : TestSeq :=
   group "CanonM" <|
     testNameRoundtrip ++
     testLevelRoundtrip ++
@@ -489,6 +490,8 @@ def testParallelLeanRoundtrip : TestSeq :=
     pure (success, 0, 0, failMsg)
   ) .done
 
+public section
+
 /-- Full canonicalization roundtrip test suite (expensive, in ignored tests). -/
 def rustSuiteIO : List TestSeq := [
   testFullCanonRoundtrip,
@@ -502,4 +505,7 @@ def parallelSuiteIO : List TestSeq := [
   testParallelLeanRoundtrip
 ]
 
+end
+
 end Tests.CanonM
+
diff --git a/Tests/Ix/Claim.lean b/Tests/Ix/Claim.lean
index f5d0e8ac..d64afb80 100644
--- a/Tests/Ix/Claim.lean
+++ b/Tests/Ix/Claim.lean
@@ -2,8 +2,9 @@
   Serialization roundtrip and encoding tests for Ix.Claim types.
 -/
 
-import Ix.Claim
-import Tests.Gen.Claim
+module
+public import Ix.Claim
+public import Tests.Gen.Claim
 
 open LSpec SlimCheck
 open Ixon (runGet)
@@ -83,7 +84,7 @@ def claimEncodingTests : TestSeq :=
 
 /-! ## Suite -/
 
-def Tests.Claim.suite : List TestSeq := [
+public def Tests.Claim.suite : List TestSeq := [
   claimUnits,
   claimEncodingTests,
   checkIO "Claim serde roundtrips" (∀ c : Claim, claimSerde c),
diff --git a/Tests/Ix/Commit.lean b/Tests/Ix/Commit.lean
index a48345ac..e83d3166 100644
--- a/Tests/Ix/Commit.lean
+++ b/Tests/Ix/Commit.lean
@@ -2,8 +2,9 @@
   Tests for the commitment pipeline and claim construction.
 -/
 
-import LSpec
-import Ix.Commit
+module
+public import LSpec
+public import Ix.Commit
 
 open LSpec
 open Ixon (Comm runGet serCommTagged)
@@ -231,7 +232,7 @@ def commitConstIOTest : TestSeq :=
 
 /-! ## Suite registration -/
 
-def Tests.Commit.suite : List TestSeq := [
+public def Tests.Commit.suite : List TestSeq := [
   commDeterminismTests,
   claimCommitTests,
   fieldCombinationTests,
@@ -239,6 +240,6 @@ def Tests.Commit.suite : List TestSeq := [
   claimConstructorTests,
 ]
 
-def Tests.Commit.suiteIO : List TestSeq := [
+public def Tests.Commit.suiteIO : List TestSeq := [
   commitConstIOTest,
 ]
diff --git a/Tests/Ix/Compile.lean b/Tests/Ix/Compile.lean
index 3d46830c..c9e9bade 100644
--- a/Tests/Ix/Compile.lean
+++ b/Tests/Ix/Compile.lean
@@ -3,18 +3,19 @@
   Verifies Lean and Rust implementations produce equivalent results.
 -/
 
-import Ix.Ixon
-import Ix.Environment
-import Ix.Address
-import Ix.Common
-import Ix.Meta
-import Ix.CompileM
-import Ix.CondenseM
-import Ix.GraphM
-import Ix.Sharing
-import Lean
-import LSpec
-import Tests.Ix.Fixtures
+module
+public import Ix.Ixon
+public import Ix.Environment
+public import Ix.Address
+public import Ix.Common
+public import Ix.Meta
+public import Ix.CompileM
+public import Ix.CondenseM
+public import Ix.GraphM
+public import Ix.Sharing
+public import Lean
+public import LSpec
+public import Tests.Ix.Fixtures
 
 open LSpec
 
@@ -460,7 +461,7 @@ def testCrossImpl : TestSeq :=
 
 /-! ## Test Suite -/
 
-def compileSuiteIO : List TestSeq := [
+public def compileSuiteIO : List TestSeq := [
   testCrossImpl,
 ]
 
diff --git a/Tests/Ix/CondenseM.lean b/Tests/Ix/CondenseM.lean
index db7140da..d8da9d91 100644
--- a/Tests/Ix/CondenseM.lean
+++ b/Tests/Ix/CondenseM.lean
@@ -4,11 +4,12 @@
   - Cross-implementation tests comparing Lean vs Rust SCC results
 -/
 
-import Ix.GraphM
-import Ix.CondenseM
-import Ix.Environment
-import Ix.Meta
-import LSpec
+module
+public import Ix.GraphM
+public import Ix.CondenseM
+public import Ix.Environment
+public import Ix.Meta
+public import LSpec
 
 open LSpec Ix
 
@@ -210,7 +211,7 @@ def testBlockRefsTwoCycles : TestSeq :=
 
 /-! ## Full Test Suite (unit tests) -/
 
-def suite : List TestSeq := [
+public def suite : List TestSeq := [
   group "basic SCCs" (
     testSingleNode ++
     testSimpleCycle ++
@@ -376,7 +377,7 @@ def testSccComparison : TestSeq :=
   ) .done
 
 /-- Cross-implementation test suite (expensive, run with --ignored) -/
-def suiteIO : List TestSeq := [
+public def suiteIO : List TestSeq := [
   testSccComparison
 ]
 
diff --git a/Tests/Ix/Decompile.lean b/Tests/Ix/Decompile.lean
index 1012de79..0e9f698a 100644
--- a/Tests/Ix/Decompile.lean
+++ b/Tests/Ix/Decompile.lean
@@ -4,16 +4,17 @@
   and compares via content hashes.
 -/
 
-import Ix.Ixon
-import Ix.Environment
-import Ix.Address
-import Ix.Common
-import Ix.Meta
-import Ix.CompileM
-import Ix.DecompileM
-import Lean
-import LSpec
-import Tests.Ix.Fixtures
+module
+public import Ix.Ixon
+public import Ix.Environment
+public import Ix.Address
+public import Ix.Common
+public import Ix.Meta
+public import Ix.CompileM
+public import Ix.DecompileM
+public import Lean
+public import LSpec
+public import Tests.Ix.Fixtures
 
 open LSpec
 
@@ -121,7 +122,7 @@ def testDecompile : TestSeq :=
 
 /-! ## Test Suite -/
 
-def decompileSuiteIO : List TestSeq := [
+public def decompileSuiteIO : List TestSeq := [
   testDecompile,
 ]
 
diff --git a/Tests/Ix/Fixtures.lean b/Tests/Ix/Fixtures.lean
index bbb12bcf..7b31159d 100644
--- a/Tests/Ix/Fixtures.lean
+++ b/Tests/Ix/Fixtures.lean
@@ -1,4 +1,7 @@
-import Tests.Ix.Fixtures.Export
+module
+public import Tests.Ix.Fixtures.Export
+
+public section
 
 namespace Test.Ix.Fixtures
 
@@ -175,3 +178,4 @@ end Import
 
 end Test.Ix.Fixtures
 
+end
diff --git a/Tests/Ix/Fixtures/Export.lean b/Tests/Ix/Fixtures/Export.lean
index bc637a05..3d55fda8 100644
--- a/Tests/Ix/Fixtures/Export.lean
+++ b/Tests/Ix/Fixtures/Export.lean
@@ -1,3 +1,9 @@
+module
+
+public section
+
 inductive MyNat
   | nill
   | next : MyNat → MyNat
+
+end
diff --git a/Tests/Ix/Fixtures/Inductives.lean b/Tests/Ix/Fixtures/Inductives.lean
deleted file mode 100644
index e69de29b..00000000
diff --git a/Tests/Ix/Fixtures/Mutual.lean b/Tests/Ix/Fixtures/Mutual.lean
index a8978d0c..8cda4c8a 100644
--- a/Tests/Ix/Fixtures/Mutual.lean
+++ b/Tests/Ix/Fixtures/Mutual.lean
@@ -1,3 +1,7 @@
+module
+
+public section
+
 namespace Test.Ix.Mutual
 
 namespace WellFounded
@@ -160,3 +164,5 @@ inductive BLEH
 end Inductive
 
 end Test.Ix.Mutual
+
+end
diff --git a/Tests/Ix/GraphM.lean b/Tests/Ix/GraphM.lean
index b66f6bc7..5efb78d2 100644
--- a/Tests/Ix/GraphM.lean
+++ b/Tests/Ix/GraphM.lean
@@ -4,10 +4,11 @@
   - Cross-implementation tests comparing Lean vs Rust graph construction
 -/
 
-import Ix.GraphM
-import Ix.Environment
-import Ix.Meta
-import LSpec
+module
+public import Ix.GraphM
+public import Ix.Environment
+public import Ix.Meta
+public import LSpec
 
 open LSpec Ix
 
@@ -313,7 +314,7 @@ def testEnvParallelVsSerial : TestSeq := Id.run do
 
 /-! ## Full Test Suite (unit tests) -/
 
-def suite : List TestSeq := [
+public def suite : List TestSeq := [
   group "graphExpr" (
     testGraphExprConst ++
     testGraphExprBvar ++
@@ -462,7 +463,7 @@ def testRefGraphComparison : TestSeq :=
   ) .done
 
 /-- Cross-implementation test suite (expensive, run with --ignored) -/
-def suiteIO : List TestSeq := [
+public def suiteIO : List TestSeq := [
   testRefGraphComparison
 ]
 
diff --git a/Tests/Ix/Ixon.lean b/Tests/Ix/Ixon.lean
index 5b665fcc..caf6764d 100644
--- a/Tests/Ix/Ixon.lean
+++ b/Tests/Ix/Ixon.lean
@@ -3,10 +3,11 @@
   Generators have been moved to Tests/Gen/Ixon.lean.
 -/
 
-import Ix.Ixon
-import Ix.Sharing
-import Tests.Gen.Ixon
-import Tests.FFI.Ixon
+module
+public import Ix.Ixon
+public import Ix.Sharing
+public import Tests.Gen.Ixon
+public import Tests.FFI.Ixon
 
 open LSpec SlimCheck Gen Ixon
 open Tests.FFI.Ixon (rsEqUnivSerialization rsEqExprSerialization rsEqConstantSerialization rsEqEnvSerialization)
@@ -241,7 +242,7 @@ def envSerializationUnitTests : TestSeq :=
 
 /-! ## Test Suite (property-based) -/
 
-def Tests.Ixon.suite : List TestSeq := [
+public def Tests.Ixon.suite : List TestSeq := [
   -- Env unit tests (for debugging serialization)
   envUnitTests,
   -- Env serialization comparison unit tests
diff --git a/Tests/Ix/RustDecompile.lean b/Tests/Ix/RustDecompile.lean
index 6f150cad..43e8ef4f 100644
--- a/Tests/Ix/RustDecompile.lean
+++ b/Tests/Ix/RustDecompile.lean
@@ -4,16 +4,17 @@
   decompiling with Rust, and comparing against the original environment.
 -/
 
-import Ix.Ixon
-import Ix.Environment
-import Ix.Address
-import Ix.Common
-import Ix.Meta
-import Ix.CompileM
-import Ix.DecompileM
-import Lean
-import LSpec
-import Tests.Ix.Fixtures
+module
+public import Ix.Ixon
+public import Ix.Environment
+public import Ix.Address
+public import Ix.Common
+public import Ix.Meta
+public import Ix.CompileM
+public import Ix.DecompileM
+public import Lean
+public import LSpec
+public import Tests.Ix.Fixtures
 
 open LSpec
 
@@ -119,7 +120,7 @@ def testRustDecompile : TestSeq :=
 
 /-! ## Test Suite -/
 
-def rustDecompileSuiteIO : List TestSeq := [
+public def rustDecompileSuiteIO : List TestSeq := [
   testRustDecompile,
 ]
 
diff --git a/Tests/Ix/RustSerialize.lean b/Tests/Ix/RustSerialize.lean
index ff54d5ac..88c10d60 100644
--- a/Tests/Ix/RustSerialize.lean
+++ b/Tests/Ix/RustSerialize.lean
@@ -4,13 +4,14 @@
   by roundtripping through Rust and comparing with the Lean serializer.
 -/
 
-import Ix.Ixon
-import Ix.Common
-import Ix.Meta
-import Ix.CompileM
-import Lean
-import LSpec
-import Tests.Ix.Fixtures
+module
+public import Ix.Ixon
+public import Ix.Common
+public import Ix.Meta
+public import Ix.CompileM
+public import Lean
+public import LSpec
+public import Tests.Ix.Fixtures
 
 open LSpec
 
@@ -92,7 +93,7 @@ def testRustSerdeRoundtrip : TestSeq :=
 
 /-! ## Test Suite -/
 
-def rustSerializeSuiteIO : List TestSeq := [
+public def rustSerializeSuiteIO : List TestSeq := [
   testRustSerdeRoundtrip,
 ]
 
diff --git a/Tests/Ix/Sharing.lean b/Tests/Ix/Sharing.lean
index 3ae1c9c5..f43620ba 100644
--- a/Tests/Ix/Sharing.lean
+++ b/Tests/Ix/Sharing.lean
@@ -5,13 +5,16 @@
   for cross-implementation compatibility.
 -/
 
-import Ix.Sharing
-import Ix.Ixon
-import Ix.CompileM
-import Ix.CanonM
-import Ix.Meta
-import Ix.Environment
-import LSpec
+module
+public import Ix.Sharing
+public import Ix.Ixon
+public import Ix.CompileM
+public import Ix.CanonM
+public import Ix.Meta
+public import Ix.Environment
+public import LSpec
+
+public section
 
 open LSpec Ix.Sharing Ixon Ix.CompileM Ix
 
@@ -647,7 +650,7 @@ def testFlipSharing : TestSeq := Id.run do
 
 /-! ## Suite -/
 
-def suite : List TestSeq := [
+public def suite : List TestSeq := [
   testForallImpReal,
   testForallImpSharing,
   testUint64ToBytesLength,
diff --git a/Tests/Keccak.lean b/Tests/Keccak.lean
index 50b39ed3..98d614ef 100644
--- a/Tests/Keccak.lean
+++ b/Tests/Keccak.lean
@@ -1,6 +1,8 @@
-import Ix.Keccak
-import LSpec
-import Ix.ByteArray
+module
+
+public import Ix.Keccak
+public import LSpec
+public import Ix.ByteArray
 
 open LSpec
 
@@ -9,7 +11,7 @@ abbrev expectedOutput : ByteArray := ⟨#[
   188, 54, 120, 158, 122, 30, 40, 20, 54, 70, 66, 41, 130, 143, 129, 125, 102, 18, 247, 180, 119, 214, 101, 145, 255, 150, 169, 224, 100, 188, 201, 138
 ]⟩
 
-def Tests.Keccak.suite : List LSpec.TestSeq :=
+public def Tests.Keccak.suite : List LSpec.TestSeq :=
 [
   test "Keccak256 hash" (expectedOutput == Keccak.hash input),
 ]
diff --git a/Tests/ShardMap.lean b/Tests/ShardMap.lean
index e5815a13..192a220b 100644
--- a/Tests/ShardMap.lean
+++ b/Tests/ShardMap.lean
@@ -1,5 +1,7 @@
-import Ix.ShardMap
-import LSpec
+module
+
+public import Ix.ShardMap
+public import LSpec
 
 open LSpec Ix
 
@@ -393,7 +395,7 @@ def testConcurrentTryGet : TestSeq :=
     -- (conservative threshold to avoid flakiness)
     pure (successes > 100, 0, 0, none)) .done
 
-def suite : List TestSeq := [
+public def suite : List TestSeq := [
   testInsertAndGet,
   testGetNonExistent,
   testMultipleInserts,
diff --git a/flake.lock b/flake.lock
index e3bb31df..44a265c5 100644
--- a/flake.lock
+++ b/flake.lock
@@ -31,11 +31,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1771879986,
-        "narHash": "sha256-YNIdmaUARBAOuST6/s5HDjNI6Q50C3kZWDHsSm6lal0=",
+        "lastModified": 1772039537,
+        "narHash": "sha256-HOSEL2CCo1A8HACVJ2P3DILGxO3OxLiHnGbWLGaH9bM=",
         "owner": "argumentcomputer",
         "repo": "Blake3.lean",
-        "rev": "810365c0e34a3f72c9ca33bf9b2bd8270986342a",
+        "rev": "564e0ab364ebaa3b1153defe2f49c9fe58a2d77c",
         "type": "github"
       },
       "original": {
diff --git a/lake-manifest.json b/lake-manifest.json
index f48cb863..fcd9c3a4 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,20 +25,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "810365c0e34a3f72c9ca33bf9b2bd8270986342a",
+   "rev": "564e0ab364ebaa3b1153defe2f49c9fe58a2d77c",
    "name": "Blake3",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "810365c0e34a3f72c9ca33bf9b2bd8270986342a",
+   "inputRev": "564e0ab364ebaa3b1153defe2f49c9fe58a2d77c",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/argumentcomputer/LSpec",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b76de469ebd3ae7a6ba494a36d34f713763623a6",
+   "rev": "41c8a9b2f08679212e075ff89fa33694a2536d64",
    "name": "LSpec",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "b76de469ebd3ae7a6ba494a36d34f713763623a6",
+   "inputRev": "41c8a9b2f08679212e075ff89fa33694a2536d64",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "ix",
diff --git a/lakefile.lean b/lakefile.lean
index 29151908..f6d1fc85 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -12,10 +12,10 @@ lean_exe ix where
   supportInterpreter := true
 
 require LSpec from git
-  "https://github.com/argumentcomputer/LSpec" @ "b76de469ebd3ae7a6ba494a36d34f713763623a6"
+  "https://github.com/argumentcomputer/LSpec" @ "41c8a9b2f08679212e075ff89fa33694a2536d64"
 
 require Blake3 from git
-  "https://github.com/argumentcomputer/Blake3.lean" @ "810365c0e34a3f72c9ca33bf9b2bd8270986342a"
+  "https://github.com/argumentcomputer/Blake3.lean" @ "564e0ab364ebaa3b1153defe2f49c9fe58a2d77c"
 
 require Cli from git
   "https://github.com/leanprover/lean4-cli" @ "v4.28.0"