from Hacker News

Show HN: FizzBee – Formal methods in Python

by jayaprabhakar on 4/2/24, 10:45 AM with 23 comments

GitHub: https://www.github.com/fizzbee-io/FizzBee

Traditionally, formal methods are used only for highly mission critical systems to validate the software will work as expected before it's built. Recently, every major cloud vendor like AWS, Azure, Mongo DB, confluent, elastic and so on use formal methods to validate their design like the replication algorithm or various protocols doesn't have a design bug. I used TLA+ for billing and usage based metering applications.

However, the current formal methods solutions like TLA+, Alloy or P and so on are incredibly complex to learn and use, that even in these companies only a few actually use.

Now, instead of using an unfamiliar complicated language, I built formal methods model checker that just uses Python. That way, any software engineer can quickly get started and use.

I've also created an online playground so you can try it without having to install on your machine.

In addition to model checking like TLA+/PlusCal, Alloy, etc, FizzBee also has performance and probabilistic model checking that be few other formal methods tool does. (PRISM for example, but it's language is even more complicated to use)

Please let me know your feedback. Url: https://FizzBee.io Git: https://www.github.com/fizzbee-io/FizzBee

  • by johndough on 4/5/24, 5:01 AM

    I was looking for Python code, but did not find anything, until I realized that it said "Python-like" instead of "Python" on the website. I'd suggest to change the title to reflect that. I did not recognize the *.fizz files as Python.

  • by pkoird on 4/4/24, 11:32 PM

    This is super cool! As someone who is interested but unfamiliar with formal verification, how "powerful" or "complete" would you say FizzBee is compared to the conventional tools such as TLA+? I'm unsure if I framed this correctly but can you do everything in Fizzbee that TLA+ supports?

  • by westurner on 4/5/24, 4:46 AM

    How does FizzBee compare to other formal methods tools for Python like Nagini, Deal-solver, Dafny? https://news.ycombinator.com/item?id=39139198

    https://news.ycombinator.com/item?id=36504073 :

    >>> Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ [or FizzBee] help with that at all?

  • by hnhn34 on 4/15/24, 12:43 PM

    Would it be a dumb idea to use Fizzbee (or any formal methods language) for non-trivial programs in general, not just distributed systems? I wonder if it would be useful for specifying bevahiors in, say, game development for example

  • by jonjacky on 4/6/24, 7:45 PM

    Possibly pertinent: PyModel, a modelling system and model checker in and for Python --- the models are coded in standard Python. In addition to analysis, the system can be used as a test case generator and test runner for offline testing and "on the fly" testing (where a long-running test case is generated as the test executes).

    https://jon-jacky.github.io/PyModel/www/

    https://github.com/jon-jacky/PyModel/

    The PyModel in that repository is written in Python 2 and has not been maintained for more than ten years.

    This fork is in Python 3 and was last revised two years ago:

    https://github.com/zlorb/PyModel

    The best description of PyModel is the talk at SciPy 2011:

    Slides: https://jon-jacky.github.io/PyModel/talks/pymodel-nwpd10.pdf

    Paper: https://jon-jacky.github.io/PyModel/talks/pymodel-scipy2011....

    PyModel's model checking is explained on p. 3 in the paper in the sections titled Analysis and Safety and Liveness.

  • by atomicnature on 4/5/24, 12:19 PM

    I think one of Lamport's arguments was that at specification level one shouldn't go for an imperative approach. Imperative is good for "how to" instructions (programs). Declarative is good for "what is" or "what should be" instructions (specifications). So in that sense TLA+ was about helping you build state machines via simple declarative syntax. Of course this was Lamport's argument, in practice, your approach may work just as well. Will definitely be interested to see how your approach evolves.

  • by User23 on 4/4/24, 11:48 PM

    Does this generate executables like Dafny? Or is it more like TLA+ and focused on checking designs?

    What’s it using on the backend for checking predicates?

  • by erezsh on 4/5/24, 8:53 PM

    I like the idea of being able to use this in a real program, but I'm not sure how that would look. I browsed the docs, and I didn't see it addressed. I guess the question boils down to - how would it interface with other languages? On its own, it can't be used for general programming, so the only option I can think of is to run it as a DSL interface to a general programming language. Probably Python, since it's the easiest in this case. But it's not obvious to me what that API would look like, or what would be the right way to use it. Do you have any thoughts on this subject?

  • by sriram_malhar on 4/5/24, 3:56 AM

    This looks fantastic. Can't wait to translate some non-trivial TLA+ to test it out.

  • by rsrsrs86 on 4/5/24, 11:46 PM

    Alloy is much simpler than TLA+.

    Is fizzbee a frontend to TLA+?

  • by knowsuchagency on 4/4/24, 11:22 PM

    Very cool