iiinova — where your digital self keeps evolving

Reposted by @jayaprabhakar.bsky.social

Zicklag @zicklag.dev · 24/03/2026

This touches on something that FizzBee helps a lot with compared to pure TLA+. It makes it very easy to write the spec similarly to pseudo-code while experiencing the failures associated with real async code. muratbuffalo.blogspot.com/2026/03/mode...

This brings us to an important lesson about formal verification and system design: the paradigm gap. Pure TLA+ is a beautiful event-driven way to describe the mathematically correct state of your system. However, the environments where these systems actually live (Java, Go, C++, or Rust) are fundamentally built around sequential threads, loops, and queues, just like our PlusCal model. The impedance mismatch between an event-driven specification and a sequential implementation introduces the risk of HOL blocking. Because modern programming languages make it so effortless to pause a thread and wait for a resource, it is incredibly easy for a system to fall into the blocking trap. We should be cognizant of this pitfall when implementing our designs.

012

jayaprabhakar.bsky.social @jayaprabhakar.bsky.social · 11/12/2025

@pierrezemb.fr Looking forward to hear more about what you modeled and your thoughts about it.

010

Reposted by @jayaprabhakar.bsky.social

Tech on the Rocks @totrrocks.bsky.social · 19/05/2025

Formal verification tools like TLA+, FizzBee, and Antithesis serve different stages: design-level verification versus implementation-level testing. Jayaprabhakar(JP) Kadarkarai on Formal Methods & Verification from ep.5

021

jayaprabhakar.bsky.social @jayaprabhakar.bsky.social · 03/05/2025

@hillelwayne.com FizzBee does exactly this. At present only supports Go. github.com/slatedb/slat... It started with the idea from @emptysqua.re's paper "Extreme modeling in practice" but making it easier to use. In addition to that FizzBee also tests concurrency that's not typically covered.

github.com

Issues · slatedb/slatedb-go

A cloud native embedded storage engine built on object storage. - Issues · slatedb/slatedb-go

010

jayaprabhakar.bsky.social @jayaprabhakar.bsky.social · 14/03/2025

FizzBee automatically tests with various fault injection. Node crash is one of them. fizzbee.io/tutorials/fa... To mark some fields as ephemeral, you just need to add an annotation `@state(ephemeral=["inmem_field1", "inmem_field2"])`. I'd be happy to assist.

fizzbee.io

Implicit Fault Injection

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 resili...

010

Reposted by @jayaprabhakar.bsky.social

Shadaj Laddad @shadaj.me · 13/02/2025

The SF Systems Meetup is back! On 2/27, we're excited to have headline talks from the creator of FizzBee and a research collaborator with Signal. This is going to be a super fun night diving deep into making distributed protocols work, hope you'll join us! lu.ma/vqjf30k3

lu.ma

SF Systems Meetup: Correctness and Security for Distributed Systems · Luma

The SF Systems Meetup is back for the new year! This meetup, our theme is correctness and security. It's easy to write a distributed protocol, but very hard to…

053

jayaprabhakar.bsky.social @jayaprabhakar.bsky.social · 07/02/2025

I really thought you were talking about 1:30 am until I got to the end...

010

jayaprabhakar.bsky.social @jayaprabhakar.bsky.social · 30/12/2024

That would be awesome. I'd be happy to answer any questions about FizzBee.

000