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.70
+cabal install --overwrite-policy=always phino-0.0.0.71
 phino --version
 ```
 
@@ -392,55 +392,55 @@
 === parse/phi ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      1283128.483 μs
-  avg:        128312.848 μs
-  min:        117090.148 μs
-  max:        159904.869 μs
-  std dev:    16799.275 μs
+  total:      1419098.230 μs
+  avg:        141909.823 μs
+  min:        127594.959 μs
+  max:        173890.065 μs
+  std dev:    17203.851 μs
 === parse/xmir ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      7638674.160 μs
-  avg:        763867.416 μs
-  min:        696616.654 μs
-  max:        834131.587 μs
-  std dev:    46054.709 μs
+  total:      7668285.122 μs
+  avg:        766828.512 μs
+  min:        701875.873 μs
+  max:        834845.017 μs
+  std dev:    47941.411 μs
 === rewrite/normalize ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      410101.450 μs
-  avg:        41010.145 μs
-  min:        37322.375 μs
-  max:        46790.558 μs
-  std dev:    3315.786 μs
+  total:      419697.477 μs
+  avg:        41969.748 μs
+  min:        39760.750 μs
+  max:        44430.602 μs
+  std dev:    1609.092 μs
 === print/sweet/multiline ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      4536347.235 μs
-  avg:        453634.724 μs
-  min:        436266.864 μs
-  max:        484874.805 μs
-  std dev:    14385.579 μs
+  total:      4102201.200 μs
+  avg:        410220.120 μs
+  min:        392265.453 μs
+  max:        432892.821 μs
+  std dev:    12013.486 μs
 === print/sweet/flat ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      4391468.284 μs
-  avg:        439146.828 μs
-  min:        421949.972 μs
-  max:        461548.132 μs
-  std dev:    12926.007 μs
+  total:      3992227.126 μs
+  avg:        399222.713 μs
+  min:        381853.621 μs
+  max:        416304.939 μs
+  std dev:    11016.036 μs
 === print/salty/multiline ===
   warmup:     3 iterations
   batches:    10 x 1
-  total:      13872760.194 μs
-  avg:        1387276.019 μs
-  min:        1347848.058 μs
-  max:        1435996.600 μs
-  std dev:    28902.131 μs
+  total:      13721988.418 μs
+  avg:        1372198.842 μs
+  min:        1332480.796 μs
+  max:        1420431.251 μs
+  std dev:    28529.557 μs
 ```
 
 The results were calculated in [this GHA job][benchmark-gha]
-on 2026-05-24 at 14:39,
+on 2026-06-01 at 19:59,
 on Linux with 4 CPUs.
 
 <!-- benchmark_end -->
@@ -476,4 +476,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/26364073830
+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/26778383106
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.71
+version: 0.0.0.72
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
@@ -67,6 +67,7 @@
     Rewriter
     Rule
     Sugar
+    Tau
     XMIR
     Yaml
 
@@ -142,6 +143,7 @@
     RewriterSpec
     RuleSpec
     Spec
+    TauSpec
     XMIRSpec
     YamlSpec
 
diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs
--- a/src/CLI/Runners.hs
+++ b/src/CLI/Runners.hs
@@ -31,6 +31,7 @@
 import Rule (RuleContext (..), matchProgramWithRule)
 import System.Directory (doesFileExist, getModificationTime)
 import System.Exit (exitSuccess)
+import Tau (seedTaus)
 import Text.Printf (printf)
 import XMIR
 import qualified Yaml as Y
@@ -47,6 +48,7 @@
   validateBreakpoint _breakpoint rules
   input <- readInput _inputFile
   program <- parseProgram input _inputFormat
+  seedTaus program
   logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)
   let listing = case (rules, _inputFormat, _outputFormat) of
         ([], XMIR, XMIR) -> (\_ -> escapeXML input)
@@ -139,6 +141,7 @@
   [foc] <- validatedDispatches "focus" [_focus]
   input <- readInput _inputFile
   prog <- parseProgram input _inputFormat
+  seedTaus prog
   let printCtx = printProgCtx foc
       canonize = if _canonize then C.canonize else id
       exclude = (`F.exclude` excluded)
@@ -223,6 +226,7 @@
 runMatch OptsMatch{..} = do
   input <- readInput _inputFile
   prog <- parseProgram input PHI
+  seedTaus prog
   if isNothing _pattern
     then logDebug "The --pattern is not provided, no substitutions are built"
     else do
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -25,7 +25,7 @@
 import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)
 import Rule (RuleContext (RuleContext), isNF)
 import Text.Printf (printf)
