diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -34,7 +34,7 @@
 
 ```bash
 cabal update
-cabal install --overwrite-policy=always phino-0.0.0.68
+cabal install --overwrite-policy=always phino-0.0.0.69
 phino --version
 ```
 
@@ -385,55 +385,55 @@
 === parse/phi ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      1431411.012 μs
-  avg:        143141.101 μs
-  min:        127073.145 μs
-  max:        171130.864 μs
-  std dev:    15649.917 μs
+  total:      1448938.560 μs
+  avg:        144893.856 μs
+  min:        129456.053 μs
+  max:        178640.839 μs
+  std dev:    16904.402 μs
 === parse/xmir ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      7598416.608 μs
-  avg:        759841.661 μs
-  min:        697811.420 μs
-  max:        822708.096 μs
-  std dev:    41396.013 μs
+  total:      7588032.720 μs
+  avg:        758803.272 μs
+  min:        700986.244 μs
+  max:        821408.758 μs
+  std dev:    37918.602 μs
 === rewrite/normalize ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      364316.104 μs
-  avg:        36431.610 μs
-  min:        35585.946 μs
-  max:        38039.285 μs
-  std dev:    724.383 μs
+  total:      388634.740 μs
+  avg:        38863.474 μs
+  min:        36132.373 μs
+  max:        42039.094 μs
+  std dev:    1775.255 μs
 === print/sweet/multiline ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      3936466.911 μs
-  avg:        393646.691 μs
-  min:        388074.584 μs
-  max:        398140.650 μs
-  std dev:    3449.956 μs
+  total:      4021506.769 μs
+  avg:        402150.677 μs
+  min:        396372.506 μs
+  max:        409920.442 μs
+  std dev:    5075.454 μs
 === print/sweet/flat ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      3778721.383 μs
-  avg:        377872.138 μs
-  min:        355092.443 μs
-  max:        394891.090 μs
-  std dev:    13649.562 μs
+  total:      3909169.505 μs
+  avg:        390916.950 μs
+  min:        359212.755 μs
+  max:        408481.102 μs
+  std dev:    17796.878 μs
 === print/salty/multiline ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      13588867.661 μs
-  avg:        1358886.766 μs
-  min:        1332657.250 μs
-  max:        1380376.704 μs
-  std dev:    13948.257 μs
+  total:      13573961.600 μs
+  avg:        1357396.160 μs
+  min:        1334521.176 μs
+  max:        1370074.545 μs
+  std dev:    12356.510 μs
 ```
 
 The results were calculated in [this GHA job][benchmark-gha]
-on 2026-05-18 at 22:53,
+on 2026-05-21 at 11:38,
 on Linux with 4 CPUs.
 
 <!-- benchmark_end -->
@@ -469,4 +469,4 @@
 [jna]: https://github.com/java-native-access/jna
 [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java
 [jeo]: https://github.com/objectionary/jeo-maven-plugin
-[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/26064953685
+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/26223356318
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.0.69
+version: 0.0.0.70
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
@@ -78,7 +78,7 @@
     Paths_phino
 
   build-depends:
-    aeson >=2.2.3 && <2.3,
+    aeson >=2.2.3 && <2.4,
     array >=0.5.4 && <0.6,
     base >=4.18.3.0 && <5,
     binary-ieee754 >=0.1.0 && <0.2,
@@ -152,7 +152,7 @@
     ImportQualifiedPost
 
   build-depends:
-    aeson >=2.2.3 && <2.3,
+    aeson >=2.2.3 && <2.4,
     base >=4.18.3.0 && <5,
     bytestring >=0.11.4 && <0.13,
     containers >=0.6.5 && <0.9,
diff --git a/src/Misc.hs b/src/Misc.hs
--- a/src/Misc.hs
+++ b/src/Misc.hs
@@ -16,6 +16,7 @@
   , btsToStr
   , btsToNum
   , withVoidRho
+  , recoverFormations
   , allPathsIn
   , ensuredFile
   , shuffle
@@ -198,6 +199,19 @@
         BiVoid AtRho -> bd : withVoidRho' rest True
         BiTau AtRho _ -> bd : withVoidRho' rest True
         _ -> bd : withVoidRho' rest hasRho
+
+-- Recursively ensure all formations have a BiVoid AtRho binding (ρ ↦ ∅).
+-- Fixes in-memory ExFormation [] to ExFormation [BiVoid AtRho] after rewriting,
+-- keeping the invariant that the parser enforces via withVoidRho.
+recoverFormations :: Expression -> Expression
+recoverFormations (ExFormation bindings) = ExFormation (withVoidRho (map recoverFormations' bindings))
+recoverFormations (ExDispatch expr attr) = ExDispatch (recoverFormations expr) attr
+recoverFormations (ExApplication expr binding) = ExApplication (recoverFormations expr) (recoverFormations' binding)
+recoverFormations expr = expr
+
+recoverFormations' :: Binding -> Binding
+recoverFormations' (BiTau attr expr) = BiTau attr (recoverFormations expr)
+recoverFormations' binding = binding
 
 -- Transform dispatch to list of attributes
 -- >>> fqnToAttrs (ExDispatch (ExDispatch (ExDispatch ExGlobal (AtLabel "org")) (AtLabel "eolang")) (AtLabel "number"))
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -20,6 +20,7 @@
 import Locator (locatedExpression, withLocatedExpression)
 import Logger (logDebug)
 import Matcher (Subst)
+import Misc (recoverFormations)
 import Must (Must (..), exceedsUpperBound, inRange)
 import Printer (printExpression)
 import Replacer (ReplaceContext (ReplaceCtx), ReplaceExpressionFunc, replaceExpression, replaceExpressionFast)
@@ -167,7 +168,7 @@
                     else pure (_rewrittens, _unique, False)
                 matched -> do
                   logDebug (printf "Rule '%s' has been matched, applying..." ruleName)
-                  expr <- tryBuildAndReplaceFast (expression, ptn, res, matched) (ReplaceCtx _maxDepth)
+                  expr <- recoverFormations <$> tryBuildAndReplaceFast (expression, ptn, res, matched) (ReplaceCtx _maxDepth)
                   if expression == expr
                     then do
                       logDebug (printf "Applied '%s', no changes made" ruleName)