FizzBee – Design Reliable, Scalable Distributed Systems

Analyze & Visualize Your Design

Specify your system design as code.
FizzBee automatically:
- Generates sequence & block diagrams
- Checks for behavioral correctness
- Analyzes performance metrics

Generate & Run Tests

Specify how the design maps to your code.
FizzBee automatically:
- Exhaustively tests every behavior
- Simulates faults and edge cases
- Validates concurrency and integration

What Engineers Are Saying

"FizzBee upholds the rigor of TLA+ while making formal verification simpler and more accessible for engineers. By leveraging Python, it reduces the learning curve, with the potential to surpass TLA+ as the go-to tool for engineers."

— Jack Vanlightly, Principal Technologist, Confluent

"I discovered FizzBee while designing the manifest for SlateDB, an embedded key-value store. FizzBee’s concepts were easy to grasp in hours, and by the next day, I had a working spec that uncovered a real concurrency bug!"

— Vignesh Chandramohan, Engineering Manager, Doordash

"FizzBee’s Python-like syntax made it easy to learn and use, unlike other formal methods languages. I picked it up over a weekend and successfully modeled our streaming ingestion platform to identify correctness bugs. It's intuitive and incredibly effective!"

— Franklyn D'souza
Staff Software Developer, Shopify

"FizzBee cured my fear of formal methods after struggling with TLA+ years ago. It's surprisingly easy to learn and a refreshing experience—something I never thought I could master. Universities should teach FizzBee!"

— Li Yazhou
Tech Lead, Cloud Platform, Databend

Why Model Your System?

Try Fizz

Read the quick start guide to learn how to write your first FizzBee model or comb through the examples or tinker with the FizzBee online playground

An example: Travel Booking Service using Two Phase Commit

Run in playground

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67


---
deadlock_detection: false
---
"""
How does a travel booking service ensure that all components in the itinerary are
booked or nothing is booked? Using Two Phase Commit protocol.

Phase 1: The Coordinator (Booking Service) asks all participants (Airline, Hotel, Car Rental) to place a hold on
the resource.
Phase 2:
    a. If all the participants successfully placed a hold on the resource, 
        the Coordinator (Booking Service) asks all participants to commit the booking.
    b. If any of the participants fail to place a hold, 
        the Coordinator (Booking Service) asks all participants to abort the booking.

The core logic is in the Coordinator.Checkout action 
"""

role Participant:
  action Init:
      self.status = "init"
 
  func placehold():
      vote = any ["accepted", "aborted"]
      self.status = vote 
      return self.status
 
  func finalize(decision):
      self.status = decision


role Coordinator:
    action Init:
        self.status = "init"
 
    action Checkout:
        require(self.status == "init")
        self.status = "inprogress"
        for p in participants:
              vote = p.placehold()
              if vote == "aborted":
                  self.finalize("aborted")
                  return
 
        self.finalize("committed")
 
 
    func finalize(decision):
        self.status = decision
        for p in participants:
            p.finalize(decision)

 
NUM_PARTICIPANTS=2
 
action Init:
    coordinator = Coordinator()
    participants = []
    for i in range(NUM_PARTICIPANTS):
        participants.append(Participant())

always assertion ParticipantsConsistent:
  for p1 in participants:
    for p2 in participants:
      if p1.status == 'committed' and p2.status == 'aborted':
        return False
  return True