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.