metabuilder/spec/KNOWN_ISSUES.md

Known Issues

metabuilder.tla

Issue: Syntax error at line 323 in the PackageConsistency invariant.

Error:

line 323, col 47 to line 323, col 47 of module metabuilder
Unknown operator: `t'.

Root Cause: The quantification over installedPackages[t] assumes the function is defined for all tenants, but TLA+ requires explicit guarding.

Status: Pre-existing issue in the original specification. Not introduced by new specifications.

Workaround: The issue is in the core specification and should be addressed separately. The new future functionality specifications (workflow_system.tla, collaboration.tla, integrations.tla) all pass validation successfully.

Suggested Fix:

\* Current (line 322-324)
PackageConsistency ==
    \A t \in Tenants, p \in installedPackages[t]:
        packageStates[p] \in {"installed", "disabled", "installing"}

\* Suggested fix
PackageConsistency ==
    \A t \in Tenants:
        \A p \in installedPackages[t]:
            packageStates[p] \in {"installed", "disabled", "installing"}

Future Functionality Specifications

All new specifications pass validation:

• ✓ workflow_system.tla: PASSED
• ✓ collaboration.tla: PASSED
• ✓ integrations.tla: PASSED

---

Last Updated: 2025-12-27