From 435ebf6474bf705d95295dd366cf333685d8e867 Mon Sep 17 00:00:00 2001 From: Chris Riccomini Date: Mon, 4 May 2026 17:38:39 -0700 Subject: [PATCH 01/92] Add AGENTS.md --- AGENTS.md | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 AGENTS.md diff --git a/AGENTS.md b/AGENTS.md new file mode 100644 index 0000000..ab9beac --- /dev/null +++ b/AGENTS.md @@ -0,0 +1,3 @@ +- Commit after each change. +- Use conventional commit syntax. Include a pargraph in the commit message dsecribing in detail what you did. +- Always use Playwright to check your changes. From 454dd3bb278afd2a554ff71bf481fdee3d1b1b64 Mon Sep 17 00:00:00 2001 From: Chris Riccomini Date: Mon, 4 May 2026 18:12:22 -0700 Subject: [PATCH 02/92] feat: refresh FizzBee website design Redesign the homepage around a full-bleed product-oriented hero, a clearer modeling workflow, refreshed proof and testimonial sections, and a stronger final CTA while preserving the original FizzBee positioning around modeling, visualization, validation, and tests. The change also adds a local Geekdoc header override to remove the dark-mode toggle, introduces persistent top navigation links, consolidates font loading, moves consent banner styling into the shared stylesheet, and updates the global light theme so docs pages inherit the new typography, spacing, colors, and code treatment. --- content/_index.md | 269 ++++---- hugo.toml | 1 + layouts/index.html | 5 + layouts/partials/consent.html | 33 - layouts/partials/head/custom.html | 5 +- layouts/partials/site-header.html | 79 +++ static/custom.css | 1000 ++++++++++++++++++++++++++--- 7 files changed, 1135 insertions(+), 257 deletions(-) create mode 100644 layouts/index.html create mode 100644 layouts/partials/site-header.html diff --git a/content/_index.md b/content/_index.md index ada9ed9..f01783d 100644 --- a/content/_index.md +++ b/content/_index.md @@ -1,148 +1,147 @@ --- -Title: FizzBee – Design Reliable, Scalable Distributed Systems -Description: Designing a distributed system? FizzBee makes it easy to model, visualize, and - validate your design—catching flaws before you code. The easiest-ever formal methods, - built for developers. -#geekdocNav: false -geekdocAlign: center +Title: FizzBee - Design Reliable Distributed Systems +Description: FizzBee helps engineers model, visualize, validate, and test distributed system designs before implementation. +geekdocNav: false +geekdocAlign: left geekdocAnchor: false geekdocBreadcrumb: false --- - -{{< columns >}} - -### 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 - -{{< /columns >}} - -{{% rawhtml %}} - -
-

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 +{{< rawhtml >}} +
+
+
+
+
+ + FizzBee
-
-

"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 +

Design distributed systems you can test before you build.

+

Write a compact, Python-like model. FizzBee explores the behaviors, draws the diagrams, and turns the same design into tests.

+
+ Start modeling + Open playground
-
-

"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 +
+ +
+
+ + travel_booking.fizz
-
-

"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 +
+ 
role Coordinator:
+  action Checkout:
+    for p in participants:
+      vote = p.placehold()
+      if vote == "aborted":
+        self.finalize("aborted")
+        return
+    self.finalize("committed")
+
+always assertion Consistent:
+  return not mixed_decisions()
+
+
+ + Model check passed +
+

1,248 states explored across failures, retries, and interleavings.

+
+
-
-{{% /rawhtml %}} - -## Why Model Your System? - -{{< figure src="https://storage.googleapis.com/fizzbee-public/website/homepage/what_fizzbee_does_graph.png" alt="Why Model Your System" caption="Modeling helps you explore edge cases, eliminate ambiguity, catch bugs early, and iterate with confidence. In addition to validating the design, you can verify the implementation" >}} - - -## Try Fizz - -Read the [quick start guide](/design/tutorials/getting-started/) to learn how to write your first FizzBee model -or comb through the [examples](/design/examples/) -or tinker with the [FizzBee online playground](/play) - -### An example: Travel Booking Service using Two Phase Commit - -{{% fizzbee %}} ---- -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 +
-{{% /fizzbee %}} +
+
+

One model, multiple payoffs

+

Turn a design sketch into executable evidence.

+
+
+
+ 01 +

Specify

+

Model actors, actions, faults, and invariants in readable code.

+
+
+ 02 +

Explore

+

Generate sequence diagrams, state views, counterexamples, and performance signals.

+
+
+ 03 +

Test

+

Map the model to real code and exercise every behavior the design allows.

+
+
+
+ +
+
+

Why model first

+

Distributed bugs hide in the schedules people do not write down.

+

FizzBee makes the schedules explicit. It checks behavioral correctness, exposes edge cases, and gives teams diagrams they can review together.

+ Browse examples +
+
+
+ client + Checkout + request received +
+
+ coordinator + PlaceHold + 2 participants +
+
+ participant + Abort + counterexample avoided +
+
+ test + Replay + implementation verified +
+
+
+
+
+

Used by engineers designing real systems

+

Formal methods without the ceremony.

+
+
+
+
FizzBee upholds the rigor of TLA+ while making formal verification simpler and more accessible for engineers.
+
Jack Vanlightly, Principal Technologist, Confluent
+
+
+
By the next day, I had a working spec that uncovered a real concurrency bug.
+
Vignesh Chandramohan, Engineering Manager, DoorDash
+
+
+
The Python-like syntax made it easy to learn and use, unlike other formal methods languages.
+
Franklyn D'souza, Staff Software Developer, Shopify
+
+
+
FizzBee cured my fear of formal methods after struggling with TLA+ years ago.
+
Li Yazhou, Tech Lead, Cloud Platform, Databend
+
+
+
+
+
+

Try FizzBee

+

Start with a model small enough to review and strong enough to break assumptions.

+
+
+ Read the quick start + Use the playground +
+
+ +{{< /rawhtml >}} diff --git a/hugo.toml b/hugo.toml index 7c8084f..3d37460 100644 --- a/hugo.toml +++ b/hugo.toml @@ -18,6 +18,7 @@ enableRobotsTXT = true geekdocLogo = "bee-left-to-right-512x512.png" geekdocPrivacyPolicy = "/privacy.html" geekdocTagsToMenu = false + geekdocDarkModeToggle = false # Needed for mermaid shortcodes [markup] diff --git a/layouts/index.html b/layouts/index.html new file mode 100644 index 0000000..dd209c2 --- /dev/null +++ b/layouts/index.html @@ -0,0 +1,5 @@ +{{ define "main" }} +
+ {{ partial "utils/content" . }} +
+{{ end }} diff --git a/layouts/partials/consent.html b/layouts/partials/consent.html index 63ec363..3f4f6df 100644 --- a/layouts/partials/consent.html +++ b/layouts/partials/consent.html @@ -1,36 +1,3 @@ -