This directory contains the formal TLA+ specification for the MetaBuilder system, a data-driven, multi-tenant platform with hierarchical permissions and declarative components.

Overview

The specification models both current and future MetaBuilder functionality through multiple TLA+ modules:

Core System Specifications:

6-Level Permission System: Hierarchical access control (Public → User → Moderator → Admin → God → Supergod)
Multi-Tenant Data Isolation: Strict separation of data between tenants
Database Abstraction Layer (DBAL): Query processing with security guarantees
Package Management: Installation, enabling, and disabling of feature packages
Audit Logging: Complete tracking of privileged operations

Future Functionality Specifications:

Workflow System: Workflow execution, scheduling, and state management
Real-Time Collaboration: Concurrent editing, presence, comments, and mentions
Integration Ecosystem: Webhooks, OAuth apps, API keys, and rate limiting

Files

Core System: `metabuilder.tla`

The main TLA+ specification file that defines:

State Variables: System state including users, permissions, tenants, packages, and DBAL
Permission Model: Hierarchical levels with inheritance
Operations: Data access, user management, package operations, DBAL transitions
Safety Properties: Invariants that must always hold
- TenantIsolation: Users can only access data in their tenant
- PermissionEnforcement: Operations require appropriate permission levels
- DataConsistency: No data overlap between tenants
- PackageConsistency: Installed packages are in valid states
- DBALSafety: No dangerous operations in error state
- AuditCompleteness: All privileged operations are logged
Liveness Properties: Things that eventually happen
- EventualProcessing: Queries eventually complete
- EventualRecovery: DBAL recovers from errors
- EventualPackageInstall: Package installations complete

`metabuilder.cfg`

Configuration file for the TLC model checker that specifies:

Constants for model checking (users, tenants, packages, records)
Invariants to check
Temporal properties to verify
State space constraints for bounded model checking

Schema-Driven Package System: `package_system.tla`

NEW - Detailed specification for the overhauled package system, aligned with schemas/package-schemas/:

Multi-Source Package Loading: Local, remote, and git package sources with priority-based resolution
Schema Validation: Validates packages against 16+ JSON schemas (metadata, entities, components, scripts, types, etc.)
Dependency Resolution: Transitive dependency tracking with version constraints
Conflict Resolution: Strategies for same package in multiple sources (priority, latest-version, local-first, remote-first)
Permission Integration: Package minLevel enforced against 6-level permission system
Safety Properties:
- AdminOnlyPackageManagement: Only Level 4+ users can install/enable/disable packages
- SupergodOnlySourceManagement: Only Level 6 can manage package sources
- EnabledImpliesInstalled: Enabled packages must be installed
- DependencyIntegrity: Enabled packages have all dependencies enabled
- NoCyclicDependencies: No circular dependency chains
- SchemaValidationRequired: Packages must pass schema validation before install
- PermissionLevelEnforcement: Package minLevel respected
- ConflictsResolvedBeforeInstall: Multi-source conflicts resolved before installation
- PackageAuditCompleteness: All package operations are logged
Liveness Properties:
- EventualOperationCompletion: Pending operations eventually complete or fail
- EventualValidation: Schema validations eventually complete
- EventualConflictResolution: Conflicts are eventually resolved
- EventualIndexRefresh: Source indexes eventually refresh after fetch

`package_system.cfg`

Configuration for package system model checking with sample packages, sources, and schema types from the actual codebase.

Future Functionality: `workflow_system.tla`

Specification for advanced workflow execution features:

Template Management: God-level users create and manage workflow templates
Workflow Execution: Admin-level users trigger manual or scheduled workflows
Step Dependencies: Define and enforce execution order constraints
Error Handling: Automatic retry logic with configurable limits
Concurrency Control: Limit concurrent workflow executions per tenant
Safety Properties:
- GodOnlyTemplateCreation: Only Level 5+ users can author workflows
- AdminOnlyExecution: Only Level 4+ users can execute workflows
- TenantIsolation: Workflows are strictly isolated by tenant
- ConcurrencyLimit: Per-tenant concurrent execution limits
- RetryLimit: Failed steps don't exceed retry threshold
- DependencyEnforcement: Steps execute only after dependencies complete
Liveness Properties:
- EventualStepExecution: Pending steps eventually execute
- EventualCompletion: Running workflows eventually complete or fail
- EventualScheduleTrigger: Scheduled workflows eventually trigger

