fizz-spec

FizzBee Spec Writing

FizzBee is a Python-like formal spec language built on Starlark. Specs model distributed systems; the model checker exhaustively verifies safety and liveness properties.

Full reference: ~/.claude/skills/fizzbee-docs/LANGUAGE_REFERENCE.md Examples index: ~/.claude/skills/fizzbee-docs/README.md

Installation

brew tap fizzbee-io/fizzbee && brew install fizzbee
# Then run: fizz spec.fizz

---

File Structure

---
# Optional YAML frontmatter
options:
  max_actions: 100
  max_concurrent_actions: 2   # 1 for single-user apps
  crash_on_yield: true        # enable fault injection

action_options:
  "RoleName.ActionName":
    max_actions: 10

deadlock_detection: true      # false for interactive apps
liveness: strict
---

Then the Fizz spec:

1. Top-level constants
2. Functions (pure helpers)
3. Roles (actors/processes)
4. Top-level actions (Init + others)
5. Assertions

---

Core Syntax

Constants and Global State

MAX = 10                        # constant
State = enum('IDLE', 'RUNNING') # enum

action Init:
    counter = 0      # becomes global state variable
    items = []
    server = Server()  # create role instance

Actions

# Modifier order: [flow] [fairness] action Name
atomic action Increment:        # atomic = no interleaving
    counter = counter + 1

fair action Progress:           # fair = weak fairness
    require not done
    done = True

atomic fair action Produce:     # both modifiers
    require len(queue) < MAX
    queue.append(item)

Key rules:

• No parameters on actions
• Init runs once; all variables defined in it become global state
• require condition disables the action (doesn't execute it)
• An action is "enabled" only after it executes a simple statement (=, method call, pass)

Roles

@state(ephemeral=['cache'])     # cache resets on crash
role Server:
    action Init:
        self.data = {}          # role state (persists)
        self.cache = {}         # ephemeral (resets on crash)

    atomic func Read(key):      # function: can have params + return
        return self.data.get(key, None)

    action Write:
        key = oneof self.pending_keys
        self.data[key] = self.pending[key]