diff --git a/examples/requirements/lovable/01-todo-app/TodoApp.fizz b/examples/requirements/lovable/01-todo-app/TodoApp.fizz
new file mode 100644
index 0000000..cb21641
--- /dev/null
+++ b/examples/requirements/lovable/01-todo-app/TodoApp.fizz
@@ -0,0 +1,137 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Personal Todo App — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+# Single user — verifies CRUD, toggle, filters, clear-completed
+#
+# Modeled after: /Users/jp/src/my-simple-todo (Lovable-generated)
+# DB schema: id (UUID), text, done (bool), created_at (timestamp)
+# Ordering: ORDER BY created_at ASC — modeled as list insertion order
+
+MAX_ITEMS = 3
+
+# IDs: nominal symmetric — like UUIDs, only equality matters
+IDS = symmetry.nominal(name="id", limit=MAX_ITEMS)
+
+# Texts: interchangeable task descriptions — specific wording doesn't affect behavior
+# Using choices() rather than materialize=True: avoids spurious branching on first add
+TEXTS = symmetry.nominal(name="task", limit=2)
+
+Filter = enum("All", "Pending", "Completed")
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# Ground truth. Supabase Postgres with RLS.
+# Stored as a list to preserve insertion order (ORDER BY created_at ASC).
+
+role Server:
+    action Init:
+        self.todos = []
+
+    atomic func AddTodo(id, text):
+        self.todos = self.todos + [record(id=id, text=text, done=False)]
+
+    atomic func ToggleTodo(id):
+        updated = []
+        for t in self.todos:
+            if t.id == id:
+                updated = updated + [record(id=id, text=t.text, done=not t.done)]
+            else:
+                updated = updated + [t]
+        self.todos = updated
+
+    atomic func DeleteTodo(id):
+        self.todos = [t for t in self.todos if t.id != id]
+
+    atomic func ClearCompleted():
+        self.todos = [t for t in self.todos if not t.done]
+
+
+# ─── User (Human + Browser) ──────────────────────────────────────────
+# React frontend. Holds a filtered view refreshed after each mutation.
+# Filter is client-side state; view is derived from DB + filter.
+
+role User:
+    action Init:
+        self.filter = Filter.All
+        self.view = []
+        self.completed_exist = False
+
+    atomic func RefreshView():
+        if self.filter == Filter.All:
+            self.view = db.todos
+        elif self.filter == Filter.Pending:
+            self.view = [t for t in db.todos if not t.done]
+        else:
+            self.view = [t for t in db.todos if t.done]
+        self.completed_exist = len([t for t in db.todos if t.done]) > 0
+
+    # ── CRUD ──
+
+    atomic action AddTodo:
+        id = IDS.fresh()
+        text = any TEXTS.choices()
+        db.AddTodo(id, text)
+        self.RefreshView()
+
+    atomic action ToggleTodo:
+        require len(self.view) > 0
+        index = any range(len(self.view))
+        item = self.view[index]
+        db.ToggleTodo(item.id)
+        self.RefreshView()
+
+    atomic action DeleteTodo:
+        require len(self.view) > 0
+        index = any range(len(self.view))
+        item = self.view[index]
+        db.DeleteTodo(item.id)
+        self.RefreshView()
+
+    # ── Filter & bulk ──
+
+    atomic fair action SwitchFilter:
+        require len(db.todos) > 0
+        new_filter = fair any [f for f in dir(Filter) if self.filter != f]
+        self.filter = new_filter
+        self.RefreshView()
+
+    atomic action ClearCompleted:
+        require self.completed_exist
+        db.ClearCompleted()
+        self.RefreshView()
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    user = User()
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: The displayed list always matches the current filter applied to the DB.
+#     Catches filter-logic bugs across all possible action sequences.
+always assertion ViewMatchesFilter:
+    if user.filter == Filter.All:
+        expected = db.todos
+    elif user.filter == Filter.Pending:
+        expected = [t for t in db.todos if not t.done]
+    else:
+        expected = [t for t in db.todos if t.done]
+    return user.view == expected
+
+# R2: The "Clear Completed" button visibility stays in sync with the DB.
+always assertion CompletedFlagConsistent:
+    has_completed = len([t for t in db.todos if t.done]) > 0
+    return user.completed_exist == has_completed
+
+# R3: No duplicate todo IDs.
+always assertion UniqueTodoIds:
+    ids = [t.id for t in db.todos]
+    return len(ids) == len(set(ids))
diff --git a/examples/requirements/lovable/02-poll/Poll.fizz b/examples/requirements/lovable/02-poll/Poll.fizz
new file mode 100644
index 0000000..54ed12c
--- /dev/null
+++ b/examples/requirements/lovable/02-poll/Poll.fizz
@@ -0,0 +1,133 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Poll / Voting App — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# A creator makes a poll with a fixed set of options. Multiple voters
+# can vote, change their vote, or abstain. The creator can close the poll.
+# Once closed, no more votes are accepted.
+#
+# New concepts: multiple symmetric users, shared mutable resource, close semantics
+
+NUM_VOTERS = 2
+
+# Options are interchangeable — which specific option a voter picks doesn't matter
+OPTIONS = symmetry.nominal(name="opt", limit=3)
+
+Status = enum("Open", "Closed")
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# polls table: status, options (fixed set)
+# votes table: voter_id -> option (one vote per voter, can update)
+
+role Server:
+    action Init:
+        self.status = Status.Open
+        self.votes = {}
+
+    atomic func CastVote(voter_id, option):
+        require self.status == Status.Open
+        self.votes[voter_id] = option
+
+    atomic func RemoveVote(voter_id):
+        require self.status == Status.Open
+        require voter_id in self.votes
+        self.votes.pop(voter_id)
+
+    atomic func ClosePoll():
+        self.status = Status.Closed
+
+
+# ─── Voter (Human + Browser) ─────────────────────────────────────────
+# Each voter sees the poll and can vote/change/retract.
+# Voters are symmetric — they are interchangeable.
+
+role Voter:
+    action Init:
+        self.my_vote = None
+        self.poll_open = True
+
+    atomic func RefreshView():
+        self.poll_open = (db.status == Status.Open)
+        if self.__id__ in db.votes:
+            self.my_vote = db.votes[self.__id__]
+        else:
+            self.my_vote = None
+
+    atomic action Vote:
+        require self.poll_open
+        require self.my_vote == None
+        option = any OPTIONS.choices()
+        db.CastVote(self.__id__, option)
+        self.RefreshView()
+
+    atomic action ChangeVote:
+        require self.poll_open
+        require self.my_vote != None
+        new_option = any [o for o in OPTIONS.choices() if o != self.my_vote]
+        db.CastVote(self.__id__, new_option)
+        self.RefreshView()
+
+    atomic action RetractVote:
+        require self.poll_open
+        require self.my_vote != None
+        db.RemoveVote(self.__id__)
+        self.RefreshView()
+
+    atomic fair action RefreshPollStatus:
+        require self.poll_open and db.status == Status.Closed
+        self.RefreshView()
+
+
+# ─── Creator (poll owner) ────────────────────────────────────────────
+# The creator can close the poll. Not a voter in this model.
+
+role Creator:
+    action Init:
+        self.closed = False
+
+    atomic action ClosePoll:
+        require not self.closed
+        db.ClosePoll()
+        self.closed = True
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    creator = Creator()
+    voters = bag()
+    for i in range(NUM_VOTERS):
+        voters.add(Voter())
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: After refresh, each voter's local my_vote matches the database.
+always assertion VoterViewConsistent:
+    for v in voters:
+        if v.__id__ in db.votes:
+            if v.my_vote != None and v.my_vote != db.votes[v.__id__]:
+                return False
+        else:
+            if v.my_vote != None and not v.poll_open:
+                return False
+    return True
+
+# R2: Once the poll is closed, the votes never change.
+transition assertion ClosedPollIsImmutable(before, after):
+    if before.db.status == Status.Closed:
+        return before.db.votes == after.db.votes
+    return True
+
+# R3: Once the poll is closed, it stays closed.
+transition assertion ClosedStaysClosed(before, after):
+    if before.db.status == Status.Closed:
+        return after.db.status == Status.Closed
+    return True
diff --git a/examples/requirements/lovable/03-booking/Booking.fizz b/examples/requirements/lovable/03-booking/Booking.fizz
new file mode 100644
index 0000000..c3feba6
--- /dev/null
+++ b/examples/requirements/lovable/03-booking/Booking.fizz
@@ -0,0 +1,101 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Booking App (Calendly-style) — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# A host creates available time slots. Guests browse slots and book one.
+# Race condition: two guests see the same slot as available, both try to book.
+# The database must prevent double-booking (only one guest per slot).
+#
+# New concepts: stale views, race condition, double-booking prevention
+
+NUM_GUESTS = 2
+NUM_SLOTS = 2
+
+SLOTS = symmetry.nominal(name="slot", limit=NUM_SLOTS)
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# slots table: slot_id -> guest_id or None (None = available)
+
+role Server:
+    action Init:
+        self.slots = {}
+
+    atomic func BookSlot(slot_id, guest_id):
+        # RLS / server-side constraint: only book if available
+        require self.slots[slot_id] == None
+        self.slots[slot_id] = guest_id
+
+    atomic func CancelBooking(slot_id, guest_id):
+        require self.slots[slot_id] == guest_id
+        self.slots[slot_id] = None
+
+
+# ─── Guest (Human + Browser) ─────────────────────────────────────────
+# Sees a snapshot of available slots. By the time they click "Book",
+# another guest may have already taken the slot.
+
+symmetric role Guest:
+    action Init:
+        self.view_available = []
+        self.my_booking = None
+
+    atomic func RefreshView():
+        self.view_available = [s for s in db.slots if db.slots[s] == None]
+        # Check if I still have a booking
+        self.my_booking = None
+        for s in db.slots:
+            if db.slots[s] == self.__id__:
+                self.my_booking = s
+
+    # Guest sees available slots and picks one to book
+    atomic action BookSlot:
+        require self.my_booking == None
+        require len(self.view_available) > 0
+        slot = any self.view_available
+        db.BookSlot(slot, self.__id__)
+        self.RefreshView()
+
+    # Guest cancels their existing booking
+    atomic action CancelBooking:
+        require self.my_booking != None
+        db.CancelBooking(self.my_booking, self.__id__)
+        self.RefreshView()
+
+    # Guest refreshes their browser to see latest availability
+    atomic fair action Refresh:
+        self.RefreshView()
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+# Host creates slots, then guests join. Slot creation is setup, not ongoing behavior.
+
+action Init:
+    db = Server()
+    for i in range(NUM_SLOTS):
+        slot_id = SLOTS.fresh()
+        db.slots[slot_id] = None
+    guests = bag()
+    for i in range(NUM_GUESTS):
+        guests.add(Guest())
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: Each slot has at most one guest assigned.
+always assertion NoDoubleBooking:
+    booked_guests = [db.slots[s] for s in db.slots if db.slots[s] != None]
+    return len(booked_guests) == len(set(booked_guests))
+
+# R2: A guest holds at most one booking at a time.
+always assertion OneBookingPerGuest:
+    for g in guests:
+        count = len([s for s in db.slots if db.slots[s] == g.__id__])
+        if count > 1:
+            return False
+    return True
diff --git a/examples/requirements/lovable/04-kanban/Kanban.fizz b/examples/requirements/lovable/04-kanban/Kanban.fizz
new file mode 100644
index 0000000..4df3fcc
--- /dev/null
+++ b/examples/requirements/lovable/04-kanban/Kanban.fizz
@@ -0,0 +1,140 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Kanban Board — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# Cards live in columns: Todo -> InProgress -> Done.
+# Two users can drag cards concurrently.
+# Race: two users see the same card in "Todo", both drag to "InProgress".
+# WIP limit: at most WIP_LIMIT cards in InProgress at once.
+#
+# New concepts: multi-column state machine, concurrent drag, WIP limits
+
+NUM_USERS = 2
+MAX_CARDS = 3
+WIP_LIMIT = 2
+
+IDS = symmetry.nominal(name="card", limit=MAX_CARDS)
+TITLES = symmetry.nominal(name="task", limit=2)
+
+Column = enum("Todo", "InProgress", "Done")
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# cards table: list of records preserving creation order
+# Each card has: id, title, column
+
+role Server:
+    action Init:
+        self.cards = []
+
+    atomic func AddCard(id, title):
+        self.cards = self.cards + [record(id=id, title=title, col=Column.Todo)]
+
+    atomic func MoveCard(card_id, from_col, to_col):
+        # WIP limit: reject move to InProgress if at capacity
+        if to_col == Column.InProgress:
+            wip = len([c for c in self.cards if c.col == Column.InProgress])
+            require wip < WIP_LIMIT
+        # Server-side guard: card must still be in expected column
+        require all([c.col == from_col for c in self.cards if c.id == card_id])
+        updated = []
+        for c in self.cards:
+            if c.id == card_id:
+                updated = updated + [record(id=c.id, title=c.title, col=to_col)]
+            else:
+                updated = updated + [c]
+        self.cards = updated
+
+    atomic func DeleteCard(card_id):
+        self.cards = [c for c in self.cards if c.id != card_id]
+
+
+# ─── User (Human + Browser) ──────────────────────────────────────────
+# Each user sees a snapshot of the board. Their view can be stale.
+
+symmetric role User:
+    action Init:
+        self.view = []
+
+    atomic func RefreshView():
+        self.view = db.cards
+
+    # Add a new card to the Todo column
+    atomic action AddCard:
+        id = IDS.fresh()
+        title = any TITLES.choices()
+        db.AddCard(id, title)
+        self.RefreshView()
+
+    # Move a card to the next column (Todo->InProgress->Done)
+    atomic action MoveCardForward:
+        movable = [c for c in self.view if c.col != Column.Done]
+        require len(movable) > 0
+        card = any movable
+        if card.col == Column.Todo:
+            db.MoveCard(card.id, Column.Todo, Column.InProgress)
+        elif card.col == Column.InProgress:
+            db.MoveCard(card.id, Column.InProgress, Column.Done)
+        self.RefreshView()
+
+    # Move a card back (Done->InProgress->Todo)
+    atomic action MoveCardBack:
+        movable = [c for c in self.view if c.col != Column.Todo]
+        require len(movable) > 0
+        card = any movable
+        if card.col == Column.Done:
+            db.MoveCard(card.id, Column.Done, Column.InProgress)
+        elif card.col == Column.InProgress:
+            db.MoveCard(card.id, Column.InProgress, Column.Todo)
+        self.RefreshView()
+
+    # Delete a card
+    atomic action DeleteCard:
+        require len(self.view) > 0
+        card = any self.view
+        db.DeleteCard(card.id)
+        self.RefreshView()
+
+    # Refresh to see latest state
+    atomic fair action Refresh:
+        self.RefreshView()
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    users = bag()
+    for i in range(NUM_USERS):
+        users.add(User())
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: WIP limit is never exceeded.
+always assertion WipLimitRespected:
+    wip = len([c for c in db.cards if c.col == Column.InProgress])
+    return wip <= WIP_LIMIT
+
+# R2: Cards only move one column at a time (valid transitions).
+transition assertion ValidColumnTransitions(before, after):
+    for ac in after.db.cards:
+        for bc in before.db.cards:
+            if ac.id == bc.id and ac.col != bc.col:
+                if bc.col == Column.Todo and ac.col != Column.InProgress:
+                    return False
+                if bc.col == Column.InProgress and ac.col not in [Column.Todo, Column.Done]:
+                    return False
+                if bc.col == Column.Done and ac.col != Column.InProgress:
+                    return False
+    return True
+
+# R3: No duplicate card IDs.
+always assertion UniqueCardIds:
+    ids = [c.id for c in db.cards]
+    return len(ids) == len(set(ids))
diff --git a/examples/requirements/lovable/04-kanban/config_wip_stress.cfg b/examples/requirements/lovable/04-kanban/config_wip_stress.cfg
new file mode 100644
index 0000000..f84f9a0
--- /dev/null
+++ b/examples/requirements/lovable/04-kanban/config_wip_stress.cfg
@@ -0,0 +1,4 @@
+# Stress-test WIP limits: tighter WIP with more users
+# Usage: ./fizz --preinit-hook-file config_wip_stress.cfg Kanban.fizz
+WIP_LIMIT = 1
+NUM_USERS = 3
diff --git a/examples/requirements/lovable/05-store/Store.fizz b/examples/requirements/lovable/05-store/Store.fizz
new file mode 100644
index 0000000..140875d
--- /dev/null
+++ b/examples/requirements/lovable/05-store/Store.fizz
@@ -0,0 +1,116 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Simple Store / Inventory — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# A store has products with limited stock. Multiple buyers browse
+# and purchase items. Race condition: two buyers see stock=1, both
+# click "Buy" — only one should succeed.
+#
+# New concepts: quantity constraints, overselling prevention
+
+NUM_BUYERS = 2
+NUM_PRODUCTS = 2
+MAX_STOCK = 2
+
+PRODUCTS = symmetry.nominal(name="prod", limit=NUM_PRODUCTS)
+ORDER_IDS = symmetry.nominal(name="order", limit=4)
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# products table: product_id -> stock (int)
+# orders table: list of records (order_id, product_id, buyer_id)
+
+role Server:
+    action Init:
+        self.products = {}
+        self.orders = []
+
+    atomic func Purchase(order_id, product_id, buyer_id):
+        # Server-side constraint: only sell if in stock
+        require self.products[product_id] > 0
+        self.products[product_id] = self.products[product_id] - 1
+        self.orders = self.orders + [record(id=order_id, product=product_id, buyer=buyer_id)]
+
+    atomic func Restock(product_id, qty):
+        self.products[product_id] = self.products[product_id] + qty
+
+
+# ─── Buyer (Human + Browser) ─────────────────────────────────────────
+# Sees product listing with stock counts (possibly stale).
+
+symmetric role Buyer:
+    action Init:
+        self.view_stock = {}
+        self.my_orders = []
+
+    atomic func RefreshView():
+        self.view_stock = db.products
+        self.my_orders = [o for o in db.orders if o.buyer == self.__id__]
+
+    atomic action BuyProduct:
+        # Buyer sees items in stock
+        available = [p for p in self.view_stock if self.view_stock[p] > 0]
+        require len(available) > 0
+        product = any available
+        order_id = ORDER_IDS.fresh()
+        db.Purchase(order_id, product, self.__id__)
+        self.RefreshView()
+
+    atomic fair action Refresh:
+        self.RefreshView()
+
+
+# ─── Admin (store owner) ─────────────────────────────────────────────
+# Can restock products.
+
+role Admin:
+    action Init:
+        pass
+
+    atomic action Restock:
+        available_products = [p for p in db.products]
+        require len(available_products) > 0
+        product = any available_products
+        require db.products[product] < MAX_STOCK
+        db.Restock(product, 1)
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    # Create products with initial stock
+    for i in range(NUM_PRODUCTS):
+        pid = PRODUCTS.fresh()
+        db.products[pid] = 1
+    admin = Admin()
+    buyers = bag()
+    for i in range(NUM_BUYERS):
+        buyers.add(Buyer())
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: Stock never goes negative (no overselling).
+always assertion NoNegativeStock:
+    for p in db.products:
+        if db.products[p] < 0:
+            return False
+    return True
+
+# R2: Stock never exceeds MAX_STOCK.
+always assertion StockNotOverMax:
+    for p in db.products:
+        if db.products[p] > MAX_STOCK:
+            return False
+    return True
+
+# R3: Each order has a unique ID.
+always assertion UniqueOrderIds:
+    ids = [o.id for o in db.orders]
+    return len(ids) == len(set(ids))
diff --git a/examples/requirements/lovable/05-store/config_high_traffic.cfg b/examples/requirements/lovable/05-store/config_high_traffic.cfg
new file mode 100644
index 0000000..9a342d3
--- /dev/null
+++ b/examples/requirements/lovable/05-store/config_high_traffic.cfg
@@ -0,0 +1,4 @@
+# More buyers competing for limited stock
+# Usage: ./fizz --preinit-hook-file config_high_traffic.cfg Store.fizz
+NUM_BUYERS = 3
+MAX_STOCK = 1
diff --git a/examples/requirements/lovable/06-doc-permissions/DocPermissions.fizz b/examples/requirements/lovable/06-doc-permissions/DocPermissions.fizz
new file mode 100644
index 0000000..44e5ae0
--- /dev/null
+++ b/examples/requirements/lovable/06-doc-permissions/DocPermissions.fizz
@@ -0,0 +1,155 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Document Permissions / CMS — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# An owner creates documents and shares them with other users.
+# Permissions: owner (full control), editor (read+write), viewer (read-only).
+# The owner can grant/revoke permissions. A revoked user must not access the doc.
+#
+# New concepts: role hierarchy, access control, permission revocation
+
+NUM_DOCS = 1
+
+DOC_IDS = symmetry.nominal(name="doc", limit=NUM_DOCS)
+CONTENT = symmetry.nominal(name="ver", limit=3)
+
+Permission = enum("NoAccess", "Viewer", "Editor")
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# docs table: doc_id -> record(content, owner_id)
+# permissions table: {doc_id: {user_id: permission}}
+
+role Server:
+    action Init:
+        self.docs = {}
+        self.perms = {}
+
+    atomic func CreateDoc(doc_id, owner_id, content):
+        self.docs[doc_id] = record(content=content, owner=owner_id)
+        self.perms[doc_id] = {}
+
+    atomic func EditDoc(doc_id, user_id, new_content):
+        # Must be owner or editor
+        if self.docs[doc_id].owner != user_id:
+            require user_id in self.perms[doc_id]
+            require self.perms[doc_id][user_id] == Permission.Editor
+        self.docs[doc_id] = record(content=new_content, owner=self.docs[doc_id].owner)
+
+    atomic func ReadDoc(doc_id, user_id):
+        # Must be owner, editor, or viewer
+        if self.docs[doc_id].owner != user_id:
+            require user_id in self.perms[doc_id]
+            require self.perms[doc_id][user_id] != Permission.NoAccess
+        return self.docs[doc_id].content
+
+    atomic func GrantPermission(doc_id, owner_id, target_user, perm):
+        require self.docs[doc_id].owner == owner_id
+        self.perms[doc_id][target_user] = perm
+
+    atomic func RevokePermission(doc_id, owner_id, target_user):
+        require self.docs[doc_id].owner == owner_id
+        require target_user in self.perms[doc_id]
+        self.perms[doc_id].pop(target_user)
+
+
+# ─── Owner ────────────────────────────────────────────────────────────
+# Creates docs and manages permissions.
+
+role Owner:
+    action Init:
+        self.my_docs = []
+
+    atomic action CreateDoc:
+        doc_id = DOC_IDS.fresh()
+        content = any CONTENT.choices()
+        db.CreateDoc(doc_id, "owner", content)
+        self.my_docs = self.my_docs + [doc_id]
+
+    atomic action EditDoc:
+        require len(self.my_docs) > 0
+        doc = any self.my_docs
+        new_content = any CONTENT.choices()
+        db.EditDoc(doc, "owner", new_content)
+
+    atomic action GrantViewer:
+        require len(self.my_docs) > 0
+        doc = any self.my_docs
+        db.GrantPermission(doc, "owner", "collaborator", Permission.Viewer)
+
+    atomic action GrantEditor:
+        require len(self.my_docs) > 0
+        doc = any self.my_docs
+        db.GrantPermission(doc, "owner", "collaborator", Permission.Editor)
+
+    atomic action RevokeAccess:
+        require len(self.my_docs) > 0
+        doc = any self.my_docs
+        db.RevokePermission(doc, "owner", "collaborator")
+
+
+# ─── Collaborator (the other user) ───────────────────────────────────
+# Can read or edit depending on granted permission.
+# Their cached permission level may be stale after revocation.
+
+role Collaborator:
+    action Init:
+        self.cached_perm = Permission.NoAccess
+        self.cached_content = None
+
+    atomic func RefreshView(doc_id):
+        if doc_id in db.perms and "collaborator" in db.perms[doc_id]:
+            self.cached_perm = db.perms[doc_id]["collaborator"]
+        else:
+            self.cached_perm = Permission.NoAccess
+
+    atomic action TryRead:
+        require len(db.docs) > 0
+        doc = any db.docs.keys()
+        require self.cached_perm != Permission.NoAccess
+        content = db.ReadDoc(doc, "collaborator")
+        self.cached_content = content
+        self.RefreshView(doc)
+
+    atomic action TryEdit:
+        require len(db.docs) > 0
+        doc = any db.docs.keys()
+        require self.cached_perm == Permission.Editor
+        new_content = any CONTENT.choices()
+        db.EditDoc(doc, "collaborator", new_content)
+        self.RefreshView(doc)
+
+    atomic fair action Refresh:
+        if len(db.docs) > 0:
+            doc = any db.docs.keys()
+            self.RefreshView(doc)
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    owner = Owner()
+    collaborator = Collaborator()
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: A user with no permission cannot read a document.
+#     (Enforced by require guards in ReadDoc/EditDoc — if those are wrong,
+#     the model checker would find a path where an unauthorized read succeeds.)
+
+# R2: Only the owner can change permissions.
+#     (Enforced structurally: only Owner role calls Grant/Revoke.)
+
+# R3: The owner always retains ownership of their documents.
+always assertion OwnerNeverLosesOwnership:
+    for doc_id in db.docs:
+        if db.docs[doc_id].owner != "owner":
+            return False
+    return True
diff --git a/examples/requirements/lovable/07-approval/Approval.fizz b/examples/requirements/lovable/07-approval/Approval.fizz
new file mode 100644
index 0000000..2493529
--- /dev/null
+++ b/examples/requirements/lovable/07-approval/Approval.fizz
@@ -0,0 +1,151 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Approval Workflow — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# A submitter creates requests that go through an approval pipeline:
+#   Draft -> Submitted -> Approved / Rejected
+# Rejected requests can be revised and resubmitted.
+# Only the approver can approve/reject. Only the submitter can submit/revise.
+#
+# New concepts: multi-step state machine, role separation, resubmit loops
+
+MAX_REQUESTS = 2
+
+IDS = symmetry.nominal(name="req", limit=MAX_REQUESTS)
+
+Status = enum("Draft", "Submitted", "Approved", "Rejected")
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# requests table: list of records (id, status)
+
+role Server:
+    action Init:
+        self.requests = []
+
+    atomic func CreateRequest(id):
+        self.requests = self.requests + [record(id=id, status=Status.Draft)]
+
+    atomic func UpdateStatus(req_id, from_status, to_status):
+        # Guard: only transition from expected status
+        updated = []
+        found = False
+        for r in self.requests:
+            if r.id == req_id and r.status == from_status and not found:
+                updated = updated + [record(id=r.id, status=to_status)]
+                found = True
+            else:
+                updated = updated + [r]
+        require found
+        self.requests = updated
+
+
+# ─── Submitter ────────────────────────────────────────────────────────
+# Creates requests, submits them, revises rejected ones.
+
+role Submitter:
+    action Init:
+        self.view = []
+
+    atomic func RefreshView():
+        self.view = db.requests
+
+    atomic action CreateRequest:
+        id = IDS.fresh()
+        db.CreateRequest(id)
+        self.RefreshView()
+
+    atomic action SubmitRequest:
+        drafts = [r for r in self.view if r.status == Status.Draft]
+        require len(drafts) > 0
+        req = any drafts
+        db.UpdateStatus(req.id, Status.Draft, Status.Submitted)
+        self.RefreshView()
+
+    atomic action ReviseAndResubmit:
+        rejected = [r for r in self.view if r.status == Status.Rejected]
+        require len(rejected) > 0
+        req = any rejected
+        # Revise (back to Draft, then immediately Submit)
+        db.UpdateStatus(req.id, Status.Rejected, Status.Submitted)
+        self.RefreshView()
+
+    atomic fair action Refresh:
+        self.RefreshView()
+
+
+# ─── Approver ─────────────────────────────────────────────────────────
+# Reviews submitted requests and approves or rejects them.
+
+role Approver:
+    action Init:
+        self.view = []
+
+    atomic func RefreshView():
+        self.view = db.requests
+
+    atomic action ApproveRequest:
+        pending = [r for r in self.view if r.status == Status.Submitted]
+        require len(pending) > 0
+        req = any pending
+        db.UpdateStatus(req.id, Status.Submitted, Status.Approved)
+        self.RefreshView()
+
+    atomic action RejectRequest:
+        pending = [r for r in self.view if r.status == Status.Submitted]
+        require len(pending) > 0
+        req = any pending
+        db.UpdateStatus(req.id, Status.Submitted, Status.Rejected)
+        self.RefreshView()
+
+    atomic fair action Refresh:
+        self.RefreshView()
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    submitter = Submitter()
+    approver = Approver()
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: Valid status transitions only.
+#     Draft -> Submitted -> {Approved, Rejected}
+#     Rejected -> Submitted (resubmit)
+#     No other transitions are possible.
+transition assertion ValidTransitions(before, after):
+    for i in range(len(after.db.requests)):
+        if i < len(before.db.requests):
+            old_status = before.db.requests[i].status
+            new_status = after.db.requests[i].status
+            if old_status != new_status:
+                # Check allowed transitions
+                if old_status == Status.Draft and new_status == Status.Submitted:
+                    pass
+                elif old_status == Status.Submitted and new_status == Status.Approved:
+                    pass
+                elif old_status == Status.Submitted and new_status == Status.Rejected:
+                    pass
+                elif old_status == Status.Rejected and new_status == Status.Submitted:
+                    pass
+                else:
+                    return False
+    return True
+
+# R2: Approved requests are final — they never change status.
+transition assertion ApprovedIsFinal(before, after):
+    for i in range(len(before.db.requests)):
+        if before.db.requests[i].status == Status.Approved:
+            if i >= len(after.db.requests):
+                return False
+            if after.db.requests[i].status != Status.Approved:
+                return False
+    return True
diff --git a/examples/requirements/lovable/08-shopping-list/ShoppingList.fizz b/examples/requirements/lovable/08-shopping-list/ShoppingList.fizz
new file mode 100644
index 0000000..56cd6bd
--- /dev/null
+++ b/examples/requirements/lovable/08-shopping-list/ShoppingList.fizz
@@ -0,0 +1,135 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Shared Shopping List — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# Two household members share a shopping list. Both can add items and
+# check them off as purchased. Race condition: both see "Milk" unchecked,
+# both check it off — should result in checked once, not an error.
+# An item checked by one user should not be "unchecked" by the other.
+#
+# New concepts: collaborative editing, idempotent check-off, concurrent mutation
+
+NUM_USERS = 2
+MAX_ITEMS = 2
+
+IDS = symmetry.nominal(name="item", limit=MAX_ITEMS)
+NAMES = symmetry.nominal(name="name", limit=2)
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# items table: list of records preserving insertion order
+# Each item: id, name, checked (bool), checked_by (user or "")
+
+role Server:
+    action Init:
+        self.items = []
+
+    atomic func AddItem(id, name):
+        self.items = self.items + [record(id=id, name=name, checked=False, checked_by="")]
+
+    atomic func CheckOffItem(item_id, user_id):
+        # Idempotent: checking an already-checked item is a no-op
+        updated = []
+        for item in self.items:
+            if item.id == item_id and not item.checked:
+                updated = updated + [record(id=item.id, name=item.name, checked=True, checked_by=user_id)]
+            else:
+                updated = updated + [item]
+        self.items = updated
+
+    atomic func UncheckItem(item_id):
+        updated = []
+        for item in self.items:
+            if item.id == item_id and item.checked:
+                updated = updated + [record(id=item.id, name=item.name, checked=False, checked_by="")]
+            else:
+                updated = updated + [item]
+        self.items = updated
+
+    atomic func RemoveItem(item_id):
+        self.items = [item for item in self.items if item.id != item_id]
+
+    atomic func ClearChecked():
+        self.items = [item for item in self.items if not item.checked]
+
+
+# ─── User (Human + Browser) ──────────────────────────────────────────
+# Each user sees a snapshot of the list. Views may be stale.
+
+symmetric role User:
+    action Init:
+        self.view = []
+
+    atomic func RefreshView():
+        self.view = db.items
+
+    atomic action AddItem:
+        id = IDS.fresh()
+        name = any NAMES.choices()
+        db.AddItem(id, name)
+        self.RefreshView()
+
+    atomic action CheckOffItem:
+        unchecked = [item for item in self.view if not item.checked]
+        require len(unchecked) > 0
+        item = any unchecked
+        db.CheckOffItem(item.id, self.__id__)
+        self.RefreshView()
+
+    atomic action UncheckItem:
+        checked = [item for item in self.view if item.checked]
+        require len(checked) > 0
+        item = any checked
+        db.UncheckItem(item.id)
+        self.RefreshView()
+
+    atomic action RemoveItem:
+        require len(self.view) > 0
+        item = any self.view
+        db.RemoveItem(item.id)
+        self.RefreshView()
+
+    atomic action ClearChecked:
+        has_checked = len([item for item in self.view if item.checked]) > 0
+        require has_checked
+        db.ClearChecked()
+        self.RefreshView()
+
+    atomic fair action Refresh:
+        self.RefreshView()
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    users = bag()
+    for i in range(NUM_USERS):
+        users.add(User())
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: No duplicate item IDs.
+always assertion UniqueItemIds:
+    ids = [item.id for item in db.items]
+    return len(ids) == len(set(ids))
+
+# R2: A checked item records who checked it off.
+always assertion CheckedHasAuthor:
+    for item in db.items:
+        if item.checked and item.checked_by == "":
+            return False
+    return True
+
+# R3: An unchecked item has no author.
+always assertion UncheckedHasNoAuthor:
+    for item in db.items:
+        if not item.checked and item.checked_by != "":
+            return False
+    return True
diff --git a/examples/requirements/lovable/09-salon-booking/SalonBooking.fizz b/examples/requirements/lovable/09-salon-booking/SalonBooking.fizz
new file mode 100644
index 0000000..899d94b
--- /dev/null
+++ b/examples/requirements/lovable/09-salon-booking/SalonBooking.fizz
@@ -0,0 +1,218 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Salon Booking App — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# Three personas:
+#   Owner     — add/remove employees, cancel any appointment
+#   Employee  — add/remove own time slots, cancel own appointments (has own browser view)
+#   Customer  — browse available slots, book, cancel own bookings (has own browser view)
+#
+# Race conditions:
+#   - Two customers book the same slot (only one should succeed)
+#   - Customer books while owner removes that employee
+#   - Employee removes a slot while customer is booking it
+#
+# Employees are symmetric roles dynamically created/removed by the Owner.
+# Each employee has their own browser session with a stale view.
+
+NUM_EMPLOYEES = 2
+NUM_CUSTOMERS = 2
+MAX_SLOTS = 2
+MAX_APPTS = 2
+
+SLOT_IDS = symmetry.nominal(name="slot", limit=MAX_SLOTS)
+APPT_IDS = symmetry.nominal(name="appt", limit=MAX_APPTS)
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# employees table: set of active employee IDs
+# slots table: slot_id -> employee_id (available, unbooked)
+# appointments table: list of record(id, slot, employee, customer)
+
+role Server:
+    action Init:
+        self.employees = set()
+        self.slots = {}
+        self.appointments = []
+
+    atomic func ActivateEmployee(emp_id):
+        self.employees.add(emp_id)
+
+    atomic func DeactivateEmployee(emp_id):
+        require emp_id in self.employees
+        self.employees.discard(emp_id)
+        # Remove their available slots
+        self.slots = {sid: self.slots[sid] for sid in self.slots if self.slots[sid] != emp_id}
+        # Cancel their appointments (slots not restored — employee is gone)
+        self.appointments = [a for a in self.appointments if a.employee != emp_id]
+
+    atomic func AddSlot(slot_id, emp_id):
+        require emp_id in self.employees
+        self.slots[slot_id] = emp_id
+
+    atomic func RemoveSlot(slot_id):
+        require slot_id in self.slots
+        self.slots.pop(slot_id)
+
+    atomic func BookAppointment(appt_id, slot_id, cust_id):
+        require slot_id in self.slots
+        emp_id = self.slots[slot_id]
+        require emp_id in self.employees
+        self.slots.pop(slot_id)
+        self.appointments = self.appointments + [record(id=appt_id, slot=slot_id, employee=emp_id, customer=cust_id)]
+
+    atomic func CancelAppointment(appt_id):
+        # Restore slot to available if employee is still active
+        for a in self.appointments:
+            if a.id == appt_id:
+                if a.employee in self.employees:
+                    self.slots[a.slot] = a.employee
+        self.appointments = [a for a in self.appointments if a.id != appt_id]
+
+
+# ─── Owner ────────────────────────────────────────────────────────────
+# Manages the business: hires/fires employees, can cancel any appointment.
+
+role Owner:
+    action Init:
+        pass
+
+    atomic action AddEmployee:
+        require len(employees) < NUM_EMPLOYEES
+        emp = Employee()
+        employees.add(emp)
+        db.ActivateEmployee(emp.__id__)
+
+    atomic action RemoveEmployee:
+        require len(employees) > 0
+        emp = any employees
+        db.DeactivateEmployee(emp.__id__)
+        employees = bag([e for e in employees if e.__id__ != emp.__id__])
+
+    atomic action CancelAnyAppointment:
+        require len(db.appointments) > 0
+        appt = any db.appointments
+        db.CancelAppointment(appt.id)
+
+
+# ─── Employee (Browser Session) ──────────────────────────────────────
+# Each employee has their own browser with a stale view of their schedule.
+# Dynamically created/removed by the Owner.
+
+symmetric role Employee:
+    action Init:
+        self.view_slots = {}
+        self.my_appts = []
+
+    atomic func RefreshView():
+        self.view_slots = {sid: db.slots[sid] for sid in db.slots if db.slots[sid] == self.__id__}
+        self.my_appts = [a for a in db.appointments if a.employee == self.__id__]
+
+    # Employee opens up a time slot on their schedule
+    # Uses stale view: employee may try to add a slot after being fired
+    atomic action AddSlot:
+        slot_id = SLOT_IDS.fresh()
+        db.AddSlot(slot_id, self.__id__)
+        self.RefreshView()
+
+    # Employee removes one of their own available slots (from stale view)
+    atomic action RemoveSlot:
+        require len(self.view_slots) > 0
+        slot = any self.view_slots.keys()
+        db.RemoveSlot(slot)
+        self.RefreshView()
+
+    # Employee cancels one of their own appointments (from stale view)
+    atomic action CancelOwnAppointment:
+        require len(self.my_appts) > 0
+        appt = any self.my_appts
+        db.CancelAppointment(appt.id)
+        self.RefreshView()
+
+    # Employee refreshes to see latest schedule
+    atomic fair action Refresh:
+        if self.__id__ in db.employees:
+            self.RefreshView()
+
+
+# ─── Customer (Human + Browser) ──────────────────────────────────────
+# Browses available slots across all employees. View can be stale.
+# Two customers competing for the same slot is the core race condition.
+
+symmetric role Customer:
+    action Init:
+        self.view_slots = {}
+        self.my_appts = []
+
+    atomic func RefreshView():
+        self.view_slots = db.slots
+        self.my_appts = [a for a in db.appointments if a.customer == self.__id__]
+
+    # Customer picks an available slot and books it
+    atomic action BookSlot:
+        require len(self.view_slots) > 0
+        slot = any self.view_slots.keys()
+        appt_id = APPT_IDS.fresh()
+        db.BookAppointment(appt_id, slot, self.__id__)
+        self.RefreshView()
+
+    # Customer cancels one of their own appointments
+    atomic action CancelMyAppointment:
+        require len(self.my_appts) > 0
+        appt = any self.my_appts
+        db.CancelAppointment(appt.id)
+        self.RefreshView()
+
+    # Customer refreshes to see latest availability
+    atomic fair action Refresh:
+        self.RefreshView()
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    owner = Owner()
+    employees = bag()
+    customers = bag()
+    for i in range(NUM_CUSTOMERS):
+        customers.add(Customer())
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: No double-booking — a slot appears in at most one appointment.
+always assertion NoDoubleBooking:
+    booked_slots = [a.slot for a in db.appointments]
+    return len(booked_slots) == len(set(booked_slots))
+
+# R2: A booked slot is never also listed as available.
+always assertion BookedNotAvailable:
+    for a in db.appointments:
+        if a.slot in db.slots:
+            return False
+    return True
+
+# R3: All appointments reference active employees.
+always assertion AppointmentsHaveActiveEmployee:
+    for a in db.appointments:
+        if a.employee not in db.employees:
+            return False
+    return True
+
+# R4: All available slots belong to active employees.
+always assertion SlotsHaveActiveEmployee:
+    for sid in db.slots:
+        if db.slots[sid] not in db.employees:
+            return False
+    return True
+
+# R5: Unique appointment IDs.
+always assertion UniqueAppointmentIds:
+    ids = [a.id for a in db.appointments]
+    return len(ids) == len(set(ids))
diff --git a/examples/requirements/lovable/09-salon-booking/config_busy_salon.cfg b/examples/requirements/lovable/09-salon-booking/config_busy_salon.cfg
new file mode 100644
index 0000000..bcbd821
--- /dev/null
+++ b/examples/requirements/lovable/09-salon-booking/config_busy_salon.cfg
@@ -0,0 +1,4 @@
+# More employees and customers with same resource limits
+# Usage: ./fizz --preinit-hook-file config_busy_salon.cfg SalonBooking.fizz
+NUM_EMPLOYEES = 3
+NUM_CUSTOMERS = 3
diff --git a/examples/requirements/lovable/10-salon-schedule/SalonSchedule.fizz b/examples/requirements/lovable/10-salon-schedule/SalonSchedule.fizz
new file mode 100644
index 0000000..3999f9d
--- /dev/null
+++ b/examples/requirements/lovable/10-salon-schedule/SalonSchedule.fizz
@@ -0,0 +1,157 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Salon Booking with Schedules and Time
+# Architecture: React (browser) + Supabase (database)
+#
+# Models:
+#   - Employee recurring schedules (day-of-week × time-slot)
+#   - Slot generation from schedule (computed when customer views)
+#   - Passage of time (clock phases within a day, days advancing)
+#   - Past slots can't be booked or cancelled
+#   - Schedule changes only affect future slot generation (existing bookings remain)
+#
+# Time model:
+#   - Calendar day: interval symmetry (only relative distances matter)
+#     No MAX_DAYS needed — states normalize by shifting.
+#   - Day of week: plain int with manual % (no symmetry reduction needed)
+#   - Time phase within day: plain int (BETWEEN=0, SLOT_1=1, ..., SLOT_N=N)
+#     PRE and POST are merged into a single BETWEEN phase (no slot active).
+#
+# Schedule encoding:
+#   (day_of_week, slot_index) → dow * SLOTS_PER_DAY + slot_idx
+
+# ─── Configuration ───────────────────────────────────────────────────
+
+DAYS_IN_WEEK = 2        # 2-day week: different schedules per day
+SLOTS_PER_DAY = 2       # bookable time slots per day
+BOOKING_WINDOW = 1      # can book for today only (1) or today+tomorrow (2)
+
+# Phases per day: 0=BETWEEN (no slot active), 1..SLOTS_PER_DAY = during slot
+# PRE+POST merged: after last slot, clock advances to next day's BETWEEN.
+
+# limit = BOOKING_WINDOW + 1: need +1 slack because AdvanceClock temporarily
+# creates a 2nd day value (clock_day + 1) before cleanup removes old references.
+DAYS = symmetry.interval(name="day", limit=BOOKING_WINDOW + 1)
+
+NUM_CUSTOMERS = 2
+
+APPT_IDS = symmetry.nominal(name="appt", limit=3)
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+
+role Server:
+    action Init:
+        # schedule: set of encoded codes (dow * SLOTS_PER_DAY + slot)
+        self.schedule = set()
+        # appointments: list of record(id, cal_day, slot, customer)
+        self.appointments = []
+
+    atomic func ToggleSchedule(schedule_code):
+        if schedule_code in self.schedule:
+            self.schedule.discard(schedule_code)
+        else:
+            self.schedule.add(schedule_code)
+
+    atomic func BookAppointment(appt_id, cal_day, slot_idx, dow_idx, cust_id):
+        require dow_idx * SLOTS_PER_DAY + slot_idx in self.schedule
+        require cal_day > clock_day or (cal_day == clock_day and slot_idx + 1 > clock_phase)
+        require all([not (a.cal_day == cal_day and a.slot == slot_idx) for a in self.appointments])
+        self.appointments = self.appointments + [record(id=appt_id, cal_day=cal_day, slot=slot_idx, customer=cust_id)]
+
+    atomic func CancelAppointment(appt_id):
+        require all([a.cal_day > clock_day or (a.cal_day == clock_day and a.slot + 1 > clock_phase) for a in self.appointments if a.id == appt_id])
+        self.appointments = [a for a in self.appointments if a.id != appt_id]
+
+    atomic func CleanupPast():
+        self.appointments = [a for a in self.appointments if a.cal_day >= clock_day]
+
+
+# ─── Employee ────────────────────────────────────────────────────────
+
+role Employee:
+    action Init:
+        pass
+
+    atomic action ToggleScheduleSlot:
+        schedule_code = any range(DAYS_IN_WEEK * SLOTS_PER_DAY)
+        db.ToggleSchedule(schedule_code)
+
+
+# ─── Customer (Human + Browser) ──────────────────────────────────────
+# Two customers competing for the same slot is the core race condition.
+
+symmetric role Customer:
+    action Init:
+        self.view_slots = []
+        self.my_appts = []
+
+    atomic func RefreshView():
+        self.view_slots = [record(cal_day=clock_day + d, slot=s, dow_idx=(clock_dow + d) % DAYS_IN_WEEK)
+            for d in range(BOOKING_WINDOW)
+            for s in range(SLOTS_PER_DAY)
+            if (clock_dow + d) % DAYS_IN_WEEK * SLOTS_PER_DAY + s in db.schedule
+            if d > 0 or s + 1 > clock_phase
+            if all([not (a.cal_day == clock_day + d and a.slot == s) for a in db.appointments])]
+        self.my_appts = [a for a in db.appointments if a.customer == self.__id__]
+
+    atomic action BookSlot:
+        chosen = any self.view_slots
+        appt_id = APPT_IDS.fresh()
+        db.BookAppointment(appt_id, chosen.cal_day, chosen.slot, chosen.dow_idx, self.__id__)
+        self.RefreshView()
+
+    atomic action CancelMyAppointment:
+        appt = any [a for a in self.my_appts if a.cal_day > clock_day or (a.cal_day == clock_day and a.slot + 1 > clock_phase)]
+        db.CancelAppointment(appt.id)
+        self.RefreshView()
+
+    atomic fair action Refresh:
+        self.RefreshView()
+
+
+# ─── Clock ───────────────────────────────────────────────────────────
+
+atomic fair action AdvanceClock:
+    if clock_phase < SLOTS_PER_DAY:
+        clock_phase = clock_phase + 1
+    else:
+        clock_day = clock_day + 1
+        clock_dow = (clock_dow + 1) % DAYS_IN_WEEK
+        clock_phase = 0
+        db.CleanupPast()
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    emp = Employee()
+    customers = bag()
+    for i in range(NUM_CUSTOMERS):
+        customers.add(Customer())
+    clock_day = DAYS.min()
+    clock_dow = 0
+    clock_phase = 0
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+always assertion NoDoubleBooking:
+    for i in range(len(db.appointments)):
+        for j in range(i + 1, len(db.appointments)):
+            if db.appointments[i].cal_day == db.appointments[j].cal_day:
+                if db.appointments[i].slot == db.appointments[j].slot:
+                    return False
+    return True
+
+# All appointments are in the future (past appointments get cleaned up).
+always assertion NoPastAppointments:
+    for a in db.appointments:
+        if a.cal_day < clock_day:
+            return False
+    return True
diff --git a/examples/requirements/lovable/10-salon-schedule/config_large.cfg b/examples/requirements/lovable/10-salon-schedule/config_large.cfg
new file mode 100644
index 0000000..ef10537
--- /dev/null
+++ b/examples/requirements/lovable/10-salon-schedule/config_large.cfg
@@ -0,0 +1,7 @@
+# Realistic scale — use with simulation mode only
+# Symmetry domain limits are unchanged; simulation mode ignores them anyway.
+# Usage: ./fizz -x --max_runs 1 --seed 42 --preinit-hook-file config_large.cfg SalonSchedule.fizz
+DAYS_IN_WEEK = 7
+SLOTS_PER_DAY = 12
+BOOKING_WINDOW = 7
+NUM_CUSTOMERS = 10
diff --git a/examples/requirements/lovable/10-salon-schedule/config_multiday.cfg b/examples/requirements/lovable/10-salon-schedule/config_multiday.cfg
new file mode 100644
index 0000000..789510e
--- /dev/null
+++ b/examples/requirements/lovable/10-salon-schedule/config_multiday.cfg
@@ -0,0 +1,5 @@
+# Single customer, wider schedule — verifies clock/cleanup with more days
+# Usage: ./fizz --preinit-hook-file config_multiday.cfg SalonSchedule.fizz
+NUM_CUSTOMERS = 1
+DAYS_IN_WEEK = 3
+SLOTS_PER_DAY = 1
diff --git a/examples/requirements/lovable/10-salon-schedule/config_race.cfg b/examples/requirements/lovable/10-salon-schedule/config_race.cfg
new file mode 100644
index 0000000..e8cbc8e
--- /dev/null
+++ b/examples/requirements/lovable/10-salon-schedule/config_race.cfg
@@ -0,0 +1,5 @@
+# Multiple customers on few slots — focus on double-booking race
+# Usage: ./fizz --preinit-hook-file config_race.cfg SalonSchedule.fizz
+NUM_CUSTOMERS = 3
+DAYS_IN_WEEK = 1
+SLOTS_PER_DAY = 1
diff --git a/examples/requirements/lovable/MODELING_GUIDE.md b/examples/requirements/lovable/MODELING_GUIDE.md
new file mode 100644
index 0000000..2bcd807
--- /dev/null
+++ b/examples/requirements/lovable/MODELING_GUIDE.md
@@ -0,0 +1,282 @@
+# Modeling Lovable Apps in FizzBee
+
+Guide for writing formal specifications of apps built with Lovable
+(React frontend + Supabase/Postgres server).
+
+---
+
+## Architecture Mapping
+
+| Lovable Component | FizzBee Model |
+|:---|:---|
+| Supabase database | `role Server` (single instance, ground truth) |
+| User's browser | `role User` or `symmetric role Customer` (view + actions) |
+| React component state | `self.view_*` fields on user roles |
+| Supabase table row | Record in a list on the Server role |
+| Row-level security (RLS) | `require` guards in Server functions |
+| Supabase realtime | Not modeled — user refreshes manually (stale views) |
+
+### Why Model Stale Views?
+
+In Lovable apps, the browser fetches data and caches it locally. Between
+fetches, other users (or the clock) can change the database. The spec
+models this explicitly:
+
+1. **RefreshView**: Reads current database state into `self.view_*`
+2. **User action**: Reads from `self.view_*` (potentially stale)
+3. **Server function**: Validates against current database state with `require`
+
+This pattern catches race conditions where two users see the same slot
+as available but only one can book it.
+
+---
+
+## Spec Structure
+
+```python
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Constants and symmetry domains
+# ...
+
+role Server:
+    action Init:
+        # Initialize database tables as lists/sets/dicts
+    # Atomic functions for database operations (INSERT, UPDATE, DELETE)
+    # Each function validates with require guards (like RLS policies)
+
+symmetric role User:
+    action Init:
+        # Initialize view state
+    atomic func RefreshView():
+        # Read from db.* into self.view_*
+    atomic action SomeUserAction:
+        # Pick from self.view_*, call db.SomeOperation(), refresh view
+
+# Clock (if time matters)
+atomic fair action AdvanceClock:
+    # Advance time, clean up past data
+
+action Init:
+    db = Server()
+    users = bag()
+    for i in range(NUM_USERS):
+        users.add(User())
+
+always assertion SomeInvariant:
+    # Check database consistency
+```
+
+### Key Settings
+
+- **`deadlock_detection: false`**: Users can always stop interacting
+- **`max_concurrent_actions: 1`**: Single-user interaction at a time
+  (even with multiple user roles, only one acts per step)
+
+---
+
+## Common Patterns
+
+### Database Tables as Lists
+
+Use lists when insertion order matters (e.g., `ORDER BY created_at`):
+
+```python
+self.items = []
+self.items = self.items + [record(id=item_id, name=name, created_by=user_id)]
+```
+
+Use sets for unordered unique values:
+
+```python
+self.schedule = set()
+self.schedule.add(schedule_code)
+self.schedule.discard(schedule_code)
+```
+
+### Stale View → Server Validation
+
+The core race condition pattern:
+
+```python
+symmetric role Customer:
+    atomic func RefreshView():
+        self.view_slots = [s for s in db.available_slots if is_valid(s)]
+
+    atomic action BookSlot:
+        chosen = any self.view_slots          # Pick from stale view
+        db.BookSlot(chosen, self.__id__)      # Server validates
+        self.RefreshView()                     # Refresh after action
+
+role Server:
+    atomic func BookSlot(slot, customer_id):
+        require slot in self.available_slots   # Might fail if stale
+        self.available_slots.remove(slot)
+        self.bookings.append(record(slot=slot, customer=customer_id))
+```
+
+### Dynamic Actors (Hire/Fire Employees)
+
+Use `symmetric role` + `bag()` for actors that can be added and removed:
+
+```python
+symmetric role Employee:
+    action Init:
+        self.status = "active"
+
+role Owner:
+    atomic action HireEmployee:
+        emp = Employee()
+        employees.add(emp)
+        db.ActivateEmployee(emp.__id__)
+
+    atomic action FireEmployee:
+        emp = any employees
+        db.DeactivateEmployee(emp.__id__)
+        employees = bag([e for e in employees if e.__id__ != emp.__id__])
+```
+
+No hire cap needed — symmetry means removed-then-recreated actors map
+to the same canonical states.
+
+### Time Modeling
+
+When appointments, deadlines, or expiration matter:
+
+```python
+DAYS = symmetry.interval(name="day", limit=BOOKING_WINDOW + 1)
+
+# +1 slack because AdvanceClock temporarily creates a 2nd day value
+# (clock_day + 1) before cleanup removes old references.
+
+atomic fair action AdvanceClock:
+    if clock_phase < SLOTS_PER_DAY:
+        clock_phase = clock_phase + 1
+    else:
+        clock_day = clock_day + 1
+        clock_dow = (clock_dow + 1) % DAYS_IN_WEEK
+        clock_phase = 0
+        db.CleanupPast()  # Free interval slots for garbage-collected data
+```
+
+**Why `limit = BOOKING_WINDOW + 1`?** When `AdvanceClock` increments
+`clock_day`, it temporarily creates a new day value. Old references
+(appointments, cached views) still point to the old day. With `limit=N`,
+at most N distinct interval values can coexist. The +1 accommodates
+this transient state before cleanup runs.
+
+### Unique IDs
+
+Use nominal symmetry for database primary keys:
+
+```python
+APPT_IDS = symmetry.nominal(name="appt", limit=3)
+appt_id = APPT_IDS.fresh()
+```
+
+The limit should be the max number of live records, not total ever created.
+Garbage-collect old records to free slots.
+
+### Cross-Role Function Returns
+
+`self.x = otherRole.fn()` crashes. Use a local variable:
+
+```python
+# CRASHES
+self.cached = db.ReadDoc(doc_id)
+
+# WORKS
+content = db.ReadDoc(doc_id)
+self.cached = content
+```
+
+---
+
+## Performance Tips for Lovable Specs
+
+1. **List comprehensions over loops**: Each statement creates nodes.
+   Collapse nested loops and if-chains into single comprehensions.
+
+2. **`any` blocks on empty**: No need for `require len(xs) > 0` before `any xs`.
+
+3. **`require all([...])`** instead of for-loop with require.
+
+4. **Tight symmetry limits**: `limit` = max coexisting values, not total ever.
+
+5. **Merge equivalent phases**: If PRE and POST have identical behavior,
+   combine into single BETWEEN phase (~25% state reduction).
+
+6. **Garbage-collect**: Remove expired records to free symmetry slots.
+
+See [Performance Guide](../../references/PERFORMANCE_GUIDE.md) for details.
+
+---
+
+## Verification Workflow
+
+Don't just check "PASSED" — verify the spec models the right thing.
+
+### 1. Simulate and Read Traces
+
+```bash
+./fizz -x --max_runs 1 --seed 1 spec.fizz
+grep -o 'label="[^"]*"' path/to/out/*/graph.dot | sed 's/.*label="//;s/"//'
+```
+
+Check: Are bookings, cancels, schedule changes happening? Is time advancing?
+
+### 2. Write Guided Traces for Key Scenarios
+
+```bash
+./fizz --trace "Employee#0.ToggleScheduleSlot
+Any:schedule_code=0
+Customer#0.Refresh
+Customer#0.BookSlot
+Any:chosen=record(cal_day = day0, dow_idx = 0, slot = 0)
+AdvanceClock
+AdvanceClock
+AdvanceClock
+Customer#0.Refresh" spec.fizz
+```
+
+If a step is blocked, you get **"Trace execution incomplete"** — investigate why.
+
+### 3. Reduce Config for Debugging
+
+```python
+DAYS_IN_WEEK = 1
+SLOTS_PER_DAY = 1
+BOOKING_WINDOW = 1
+NUM_CUSTOMERS = 1  # or remove symmetric role, use single role
+```
+
+Small configs generate visual graphs (< 250 nodes).
+
+### 4. Visualize
+
+```bash
+dot -Tsvg path/to/out/*/graph.dot -o graph.svg && open graph.svg
+```
+
+See [Verification Guide](../../references/VERIFICATION_GUIDE.md) for the full workflow.
+
+---
+
+## Examples
+
+| # | App | Key Features | States |
+|:--|:----|:-------------|:-------|
+| 01 | Todo | CRUD, reordering | 52 |
+| 02 | Poll | Multi-option voting, toggle | 72 |
+| 03 | Booking | Time slots, double-booking prevention | 94 |
+| 04 | Kanban | Drag-drop columns, WIP limits | 26 |
+| 05 | Store | Cart, inventory, checkout | 308 |
+| 06 | Doc Permissions | Owner/viewer/editor, access control | 28 |
+| 07 | Approval | Multi-stage workflow, roles | 56 |
+| 08 | Shopping List | Collaborative editing, real-time sync | 202 |
+| 09 | Salon Booking | Dynamic employees, symmetric roles | 1,012 |
+| 10 | Salon Schedule | Recurring schedules, time passage, interval symmetry | 14,496 |