`workflow_system.cfg`

Configuration for workflow system model checking with workflow templates, steps, and execution limits.

Future Functionality: `collaboration.tla`

Specification for real-time collaboration features:

Session Management: User connection, idle, and disconnection states
Concurrent Editing: Multiple users editing documents simultaneously
Comments and Mentions: Users can comment and mention others in documents
Presence Tracking: Real-time user online/idle/offline status
Notifications: Mention notifications with read status tracking
Version History: Document snapshot creation and tracking
Safety Properties:
- DocumentTenantIsolation: Editors can only access documents in their tenant
- ConcurrentEditorLimit: Maximum concurrent editors per document
- CommentTenantConsistency: Comments belong to document's tenant
- MentionTenantIsolation: Mentions stay within tenant boundaries
- NotificationLimit: Pending notifications don't exceed limits
- DisconnectedNotEditing: Disconnected users automatically stop editing
- OperationAuthorship: All operations come from authorized editors
Liveness Properties:
- EventualNotificationHandling: Notifications eventually get read or cleared
- EventualMentionRead: Mentioned users eventually see their mentions
- EventualStopEditing: Active editors eventually stop or disconnect

`collaboration.cfg`

Configuration for collaboration model checking with documents, comments, and concurrent editors.

Future Functionality: `integrations.tla`

Specification for integration ecosystem:

Webhook Management: Create, configure, and manage webhooks for events
OAuth Applications: OAuth app lifecycle and token management
API Key Management: User-level API key creation and expiration
Event Subscriptions: Subscribe to and filter system events
Rate Limiting: Track and enforce API call rate limits per identity
Delivery Guarantees: Webhook delivery with retry logic
Safety Properties:
- AdminOnlyIntegrationManagement: Only Level 4+ users manage integrations
- WebhookTenantLimit: Webhooks per tenant don't exceed limits
- APIKeyUserLimit: API keys per user don't exceed limits
- RateLimitEnforcement: API calls respect rate limits
- WebhookTenantIsolation: Webhooks isolated by tenant
- OAuthAppTenantIsolation: OAuth apps isolated by tenant
- TokenTenantConsistency: OAuth tokens match app tenants
- ActiveDeliveriesQueued: Active deliveries are properly queued
Liveness Properties:
- EventualDeliveryCompletion: Webhook deliveries eventually complete or fail
- EventualRetryOrFail: Failed deliveries retry or permanently fail
- EventualExpiration: Expired API keys eventually marked as expired

`integrations.cfg`

Configuration for integration ecosystem model checking with webhooks, OAuth apps, and API keys.

Key Concepts

Permission Levels

The system enforces a strict hierarchy:

Level 1 (Public)    → Unauthenticated, read-only access
Level 2 (User)      → Authenticated users, can create/modify own content
Level 3 (Moderator) → Content moderation capabilities
Level 4 (Admin)     → User management, package installation, tenant administration
Level 5 (God)       → Advanced workflows, system scripting
Level 6 (Supergod)  → Complete system control

Higher levels inherit all permissions from lower levels.

Multi-Tenancy

Every user belongs to exactly one tenant, and:

Users can only access data within their tenant
All database queries are automatically filtered by tenantId
Tenant data is completely isolated from other tenants
Package installations are per-tenant

DBAL (Database Abstraction Layer)

The specification models the DBAL as a state machine with states:

ready: Ready to accept queries
processing: Actively executing a query
error: Encountered an error (can recover)

The DBAL enforces:

Permission checks before query execution
Row-level security
Audit logging
Eventual consistency

Package System

Packages are self-contained feature modules managed through a schema-driven system:

Basic Operations (metabuilder.tla):

Installed by admins (Level 4+)
Enabled or disabled per-tenant
Tracked through state transitions: available → installing → installed ↔ disabled

Advanced Features (package_system.tla):

