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.

TLA+ is growing adoption. Most modern cloud vendor uses TLA+ (AWS, Azure, Mongo, Redis, Elastic, and a lot more). I see a lot of usage in crypto world.

Note: I am the developer of https://fizzbee.io a formal specification system using Pythonish language. If you are just getting started on formal methods, FizzBee would be the easiest to learn.

I'm the developer of FizzBee. Thanks for sharing here. I just noticed it even searching for my own post on this.

I hope you tried FizzBee and I love any feedback

The single biggest advantage of keeping formal design separate from the forms implementation/verification is you check your design before the implementation starts.

Anything that operates by checking the implementation can find implementation bugs. Even if they find design bugs it's too late.

As an analogy. You can document the code with comments. Comments explaining why you do what you do. This along with the code can be reviewed and be part of the revision control.

That said, do you still recommend writing separate design documents? If so why? This will also answer your question on why we will need a design spec that's separate from the implementation

This kind of argument aren't new to formal methods. They have been present ever since high level programming language came to existence. Functional programming proponents have always argued how great functional languages are and how natural they are and how elegant their programs look. However, what really matters is what gets the work done.

From my understanding of the history of programming, people will always resort to multi-paradigm solutions. For programming, they will use objects oriented concepts, sprinkle with imperative code within their classes, occasionally use functional programming when that is actually elegant.

Despite that, TLA+ ended up having PlusCal which is almost an imperative style (not actually imperative) language.

FizzBee is a totally new implementation of the model checker. It does not cross compile to TLA+. That said, FizzBee is also modeled after and totally inspired by TLA+.

I don't know which part of the description have the impression that this could be used by itself in a real program. I'll update if the description either here or in the website had an incorrect statement.

FizzBee's goal is to be a specification language that happens before the implementation starts.

FizzBee is an alternative to TLA+ designed to be the easiest to get started for every software engineer. To make it easiest to use, the language of specification is Python instead of using some kind of mathematical presentation language like TLA+. So it's a formal methods in Python not for Python.

FizzBee is a design specification language whereas Nagini and deal solver are implementation verification language. FizzBee is supposed to be before you start coding, or actually before sending out the design document for review to iron out design bugs. The latter two are supposed to be used to verify the implementation.

Dafny is actually an implementation language designed as verification aware programming language. It does code generation into multiple languages and inserts various preconditions and other assertions into the code. Again, it is suitable for verifying the design.

Thank you. Please let me know how it goes. Also, I can work with you on modeling it if you need - I'll want to see where the language design is causing the issue

No, there's no code generation. In that sense, it's more like TLA+.

The code generation is not in the plan, at least, not for the next couple of years until a few prerequisites happen that's not in my control.

The primary reasons for not taking code generation are, 1. It complicates the model spec. My intention is, the spec should be as close to pseudo code as possible that is you ever write pseudo code on your design doc, it should be in fizz. 2. The past experience trying to do complete code generation all failed except for some trivial use cases (like protocol buffers)

-- For the last question, for evaluating expressions, FizzBee uses starlark go library (subset of Python).

Yes, that's the intended goal. To do everything tla+ does (behavioral modeling) but not stop there. The second biggest area that's missing in tla+ but indispensable is performance modeling that will be integrated. (PRISM model checker does it, but with a unwieldy complex language not suitable for more than a few dozen states) The performance modeling is work in progress, you can still try it, but you need to download and use the command line tool at present.

The third goal is to make it suitable as a design documentation tool. I haven't started, but I would love to share the plan to get early feedback.