Introduction

FizzBee is a Python-like formal specification language for modeling distributed systems. It is based on Starlark (a Python subset) and provides explicit model checking with automatic fault injection capabilities.

Key Differentiators from TLA+

Python-like syntax: Easy to learn and read
Implicit fault injection: Automatic crash and message loss simulation
Non-atomic actions: Natural modeling of multi-step operations
Role-based modeling: Object-oriented approach to distributed actors

Language Foundation

FizzBee uses Starlark as its expression and statement engine:

Python-compatible syntax for expressions
Deterministic execution
No import statement and no arbitrary Python imports — a curated set of modules is auto-imported globally (see Standard Library)
Built-in support for common data structures