Using Python syntax makes it more accessible.
Thanks. Please give it a try, and let me know if you have any issues. I'd be happy to help.
Readit Newsjayaprabhakar commented on Show HN: FizzBee – Formal Model based autonomous testing fizzbee.io/testing/... · Posted by u/jayaprabhakar
jayaprabhakar commented on Show HN: FizzBee – Formal Model based autonomous testing fizzbee.io/testing/... · Posted by u/jayaprabhakar
This is neat. I've used FizzBee and TLA+ for model checking. Being able to test the implementation would be nice.
How is this different from test case generation in TLA+?
Glad you have tried FizzBee before. Do you have any feedback on it?
With TLA+, I mostly see papers and example projects that typically implement model based trace checking solutions in TLA+.
While it works, usually, it will clutter the main code (SUT) with tracing library calls. And in some papers, you'll need to create a separate modified version of spec with the tracing spec.
MongoDB published a paper a while ago comparing model based testing and model based trace checking. I'll soon list more details.
Microsoft backed this $1.5 billion AI startup that was just discovered to be 700 engineers pretending to be AI
jayaprabhakar commented on Formal Methods: Just Good Engineering Practice? (2024) brooker.co.za/blog/2024/0... · Posted by u/aiono
One issue with the current proponents of formal methods is, they want to claim others who don't use formal methods as "lazy" or "dumb" and want to claim their superiority because they "do the right thing" and "mastered a complex language".
Some of them (not all, I know a few good ones) are, actually one trick pony. For example, ask them about other formal methods systems they learnt or tried in the recent years, they would claim they are "too busy" to learn anything new.
Recent easier to use formal methods: 1. FizzBee (Uses Python dialect, almost reads like pseudo code) 2. Quint: Another formal language with easier to use syntax 3. P: Use syntax similar to C# users.
The author of the posted article himself posted another article that Formal methods solves only half his problems (https://brooker.co.za/blog/2022/06/02/formal.html) But the problem he mentioned is actually solved by PRISM (It is not new). But Brooker just won'd bother to look around or learn.
jayaprabhakar commented on Formal Methods: Just Good Engineering Practice? (2024) brooker.co.za/blog/2024/0... · Posted by u/aiono
Modern formal methods like TLA+ and Alloy are as easy to pick up as Python, and other than having to write a spec (an ultra-simplified model of part of a system) they are completely automatic (based on model checkers). There is no reason for a modern software engineer not to have them on her radar. As a matter of fact most of the cloud systems you are using everyday have been verified with modern formal tools: Azure Cosmos DB, Dynamo DB, MongoDB, CockroachDB, ... and many others.
Have you tried FizzBee, it uses python dialect itself for specification?
jayaprabhakar commented on Formal Methods: Just Good Engineering Practice? (2024) brooker.co.za/blog/2024/0... · Posted by u/aiono
IMO formal software verification is still waaay too difficult to be worth it in all but the most extreme cases. That's really different to formal hardware verification where it is a no-brainer.
I keep trying to learn it, but you need to be a real expert. Like "I wrote the compiler" level expert for most systems.
For example I tried to prove a varint encoder/decoder. It worked for one or two bytes, but not more. Asking for help the reason was that the compiler internally only unrolls loops 5 times, or some random internal detail like that that you could never really hope to know.
I've been learning Lean recently, and ... I mean I like it, but if you learn it you're going to encounter documentation like this:
> Definitional equality includes η-equivalence of functions and single-constructor inductive types. That is, fun x => f x is definitionally equal to f, and S.mk x.f1 x.f2 is definitionally equal to x, if S is a structure with fields f1 and f2. It also features proof irrelevance, so any two proofs of the same proposition are definitionally equal. It is reflexive, symmetric, and a congruence.
And that's not really a knock on Lean - it seems to have some of the better documentation out of the alternatives.
Have you tried FizzBee.io? It has a python-like syntax. Take a look at the example.
https://fizzbee.io/examples/two_phase_commit_actors/#complet...
Formal methods don't have to be complex. The issue is, most formal methods are designed as an academic exercise to demonstrate a specific topic the professor was interested in. (Or TLA+, that was designed specifically for writing papers)
This is neat! How does this compare with tools like draw.io or mermaidjs
Those are pure drawing tools.
*Tools like draw.io, Lucidchart, and Excalidraw excel at creating raw diagrams through drag-and-drop interfaces. However, they often become cumbersome when updates are needed, and their outputs are rarely stored in source control, making versioning and collaboration more difficult. While these tools give you full control over the layout and appearance of the diagrams, they require manual effort each time you make changes.
*Mermaid.js, websequencediagrams, and PlantUML, on the other hand, allow you to generate diagrams from a text description. FizzBee builds on this concept by generating these text descriptions directly from your algorithm specification, then leveraging mermaid.js to render sequence diagrams and Graphviz for other diagram types.
*Where FizzBee truly shines is in its ability to automatically generate diagrams for every significant scenario your system might encounter, not just a single use case. For example, with a two-phase commit protocol:
- The 'happy path' where all participants and the coordinator agree to commit, and everything proceeds smoothly.
- A case where the first participant prepares, but the second one aborts.
- Scenarios where both participants prepare but some messages get dropped.
- A situation where both participants prepare, but the coordinator crashes and restarts—how does the system recover?
These are just a few examples. The ability to generate these scenarios automatically means FizzBee pays for itself very quickly compared to manually drawing sequence diagrams for each possible case.
This is in addition to verifying for correctness or clearer communication benefits.
https://fizzbee.io/testing/tutorials/quick-start/#parallel-t...
Sequential logic is generally easier to test (also concurrency testing of linearizable systems). FizzBee specification language is created primarily to express concurrent behavior of non-linearizable systems - like eventual consistency, etc.