diff --git a/README.md b/README.md
index ddb685e14..ccdb77eb9 100644
--- a/README.md
+++ b/README.md
@@ -39,6 +39,12 @@ lake build && lake test
 
 Unit tests are run with `#guard_msgs` commands. No output means the tests passed.
 
+To build executable files only and omit proof checks that might take a long time, use
+
+```bash
+lake build strata:exe StrataVerify StrataToCBMC StrataCoreToGoto
+```
+
 ## Running Analyses on Existing Strata Programs
 
 Strata programs use the `.st` file extension, preceded by the dialect name,
diff --git a/Strata.lean b/Strata.lean
index 4115531d8..56c0feb94 100644
--- a/Strata.lean
+++ b/Strata.lean
@@ -5,6 +5,7 @@
 -/
 
 -- This module serves as the root of the `Strata` library.
+-- In each category, imports are sorted by alphabetical order.
 
 /- DDM -/
 import Strata.DDM.Integration.Lean
@@ -19,8 +20,13 @@ import Strata.DL.Imperative.Imperative
 import Strata.Util.Sarif
 
 /- Strata Core -/
+import Strata.Languages.Core.FactoryWF
 import Strata.Languages.Core.StatementSemantics
 import Strata.Languages.Core.SarifOutput
 
+/- Code Transforms -/
+import Strata.Transform.CallElimCorrect
+import Strata.Transform.DetToNondetCorrect
+
 /- Backends -/
 import Strata.Backends.CBMC.CProver
diff --git a/StrataTest/Languages/Core/FactoryWF.lean b/Strata/Languages/Core/FactoryWF.lean
similarity index 100%
rename from StrataTest/Languages/Core/FactoryWF.lean
rename to Strata/Languages/Core/FactoryWF.lean
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 81cdc79a3..261d712ca 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -5,7 +5,7 @@
 -/
 
 -- Minimal Laurel dialect for AssertFalse example
-import Strata
+import Strata.DDM.Integration.Lean
 
 namespace Strata
 namespace Laurel
diff --git a/StrataTest/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean
similarity index 100%
rename from StrataTest/Transform/CallElimCorrect.lean
rename to Strata/Transform/CallElimCorrect.lean
diff --git a/StrataTest/Transform/DetToNondetCorrect.lean b/Strata/Transform/DetToNondetCorrect.lean
similarity index 100%
rename from StrataTest/Transform/DetToNondetCorrect.lean
rename to Strata/Transform/DetToNondetCorrect.lean