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:
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.
meoleo 50 minutes ago [-]
I am not sure if I understand clearly why Kiro's approach would not find the issue.
jayaprabhakar 28 seconds ago [-]
I'll add a detailed article explaining the difference.
ActionHank 4 hours ago [-]
Ok, so the proposed answer here is to define the spec in what is essentially code for another LLM to then interpret into different code?
I'm not sure if this does much more than a grillme skill and then poking an agent to do the work.
jayaprabhakar 2 hours ago [-]
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.
whattheheckheck 2 hours ago [-]
Sell consultancy services to build software better faster or cheaper!
Bpmn, tla+, event-b, P and ModP are all likely contenders to jump in popularity and mainstream swe worlds
pbronez 1 hours ago [-]
The related https://fizzbee.ai/ tool is pretty neat. It's similar to /grillme but with additional formalism. Not sure if the resulting specs are definitively better, if only because the FizzBee code is harder for me to decipher.
jayaprabhakar 53 minutes ago [-]
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.
jackdaniels4me 12 hours ago [-]
Today, most coding agents support spec-driven development (or plan mode).
They typically capture the requirements, design, and implementation plan in Markdown files. But is that Markdown file actually a specification?
This article explores how formal analysis can uncover requirements gaps that are easy to miss.
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.
I'm not sure if this does much more than a grillme skill and then poking an agent to do the work.
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.
Bpmn, tla+, event-b, P and ModP are all likely contenders to jump in popularity and mainstream swe worlds
They typically capture the requirements, design, and implementation plan in Markdown files. But is that Markdown file actually a specification?
This article explores how formal analysis can uncover requirements gaps that are easy to miss.