GitHub: <a href="https://www.github.com/fizzbee-io/FizzBee">https://www.github.com/fizzbee-io/FizzBee</a><p>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.<p>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.<p>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.<p>I've also created an online playground so you can try it without having to install on your machine.<p>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)<p>Please let me know your feedback.
Url: <a href="https://FizzBee.io" rel="nofollow">https://FizzBee.io</a>
Git: <a href="https://www.github.com/fizzbee-io/FizzBee">https://www.github.com/fizzbee-io/FizzBee</a>
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.
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?
How does FizzBee compare to other formal methods tools for Python like Nagini, Deal-solver, Dafny? <a href="https://news.ycombinator.com/item?id=39139198">https://news.ycombinator.com/item?id=39139198</a><p><a href="https://news.ycombinator.com/item?id=36504073">https://news.ycombinator.com/item?id=36504073</a> :<p>>>> <i>Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ [or FizzBee] help with that at all?</i>
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
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).<p><a href="https://jon-jacky.github.io/PyModel/www/" rel="nofollow">https://jon-jacky.github.io/PyModel/www/</a><p><a href="https://github.com/jon-jacky/PyModel/">https://github.com/jon-jacky/PyModel/</a><p>The PyModel in that repository is written in Python 2 and has not been
maintained for more than ten years.<p>This fork is in Python 3 and was last revised two years ago:<p><a href="https://github.com/zlorb/PyModel">https://github.com/zlorb/PyModel</a><p>The best description of PyModel is the talk at SciPy 2011:<p>Slides: <a href="https://jon-jacky.github.io/PyModel/talks/pymodel-nwpd10.pdf" rel="nofollow">https://jon-jacky.github.io/PyModel/talks/pymodel-nwpd10.pdf</a><p>Paper: <a href="https://jon-jacky.github.io/PyModel/talks/pymodel-scipy2011.pdf" rel="nofollow">https://jon-jacky.github.io/PyModel/talks/pymodel-scipy2011....</a><p>PyModel's model checking is explained on p. 3 in the paper in the sections titled <i>Analysis</i> and <i>Safety and Liveness</i>.
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.
Does this generate executables like Dafny? Or is it more like TLA+ and focused on checking designs?<p>What’s it using on the backend for checking predicates?
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?