jayaprabhakar

This is a follow up to my previous post that finds requirements completeness issues. https://blog.fizzbee.ai/formal-analysis-in-requirements-spec...

Author here. FizzBee is a model checker I’ve been building, with the goal of bringing formal methods to mainstream software engineering.

In this article, I take a requirements specification for a simple CRUD app, and show how writing the spec in a formal language helps catch requuirements conflicts as the product evolves.

Feedback welcome.

I'll add a detailed article explaining the difference.

Thanks. Just curious, have you tried building the app using the generated spec with any coding agents? This is something I am trying to work on next.

The overlapping part of what FizzBee and Kiro is we formalize the requirements first and do formal analysis on them to identify various requirements issues.

However the technique is significantly different. Kiro's post says they use predicate logic. Whereas FizzBee uses Dynamic Logic. So, Kiro's approach cannot find many issues. Let us take the same example from the fizzbee blog. FizzBee found the issue as linked in the blog:

https://blog.fizzbee.ai/formal-analysis-in-requirements-spec...

But Kiro's approach would say, it is both consistent and complete. That is, R2 + R2b => R3 in this case.

-----

Another thing is testability. FizzBee's approach checks for testability without LLM deterministically. And it naturally produces extensive test cases, but with Kiro it doesn't. It needs more LLM use to convert them to test cases.

The difference is accuracy, cost, time and more importantly consistency.

In case you noticed, a year ago, LLMs could not reliably count the number of 'R's in strawberry. Now they all do well. Guess how? Instead of training LLMs to do this, it was easier for them to write a small python script and run that. That solved the problem once and for all.

The same thing here, instead of just using LLMs and keep grilling repeatedly, there is a higher chance of getting a workable solution quickly. The best part about formal methods here is, it is self validating. It checks in seconds, what would have taken hours or even days with LLM only flow.

Thanks a lot. It does handle concurrency.

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.

Thanks. Please give it a try, and let me know if you have any issues. I'd be happy to help.

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

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.

Have you tried FizzBee, it uses python dialect itself for specification?

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)

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.

TLA+ is 25 years old. Despite the power it's syntax is too alien to become mainstream. Have you considered https://FizzBee.io? Almost Python-like syntax, has more powerful semantics, beautiful visualizations with no extra work, only formal methods system that can do performance analysis.

Putin signed a decree that Russia would welcome foreigners wanting to escape Western liberal ideals. Applicants may include those from countries unaligned with "Russian spiritual and moral values." The application process has been simplified, and visas may be issued as soon as next month.

A principal researcher at Confluent explains Apache icebergs consistency model. Also shows the formal modeling using a Python'ish language FizzBee to find bugs.

https://FizzBee.io is not just a syntax transpiler, but a complete implementation. It uses starlark language (a Python variant) for specification. In addition to behavioral modeling like TLA+, Quint etc, it supports probabilistic and performance modeling. Generates state and sequence diagrams automatically.

This looks cool. The UI animation is good. Looking forward for more such games. A few minor feedbacks.

1. Even on phones, it leaves a lot of margin/padding, and the boxes are a bit too small. Can you make it a bit more responsive and use up the whole width of the screen (up to a max width of course) 2. Only the first and the last needs to be selected, and so slide doesn't work. 3. A minor confusion in the UI, that I'm not sure if the equation can span across multiple lines?

When publishing algorithms for others' consumption either for a paper or blog, please post the source code.

This post is a follow up of https://ahelwer.ca/post/2023-03-30-pseudocode/

Where Andrew pointed compared executable Python code vs executable model checker PlusCal.

In this blog, I'm showing how to model check Python code with minor changes.

For the curious, model checking is the formal methods technique that explores every possible path to ensure the invariants are met in every case.