-import Yaml (ExtraArgument (ArgAttribute), normalizationRules)
+import Yaml (normalizationRules)
 
 type Dataized = (Maybe Bytes, [Rewritten])
 
@@ -209,7 +209,7 @@
 -- which refers to expression we want to dataize.
 _dataize :: Expression -> DataizeContext -> IO (Maybe Bytes)
 _dataize expr ctx@DataizeContext{_buildTerm = buildTerm, _program = Program (ExFormation bds)} = do
-  (TeAttribute attr) <- buildTerm "random-tau" (map ArgAttribute (attributesFromBindings bds)) substEmpty
+  (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty
   let prog = Program (ExFormation (BiTau attr expr : bds))
   (bts, _) <- dataize' (expr, (prog, Nothing) :| []) ctx{_program = prog}
   pure bts
diff --git a/src/Functions.hs b/src/Functions.hs
--- a/src/Functions.hs
+++ b/src/Functions.hs
@@ -12,9 +12,7 @@
 import qualified Data.ByteString.Char8 as B
 import Data.Functor
 import qualified Data.Set as Set
-import qualified Data.Text as T
 import Deps
-import GHC.IO (unsafePerformIO)
 import Logger (logDebug)
 import Matcher
 import Misc
@@ -22,6 +20,7 @@
 import Printer (printAttribute, printBinding, printExpression, printExtraArg)
 import Random (randomString)
 import Regexp
+import Tau (freshTau)
 import Text.Printf (printf)
 import qualified Yaml as Y
 
@@ -74,29 +73,13 @@
   pure (TeExpression scope)
 _scope _ _ = throwIO (userError "Function scope() requires exactly 1 argument as expression")
 
+-- Uniqueness is the engine's job: 'freshTau' draws from the document-wide
+-- avoid-set seeded at the start of the run, so no collision list is needed.
+-- The function takes no arguments and rejects any extras so rule mistakes are
+-- not silently accepted.
 _randomTau :: BuildTermMethod
-_randomTau args subst = do
-  attrs <- argsToAttrs args
-  tau <- randomTau attrs
-  pure (TeAttribute (AtLabel (T.pack tau)))
-  where
-    argsToAttrs :: [Y.ExtraArgument] -> IO [String]
-    argsToAttrs [] = pure []
-    argsToAttrs (arg : rest) = case arg of
-      Y.ArgExpression _ -> argsToAttrs rest
-      Y.ArgAttribute attr -> do
-        attr' <- buildAttributeThrows attr subst
-        rest' <- argsToAttrs rest
-        pure (printAttribute attr' : rest')
-      Y.ArgBinding bd -> do
-        bds <- buildBindingThrows bd subst
-        rest' <- argsToAttrs rest
-        pure (map show (attributesFromBindings bds) ++ rest')
-      Y.ArgBytes _ -> throwIO (userError "Bytes can't be argument of random-tau() function")
-    randomTau :: [String] -> IO String
-    randomTau attrs = do
-      tau <- randomString "a🌵%d"
-      if tau `elem` attrs then randomTau attrs else pure tau
+_randomTau [] _ = TeAttribute . AtLabel <$> freshTau
+_randomTau _ _ = throwIO (userError "Function random-tau() requires exactly 0 arguments")
 
 _dataize :: BuildTermMethod
 _dataize [Y.ArgBytes bytes] subst = do
@@ -218,7 +201,7 @@
 _join [] _ = pure (TeBindings [])
 _join args subst = do
   bds <- buildBindings args
-  pure (TeBindings (join' bds Set.empty))
+  TeBindings <$> join' bds Set.empty
   where
     buildBindings :: [Y.ExtraArgument] -> IO [Binding]
     buildBindings [] = pure []
@@ -227,8 +210,8 @@
       next <- buildBindings args'
       pure (bds ++ next)
     buildBindings _ = throwIO (userError "Function 'join' can work with bindings only")
-    join' :: [Binding] -> Set.Set Attribute -> [Binding]
-    join' [] _ = []
+    join' :: [Binding] -> Set.Set Attribute -> IO [Binding]
+    join' [] _ = pure []
     join' (bd : bds) attrs =
       case attributesFromBindings [bd] of
         [attr] ->
@@ -236,19 +219,20 @@
             then
               if attr == AtRho || attr == AtDelta || attr == AtLambda
                 then join' bds attrs
-                else
-                  let new = case bd of
-                        BiTau at ex -> BiTau (updated at attrs) ex
-                        BiVoid at -> BiVoid (updated at attrs)
-                        other -> other
-                   in new : join' bds attrs
-            else bd : join' bds (Set.insert attr attrs)
-        _ -> bd : join' bds attrs
-    updated :: Attribute -> Set.Set Attribute -> Attribute
-    updated _ attrs =
-      case unsafePerformIO (_randomTau (map Y.ArgAttribute (Set.toList attrs)) subst) of
-        TeAttribute attr' -> attr'
-        _ -> AtLabel "unknown"
+                else do
+                  new <- case bd of
+                    BiTau _ ex -> (`BiTau` ex) <$> freshAttr
+                    BiVoid _ -> BiVoid <$> freshAttr
+                    other -> pure other
+                  (new :) <$> join' bds attrs
+            else (bd :) <$> join' bds (Set.insert attr attrs)
+        _ -> (bd :) <$> join' bds attrs
+    freshAttr :: IO Attribute
+    freshAttr = do
+      term <- _randomTau [] subst
+      case term of
+        TeAttribute attr' -> pure attr'
+        _ -> throwIO (userError "random-tau() did not return an attribute, internal invariant violated")
 
 _splice :: BuildTermMethod
 _splice = _spliceLike "splice" True
@@ -262,8 +246,7 @@
   repBds <- buildBindingThrows repArg subst
   mapM_ validateRep repBds
   (sentinel, _) <- buildExpressionThrows sentExpr subst
-  let avoid = map Y.ArgAttribute (attributesFromBindings (inBds ++ repBds))
-  result <- walk inBds sentinel repBds avoid
+  result <- walk inBds sentinel repBds
   pure (TeBindings result)
   where
     validateRep :: Binding -> IO ()
@@ -278,15 +261,15 @@
                 (printBinding bd)
             )
         )
-    walk :: [Binding] -> Expression -> [Binding] -> [Y.ExtraArgument] -> IO [Binding]
-    walk [] _ _ _ = pure []
-    walk (bd : rest) sent rep avoid
+    walk :: [Binding] -> Expression -> [Binding] -> IO [Binding]
+    walk [] _ _ = pure []
+    walk (bd : rest) sent rep
       | matches sent bd = do
-          fresh <- traverse (renamed avoid) rep
-          tail' <- walk rest sent rep avoid
+          fresh <- traverse renamed rep
+          tail' <- walk rest sent rep
           pure (fresh ++ (if keepMarker then bd : tail' else tail'))
       | otherwise = do
-          tail' <- walk rest sent rep avoid
+          tail' <- walk rest sent rep
           pure (bd : tail')
     matches :: Expression -> Binding -> Bool
     matches sent (BiTau _ (ExFormation bds)) = any (isPhi sent) bds
@@ -294,18 +277,18 @@
     isPhi :: Expression -> Binding -> Bool
     isPhi sent (BiTau AtPhi expr) = expr == sent
     isPhi _ _ = False
-    renamed :: [Y.ExtraArgument] -> Binding -> IO Binding
-    renamed avoid (BiTau (AtLabel _) expr) = do
-      term <- _randomTau avoid subst
+    renamed :: Binding -> IO Binding
+    renamed (BiTau (AtLabel _) expr) = do
+      term <- _randomTau [] subst
       case term of
         TeAttribute attr -> pure (BiTau attr expr)
         _ -> throwIO (userError (printf "Failed to generate fresh tau attribute for %s" name))
-    renamed avoid (BiVoid (AtLabel _)) = do
-      term <- _randomTau avoid subst
+    renamed (BiVoid (AtLabel _)) = do
+      term <- _randomTau [] subst
       case term of
         TeAttribute attr -> pure (BiVoid attr)
         _ -> throwIO (userError (printf "Failed to generate fresh tau attribute for %s" name))
-    renamed _ bd = pure bd
+    renamed bd = pure bd
 _spliceLike name _ _ _ =
   throwIO (userError (printf "Function %s() requires exactly 3 arguments: input bindings, sentinel expression, replacement bindings" name))
 
diff --git a/src/Tau.hs b/src/Tau.hs
new file mode 100644
--- /dev/null
+++ b/src/Tau.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+-- Uniqueness of generated 𝜏-labels is the engine's job, not the caller's.
+-- Instead of asking every 'random-tau' call site to hand over the names it
+-- must steer clear of, we scan the document once at the start of a run and
+-- remember every attribute label it already uses. Each minted name is added
+-- back to that set so later firings (the fixpoint loop re-applies rules across
+-- cycles) never reuse one. A monotonic cursor advances past taken indices so
+-- minting never rescans the document. Names are sequential rather than
+-- random, which makes the rewritten output deterministic.
+module Tau (seedTaus, freshTau) where
+
+import AST
+import Data.IORef (IORef, atomicModifyIORef', newIORef, writeIORef)
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Text (Text)
+import qualified Data.Text as T
+import GHC.IO (unsafePerformIO)
+
+-- The set of attribute labels already taken in the document being rewritten,
+-- paired with a monotonic cursor pointing at the next candidate index.
+taus :: IORef (Set Text, Int)
+{-# NOINLINE taus #-}
+taus = unsafePerformIO (newIORef (Set.empty, 0))
+
+-- Scan the program once and seed the avoid-set with every attribute label it
+-- contains, resetting the cursor back to the start.
+seedTaus :: Program -> IO ()
+seedTaus (Program expr) = writeIORef taus (exprLabels expr, 0)
+
+-- Mint a fresh, deterministic 𝜏-label that collides with no taken name,
+-- advancing the cursor past taken indices and recording the new name so it is
+-- never handed out again. Atomic so concurrent callers cannot mint duplicates
+-- or lose updates.
+freshTau :: IO Text
+freshTau = atomicModifyIORef' taus advance
+  where
+    advance (taken, cursor) =
+      let (minted, idx) = mint taken cursor
+       in ((Set.insert minted taken, idx + 1), minted)
+
+-- Find the first index at or after the cursor whose name is still free.
+mint :: Set Text -> Int -> (Text, Int)
+mint taken idx
+  | name `Set.member` taken = mint taken (idx + 1)
+  | otherwise = (name, idx)
+  where
+    name = "a🌵" <> T.pack (show idx)
+
+exprLabels :: Expression -> Set Text
+exprLabels (ExFormation bds) = Set.unions (map bindingLabels bds)
+exprLabels (ExApplication expr bd) = exprLabels expr <> bindingLabels bd
+exprLabels (ExDispatch expr attr) = exprLabels expr <> attrLabel attr
+exprLabels (ExMetaTail expr _) = exprLabels expr
+exprLabels (ExPhiMeet _ _ expr) = exprLabels expr
+exprLabels (ExPhiAgain _ _ expr) = exprLabels expr
+exprLabels _ = Set.empty
+
+bindingLabels :: Binding -> Set Text
+bindingLabels (BiTau attr expr) = attrLabel attr <> exprLabels expr
+bindingLabels (BiVoid attr) = attrLabel attr
+bindingLabels _ = Set.empty
+
+attrLabel :: Attribute -> Set Text
+attrLabel (AtLabel label) = Set.singleton label
+attrLabel _ = Set.empty
diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs
--- a/test/RewriterSpec.hs
+++ b/test/RewriterSpec.hs
@@ -23,6 +23,7 @@
 import Printer (printProgram)
 import Rewriter (RewriteContext (RewriteContext), rewrite)
 import System.FilePath (makeRelative, replaceExtension, (</>))
+import Tau (seedTaus)
 import Test.Hspec (Spec, describe, expectationFailure, it, pending, runIO)
 import Yaml (normalizationRules)
 import Yaml qualified as Y
@@ -84,6 +85,7 @@
             Just True -> pending
             _ -> do
               prog <- parseProgramThrows (input pack)
+              seedTaus prog
               rules' <- case rules pack of
                 Just _rules -> case custom _rules of
                   Just custom' -> pure custom'
diff --git a/test/TauSpec.hs b/test/TauSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/TauSpec.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+-- SPDX-License-Identifier: MIT
+
+module TauSpec where
+
+import AST
+import Control.Monad (replicateM)
+import Tau (freshTau, seedTaus)
+import Test.Hspec (Spec, describe, it, shouldBe)
+
+spec :: Spec
+spec = describe "Tau" $ do
+  it "mints sequential names after seeding from an empty document" $ do
+    seedTaus (Program (ExFormation []))
+    names <- replicateM 3 freshTau
+    names `shouldBe` ["a🌵0", "a🌵1", "a🌵2"]
+  it "resets the cursor on every seeding so output is deterministic" $ do
+    seedTaus (Program (ExFormation []))
+    first <- freshTau
+    seedTaus (Program (ExFormation []))
+    second <- freshTau
+    (first, second) `shouldBe` ("a🌵0", "a🌵0")
+  it "skips names already taken in the document" $ do
+    seedTaus
+      ( Program
+          ( ExFormation
+              [ BiTau (AtLabel "a🌵0") ExGlobal
+              , BiTau (AtLabel "a🌵2") ExGlobal
+              ]
+          )
+      )
+    names <- replicateM 2 freshTau
+    names `shouldBe` ["a🌵1", "a🌵3"]