jayaprabhakar

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