Multi-source loading: Local (packages/), remote registries, git repositories
Schema validation against 16+ JSON schemas in schemas/package-schemas/
Dependency resolution with version constraints (semver)
Conflict resolution when package exists in multiple sources
Permission-level filtering via minLevel property

Schema Alignment:

schemas/package-schemas/
├── metadata_schema.json    → Package identity, version, minLevel
├── entities_schema.json    → Database entities (Prisma-like)
├── components_schema.json  → UI component definitions
├── script_schema.json      → Script/JSON script logic
├── types_schema.json       → Type definitions
├── validation_schema.json  → Data validators
├── api_schema.json         → REST/GraphQL endpoints
├── events_schema.json      → Event-driven patterns
├── jobs_schema.json        → Background tasks
├── permissions_schema.json → RBAC/ABAC rules
├── forms_schema.json       → Dynamic form definitions
├── styles_schema.json      → Design tokens
├── migrations_schema.json  → Database migrations
├── assets_schema.json      → Static assets
├── storybook_schema.json   → Storybook config
└── index_schema.json       → Master registry validation

Package Structure:

packages/{name}/
├── package.json           # Metadata (validated against metadata_schema.json)
├── components/            # UI components
├── scripts/               # Script/JSON scripts
├── permissions/           # Permission definitions
├── static_content/        # Assets including icon.svg
├── styles/                # SCSS/design tokens
├── storybook/             # Storybook stories
└── tests/                 # Test suites

Using the Specification

Prerequisites

Install the TLA+ Toolbox or command-line tools:

TLA+ Toolbox (GUI)
TLA+ Tools (command-line)

Model Checking

With TLA+ Toolbox:
- Open the Toolbox
- Create a new specification and add metabuilder.tla
- Create a new model based on metabuilder.cfg
- Run the model checker (TLC)

With Command Line:

# Check syntax
java -cp tla2tools.jar tla2sast.SANY spec/metabuilder.tla

# Run model checker
java -cp tla2tools.jar tlc2.TLC spec/metabuilder.tla -config spec/metabuilder.cfg

Adjusting the Model

The constants in metabuilder.cfg can be adjusted to explore different scenarios:

CONSTANTS
    Users = {u1, u2, u3}      # Add more users
    Tenants = {t1, t2, t3}    # Add more tenants
    Packages = {p1, p2}       # Add more packages
    DataRecords = {r1, r2}    # Add more records
    MaxLevel = 6               # Fixed at 6 levels

Note: Larger constants will increase the state space exponentially. Use constraints to bound the search:

CONSTRAINT
    Len(auditLog) <= 10
    Cardinality(activeQueries) <= 5

Properties Verified

Safety (Invariants)

These properties must hold in every reachable state:

Type Safety: All variables have correct types
Tenant Isolation: Cross-tenant access is impossible
Permission Enforcement: Operations require appropriate levels
Data Consistency: No data duplication across tenants
Package State Consistency: Packages have valid states
DBAL Safety: No dangerous operations during errors
Audit Completeness: All privileged operations are logged

Liveness (Temporal Properties)

These properties describe what eventually happens:

Query Completion: Active queries eventually complete
Error Recovery: DBAL recovers from error states
Package Installation: Package installs eventually complete

Understanding Results

Invariant Violations

If TLC finds an invariant violation, it will show:

The violated invariant
A trace of actions leading to the violation
The state where the violation occurred

This helps identify:

Permission bypass vulnerabilities
Tenant isolation breaches
Data consistency issues
Missing audit log entries

Deadlocks

If TLC finds a deadlock (state with no enabled actions and liveness properties unfulfilled), review:

Whether queries can complete
Whether DBAL can recover from errors
Whether packages can finish installing

Extending the Specification

To add new features:

Add State Variables: Define new variables in the VARIABLES section
Update TypeOK: Add type constraints for new variables
Define Operations: Add new actions in the style of existing operations
Update Next: Include new actions in the next-state relation
Add Invariants: Define safety properties for new features
Add to Spec: Include weak fairness conditions if needed

Example: Adding workflow execution:

VARIABLES
    workflows,          \* Tenant -> Set of workflows
    runningWorkflows    \* Set of currently executing workflows

