# FizzBee

> The easiest formal specification language and model checker for the full development cycle: requirements analysis, design verification, and model-based testing.

FizzBee specs look like Python: you model a system as actions on state, then the model checker explores every interleaving to verify safety and liveness properties, and the model-based testing runner checks a real implementation against the model. Each page below is available as clean markdown at the listed URL; the HTML version is the same URL without `index.md`.

## Language Reference

- [Introduction](https://fizzbee.io/reference/language/introduction/index.md): What FizzBee is: a Python-like formal specification language built on Starlark, with explicit model checking, implicit fault injection and role-based modeling.
- [Language Reference](https://fizzbee.io/reference/language/index.md): The FizzBee specification language chapter by chapter: syntax and semantics of every construct, each with runnable examples and expected results.
- [File Structure](https://fizzbee.io/reference/language/file-structure/index.md): How a FizzBee spec file is laid out: optional YAML frontmatter for model-checker options, followed by the specification itself.
- [Keywords and Reserved Words](https://fizzbee.io/reference/language/keywords-and-reserved-words/index.md): Every FizzBee keyword in one place: flow modifiers, fairness and assertion modifiers, control flow, state and scope, and built-in types.
- [Actions](https://fizzbee.io/reference/language/actions/index.md): FizzBee actions: how the model checker invokes them, the Init action, enabling conditions with require, and the pass statement, with runnable examples.
- [Functions](https://fizzbee.io/reference/language/functions/index.md): FizzBee functions: atomic vs serial functions, where they can be called from, and the limits on call syntax, with runnable examples.
- [Roles](https://fizzbee.io/reference/language/roles/index.md): FizzBee roles model actors and processes: role state, Init, durable vs ephemeral state, and how roles call each other, with runnable examples.
- [Flow Modifiers](https://fizzbee.io/reference/language/flow-modifiers/index.md): Atomic, serial, parallel and oneof blocks in FizzBee: how each controls execution and where yield points let other actions interleave.
- [Fairness](https://fizzbee.io/reference/language/fairness/index.md): Unfair, weakly fair and strongly fair actions in FizzBee, and why liveness properties need fairness, with runnable examples of each.
- [Assertions](https://fizzbee.io/reference/language/assertions/index.md): FizzBee assertions: always (safety), exists, transition, eventually always and always eventually (liveness), plus next_states() lookahead, with examples.
- [Data Structures](https://fizzbee.io/reference/language/data-structures/index.md): FizzBee data structures: lists, sets, dicts, bags, enums, records and structs, and the generic collections for unhashable values, with runnable examples.
- [Control Flow](https://fizzbee.io/reference/language/control-flow/index.md): if/elif/else, for and while loops, break and continue, and checkpoints in FizzBee, including how loops behave under atomic, serial and parallel modifiers.
- [Nondeterminism](https://fizzbee.io/reference/language/nondeterminism/index.md): Nondeterministic choice in FizzBee: the any statement, oneof blocks, fairness on choices, and the concise vs block forms, with runnable examples.
- [State Management](https://fizzbee.io/reference/language/state-management/index.md): How FizzBee state works: global variables from Init, top-level constants, local variables, and per-role state, with runnable examples.
- [Fault Injection](https://fizzbee.io/reference/language/fault-injection/index.md): Implicit fault injection in FizzBee: crashes at yield points, message loss in RPC, and how ephemeral vs durable state behaves after a crash.
- [Configuration](https://fizzbee.io/reference/language/configuration/index.md): Configuring the FizzBee model checker: options in YAML frontmatter or fizz.yaml, per-action options, and which setting takes precedence.
- [Symmetry Reduction](https://fizzbee.io/reference/language/symmetry-reduction/index.md): Symmetry reduction in FizzBee: symmetric values and roles, why lists break symmetry, measuring the state-space savings, and the symmetry module API.
- [Best Practices](https://fizzbee.io/reference/language/best-practices/index.md): Writing FizzBee specs that check fast and mean what you think: bounding state, guard clauses, atomic vs serial, role design, assertions and fairness.
- [Quick Reference](https://fizzbee.io/reference/language/quick-reference/index.md): A FizzBee cheat sheet: common spec patterns such as mutexes and retries, plus debugging tips for failing or slow model checks.
- [Standard Library](https://fizzbee.io/reference/language/standard-library/index.md): The modules and builtins every FizzBee spec can use without imports: top-level builtins, math, itertools and symmetry, and the method-call form.
- [Known Issues and Limitations](https://fizzbee.io/reference/language/known-issues-and-limitations/index.md): Current FizzBee limitations and known issues, such as error line numbers and unsupported Python features, with workarounds for each.
- [Gotchas and Common Issues](https://fizzbee.io/reference/language/gotchas/index.md): FizzBee gotchas: language quirks that trip people up, such as tuple unpacking, require vs assertions and the any keyword, with fixes.

## Model Checker Guides

- [Verification Guide](https://fizzbee.io/reference/verification/index.md): How to check that a FizzBee spec is right, not just passing: simulation, guided traces, and sanity checks beyond PASSED and state counts.
- [Performance Guide](https://fizzbee.io/reference/performance/index.md): Make FizzBee model checking faster: practical ways to shrink the state space and runtime, each ranked by typical impact.
- [Reference](https://fizzbee.io/reference/index.md): FizzBee language reference: actions, functions, roles, flow modifiers, fairness, assertions, fault injection and symmetry, each with runnable examples.

## Distributed Systems Patterns

- [Distributed Systems Patterns](https://fizzbee.io/design/patterns/index.md): Locking, sagas, consensus, message queues, caching and circuit breakers as small runnable formal models, each with the invariants checked and the expected result.
- [Mutex Pattern](https://fizzbee.io/design/patterns/mutex/index.md): The mutex pattern as a runnable model: threads lock and unlock around a critical section, and a model checker verifies mutual exclusion in every interleaving.
- [Read-Write Lock Pattern](https://fizzbee.io/design/patterns/read-write-lock/index.md): A read-write lock as a runnable model: many concurrent readers or one exclusive writer, checked so no reader ever overlaps a writer and at most one writer holds the lock.
- [Distributed Lock Pattern](https://fizzbee.io/design/patterns/distributed-lock/index.md): Distributed lock with lease expiration and fencing tokens: a runnable model of clients competing for a lock, checked so at most one client holds a valid lease and tokens only increase.
- [Optimistic Locking Pattern](https://fizzbee.io/design/patterns/optimistic-locking/index.md): Optimistic locking with version numbers: a runnable model of concurrent read-modify-write updates using compare-and-set, checked for lost updates.
- [Saga Pattern](https://fizzbee.io/design/patterns/saga-pattern/index.md): The saga pattern as a runnable model: a long-running transaction that runs compensating steps to roll back on failure, checked so a completed saga committed every step and a rolled-back one undid its work.
- [Snapshot Isolation Pattern](https://fizzbee.io/design/patterns/snapshot-isolation/index.md): Snapshot isolation as a runnable model: transactions read from a snapshot and commit only if their write sets do not conflict, checked for lost updates.
- [Leader Election (Simplified Raft)](https://fizzbee.io/design/patterns/leader-election/index.md): Leader election with term-based voting, a simplified Raft: nodes request votes over RPC and a model checker verifies at most one leader per term.
- [Compare-And-Swap Pattern](https://fizzbee.io/design/patterns/compare-and-swap/index.md): Compare-and-swap for lock-free updates: a runnable model of concurrent CAS retries on a shared value, checked so the value stays valid under every interleaving.
- [Producer-Consumer Pattern](https://fizzbee.io/design/patterns/producer-consumer/index.md): The producer-consumer problem with a bounded buffer: a runnable model checked so the buffer never overflows and consumers only take items that were produced.
- [Message Queue Pattern](https://fizzbee.io/design/patterns/message-queue/index.md): A message queue with multiple producers and consumers: a runnable model that checks FIFO order, no duplicate deliveries, and that every message is eventually consumed.
- [Cache Coherence Pattern](https://fizzbee.io/design/patterns/cache-coherence/index.md): Cache coherence with a write-through cache and invalidation: a runnable model checked so a cached value never disagrees with the backing store.
- [Eventual Consistency Pattern](https://fizzbee.io/design/patterns/eventual-consistency/index.md): Eventual consistency with asynchronous primary-replica replication: a runnable model checking that replicas never get ahead of the primary and eventually converge.
- [Idempotent Operations Pattern](https://fizzbee.io/design/patterns/idempotent-operations/index.md): Idempotent operations with request IDs: a runnable model of retried requests and deduplication, checked so a retried request is never applied twice.
- [Circuit Breaker Pattern](https://fizzbee.io/design/patterns/circuit-breaker/index.md): The circuit breaker pattern as a runnable model: closed, open and half-open states, checked so the circuit is never closed once failures reach the threshold.
- [Rate Limiting Pattern](https://fizzbee.io/design/patterns/rate-limiting/index.md): A token bucket rate limiter as a runnable model: tokens refill and requests spend them, checked so the bucket stays within capacity and only funded requests are processed.
- [Write-Ahead Log Pattern](https://fizzbee.io/design/patterns/write-ahead-log/index.md): A write-ahead log as a runnable model: changes are logged before they are applied, checked so the data always matches the last applied log entry.
- [Event Sourcing Pattern](https://fizzbee.io/design/patterns/event-sourcing/index.md): Event sourcing as a runnable model: state is derived from an append-only event stream, checked so replaying the events always rebuilds the same state.

## Design Tutorials

- [Quick Start: Modeling and Validating Distributed Systems in FizzBee](https://fizzbee.io/design/tutorials/quick-start/index.md): Model a gossip protocol and watch the model checker find design flaws for you. A hands-on introduction to formal methods for distributed systems.
- [Getting Started](https://fizzbee.io/design/tutorials/getting-started/index.md): Learn how to model systems with FizzBee. This guide walks you through writing your first FizzBee model, covering key concepts like actions, control flow, non-determinism, fairness, and correctness properties—no prior formal methods experience needed.
- [Guard Clauses And Enabling Conditions](https://fizzbee.io/design/tutorials/guard-clause/index.md): Learn how guard clauses and enabling conditions work in FizzBee to control action transitions. This guide covers testing for deadlocks, liveness, and common pitfalls—a must-read before you start writing your first model.
- [Tutorials](https://fizzbee.io/design/tutorials/index.md): Learn FizzBee step by step: your first specification, then guards, fairness and liveness, roles, channels and fault injection. No prior formal methods experience needed.
- [Config and Front Matter](https://fizzbee.io/design/tutorials/frontmatter/index.md): Configure the FizzBee model checker with fizz.yaml or spec front matter: action options, invariant handling, exploration limits, and more.
- [Liveness and Fairness](https://fizzbee.io/design/tutorials/liveness/index.md): Liveness ensures something good eventually happens. Learn how to model and verify liveness properties in FizzBee, from fairness levels to temporal logic—crucial for designing reliable distributed systems.
- [Enums, Records, and Collections](https://fizzbee.io/design/tutorials/datastructures/index.md): Learn how to use enums, records, collections, and other common data structures in FizzBee.
- [Modeling msg delivery guarantees](https://fizzbee.io/design/tutorials/msg-delivery-guarantees/index.md): Learn how to model message delivery guarantees in distributed systems—ordered vs. unordered delivery, at most once, exactly once, at least once, message deduplication, and more.
- [Actors / Roles](https://fizzbee.io/design/tutorials/roles/index.md): Roles are a core concept in FizzBee, simplifying how we model system participants like microservices, processes, and threads. Learn how to define roles, manage state, handle communication, and model dynamic behaviors.
- [Channels](https://fizzbee.io/design/tutorials/channels/index.md): Channels make modeling message passing as intuitive as sketching on a whiteboard. Learn how to define delivery, ordering, and blocking behavior with default and custom channels.
- [Implicit Fault Injection](https://fizzbee.io/design/tutorials/fault-injection/index.md): Explore FizzBee’s built-in fault injection for modeling failures in distributed systems. Learn how the model checker simulates message loss, network partitions, crashes, and more to test system resilience.
- [Symmetry Reduction](https://fizzbee.io/design/tutorials/symmetry_reduction/index.md): Symmetry reduction is a technique for modeling values and objects that are interchangeable, while reducing the number of states explored by the model checker. FizzBee supports extensive symmetry types like nominal, ordinal, interval, rotational and reflection symmetries that go beyond what are supported by most formal modeling systems.
- [Probabilistic Modeling](https://fizzbee.io/design/tutorials/probabilistic-modeling/index.md): Learn how to model uncertainty in distributed systems using probabilities. This tutorial covers random events like message loss, failures, and API errors—laying the foundation for performance and reliability analysis.
- [Performance Modeling](https://fizzbee.io/design/tutorials/performance-modeling/index.md): Go beyond correctness—model system performance in FizzBee. Analyze response latency, throughput, error rates, resource utilization, and scalability using probabilistic techniques.
- [Whiteboard Visualizations](https://fizzbee.io/design/tutorials/visualizations/index.md): Automatically generate sequence diagrams, state diagrams, and algorithm animations from simple pseudo code. Explore every state and transition interactively, ensuring your algorithms meet all requirements with zero extra effort.
- [Current Limitations](https://fizzbee.io/design/tutorials/limitations/index.md): Current limitations of the FizzBee language and model checker — know what to expect from this fast-improving formal methods tool.
- [Design Verification](https://fizzbee.io/design/index.md): Learn FizzBee, a Python-like language for formal specification and model checking. Explore tutorials, worked examples, and guides to verifying distributed systems.

## Examples

- [Examples](https://fizzbee.io/design/examples/index.md): Two-phase commit, Raft, Dijkstra's token ring and classic algorithms, explained step by step with runnable models, failure traces and diagrams.
- [Cycle Detection in Linked List](https://fizzbee.io/design/examples/linked_list_cycle/index.md): Floyd's tortoise-and-hare and a visited-set approach to linked-list cycle detection, written as runnable pseudocode and checked exhaustively on small lists.
- [Die Hard](https://fizzbee.io/design/examples/die-hard/index.md): Can you measure exactly 4 litres with a 3-litre and a 5-litre jug? Explore every possible state and see the sequence of pours that solves the Die Hard puzzle.
- [EWD426 Token Ring](https://fizzbee.io/design/examples/ewd426-token-ring/index.md): Can a token ring recover from any state? Dijkstra's EWD426 self-stabilizing algorithm explained, including why it needs fairness and when it is guaranteed to stabilize.
- [Two Phase Commit](https://fizzbee.io/design/examples/two_phase_commit/index.md): Two-phase commit explained step by step: how participants vote and the coordinator decides, why failures make it hard, and the invariants that keep transactions atomic.
- [Two Phase Commit (Procedural)](https://fizzbee.io/design/examples/two_phase_commit_procedural/index.md): Two-phase commit written as plain procedural code, with yield points, parallel steps and message passing, and every interleaving checked for atomicity.
- [Two Phase Commit (Actor model/Object oriented)](https://fizzbee.io/design/examples/two_phase_commit_actors/index.md): Build two-phase commit from scratch with roles and RPCs, then add timeouts and watch plausible fixes fail one by one until one works, with sequence diagrams.
- [Raft Consensus Protocol - FizzBee Specification for Reasoning](https://fizzbee.io/design/examples/raft-algorithm-reasoning-spec/index.md): Derive Raft from first principles: start with a whiteboard-level model and let the model checker's counterexamples show why each rule is needed.
- [Raft Consensus Protocol](https://fizzbee.io/design/examples/raft-consensus-algorithm/index.md): Model the Raft consensus protocol step by step: leader election, log replication, RPCs and timeouts, then model-check election safety and log matching.
- [Knuth-Yao Sampling Algorithm for Random Variate Generation](https://fizzbee.io/design/examples/knuth-yao-sampling-algorithm/index.md): The Knuth–Yao algorithm explained: generate any distribution from fair coin flips optimally — two dice take 4.39 flips on average instead of 7.33.
- [Time oblivious Sampling Algorithm for Random Variate Generation](https://fizzbee.io/design/examples/time-oblivious-sampling-algorithm/index.md): A sampling algorithm whose running time reveals nothing about its output: generate random variates resistant to timing attacks, and compare its cost with Knuth–Yao.

## Model-Based Testing

- [Getting Started](https://fizzbee.io/testing/tutorials/getting-started/index.md): How FizzBee model-based testing works: write a model of your system's behavior, connect it to your code with an adapter, and run autonomous, reproducible tests.
- [Quick Start](https://fizzbee.io/testing/tutorials/quick-start/index.md): TDD without writing tests: model a Go counter in FizzBee, implement the adapter, and let the test runner drive single-threaded, concurrent, and database tests.
- [Model-Based Testing](https://fizzbee.io/testing/index.md): Test that your code matches your intent, not just hope AI-written tests cover enough. Model-based testing for business logic, APIs, databases, and web UIs.
- [Upcoming Features](https://fizzbee.io/testing/tutorials/work-in-progress/index.md): These are the features not yet implemented, and some work in progress.
- [White box testing - State assertion](https://fizzbee.io/testing/tutorials/white-box-testing-state-assertion/index.md): White-box model-based testing: state assertions find bugs faster and flag the exact step where internal state goes wrong. Fix bugs instead of hunting for them.

## Optional

- [News](https://fizzbee.io/posts/index.md): Articles on formal methods and distributed systems design: finding real design bugs with model checking, explained for working developers.
- [Introducing FizzBee: Simplifying Formal Methods for All](https://fizzbee.io/posts/formal-methods-wire-transfer/index.md): A wire transfer that debits Alice but never credits Bob: how a model checker finds this concurrency bug, and why formal methods are worth learning.
- [Publish algorithms with testable code](https://fizzbee.io/posts/pseudocode-modelchecking/index.md): Publish algorithms as precise pseudocode you can actually run and test: a Python-like alternative to TLA+ and PlusCal for specifying and model checking.