From 919f8f294801c361f218afb604e1be5bca66b91e Mon Sep 17 00:00:00 2001
From: johndoe6345789 <john.doe6345789@gmail.com>
Date: Sat, 27 Dec 2025 15:27:21 +0000
Subject: [PATCH] fix: guard package consistency quantifier

---
 spec/metabuilder.tla | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/spec/metabuilder.tla b/spec/metabuilder.tla
index 8d7726a5d..045cce7d8 100644
--- a/spec/metabuilder.tla
+++ b/spec/metabuilder.tla
@@ -320,8 +320,9 @@ DataConsistency ==
 
 \* Package consistency: installed packages must be in installed or disabled state
 PackageConsistency ==
-    \A t \in Tenants, p \in installedPackages[t]:
-        packageStates[p] \in {"installed", "disabled", "installing"}
+    \A t \in Tenants:
+        \A p \in installedPackages[t]:
+            packageStates[p] \in {"installed", "disabled", "installing"}
 
 \* DBAL safety: no queries processed in error state
 DBALSafety ==