\* God can execute workflows (requires Level 5+)
ExecuteWorkflow(user, workflow) ==
    /\ CanPerformAction(user, userTenants[user], Level.God)
    /\ workflow \in workflows[userTenants[user]]
    /\ runningWorkflows' = runningWorkflows \cup {workflow}
    /\ ...

Architecture Alignment

storybook/JSON_PACKAGES.md → JSON package format and discovery This specification aligns with the MetaBuilder architecture documentation: storybook/JSON_PACKAGES.md → JSON package format and discovery

docs/architecture/security-docs/5-level-system.md → Permission model (extended to 6 levels)
schemas/package-schemas/ → 16+ JSON schemas defining package structure
docs/packages/package-sources.md → Multi-source package loading architecture
packages/*/package.json → Package metadata structure
dbal/README.md → DBAL state machine and security model
README.md → Multi-tenant system
docs/todo/improvements/20-FUTURE-FEATURES-TODO.md → Future features specifications

Schema-Specification Traceability

Schema File	TLA+ Concept	Location
`metadata_schema.json`	`PackageEntry`, `PackageIndexEntry`	`package_system.tla`
`entities_schema.json`	`DataRecords` (typed)	`metabuilder.tla`
`components_schema.json`	`exports.components`	`package_system.tla`
`permissions_schema.json`	`PermissionLevel`, `minLevel`	Both
`validation_schema.json`	`SchemaValidationRequired` invariant	`package_system.tla`

Modeling Future Features

The TLA+ specifications for future features serve multiple purposes:

1. Design Validation

Before implementing complex features like workflows or real-time collaboration, the formal specifications help:

Identify potential race conditions and deadlocks
Verify that permission enforcement is complete
Ensure multi-tenant isolation is maintained
Validate concurrency control mechanisms

2. API Contract Definition

The specifications define precise contracts for:

Package System: Schema validation, multi-source resolution, dependency management
Workflow System: Template creation, execution triggers, step dependencies
Collaboration: Session management, concurrent editing, notification delivery
Integrations: Webhook delivery guarantees, OAuth token lifecycle, rate limiting

3. Implementation Guide

Each specification provides:

Clear state transitions for the system to implement
Invariants that must be maintained by the implementation
Temporal properties describing expected system behavior
Edge cases that must be handled (retries, failures, disconnections)

4. Testing Blueprint

The specifications can guide:

Property-based testing strategies
Concurrency test scenarios
Multi-tenant isolation test cases
Load testing parameters (rate limits, concurrent users)

Running Feature Specs

Model check individual features:

# Check core system (permissions, DBAL, basic packages)
java -cp tla2tools.jar tlc2.TLC spec/metabuilder.tla -config spec/metabuilder.cfg

# Check schema-driven package system (multi-source, validation, dependencies)
java -cp tla2tools.jar tlc2.TLC spec/package_system.tla -config spec/package_system.cfg

# Check workflow system
java -cp tla2tools.jar tlc2.TLC spec/workflow_system.tla -config spec/workflow_system.cfg

# Check collaboration system
java -cp tla2tools.jar tlc2.TLC spec/collaboration.tla -config spec/collaboration.cfg

# Check integrations system
java -cp tla2tools.jar tlc2.TLC spec/integrations.tla -config spec/integrations.cfg

Or use the validation script:

cd spec && ./validate-specs.sh

Each specification is standalone and can be verified independently. This modular approach allows:

Parallel verification of different subsystems
Incremental feature development
Focused debugging when invariants are violated

References

Contributing

When modifying the system implementation:

Update this specification to reflect changes
Run the model checker to verify properties still hold
Update the configuration if new constants are needed
Document any new invariants or properties
Update this README with relevant changes

The specification serves as:

Documentation: Precise description of system behavior
Design Tool: Explore design decisions before implementation
Verification: Prove critical properties hold
Regression Prevention: Detect when changes violate invariants

Last Updated: 2025-12-27
TLA+ Version: Compatible with TLA+ 2.x
MetaBuilder Version: Iteration 25+

README.md

MetaBuilder Formal Specification