Find bugs before you code

FizzBee is a formal specification language and model checker to specify distributed systems.

Exhaustive model checking

Explore all possible behaviors and exhaustive set of complex interactions and verify the system does what you think it does.

Easiest specification language

FizzBee uses Python-like language, using imperative style. You can be productive in minutes.

Performance modeling

FizzBee comes with probabilistic model checker for modeling performance characteristics like expected of latency, throughput, availability SLAs.

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

Run in playground

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17


# Fizzbee model checker

invariants:
  always value <= 3  # This statement is always true
  always eventually value == 0  # The value can be anything, but always come back to 0
  eventually always value >= 0  # The value will reach 0 eventually, and stay >= 0


action Init:
  value = -2


atomic fair action Add:
  if value < 3:
      value += 1
  else:
      value = 0