HN Explorer

Show HN: FizzBee – Formal methods in Python (fizzbee.io)

119 points by jayaprabhakar ↗ HN
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

24 comments

[ 4.4 ms ] story [ 72.0 ms ] thread
pkoird
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?
jayaprabhakar
Yes, that's the intended goal. To do everything tla+ does (behavioral modeling) but not stop there. The second biggest area that's missing in tla+ but indispensable is performance modeling that will be integrated. (PRISM model checker does it, but with a unwieldy complex language not suitable for more than a few dozen states) The performance modeling is work in progress, you can still try it, but you need to download and use the command line tool at present.

The third goal is to make it suitable as a design documentation tool. I haven't started, but I would love to share the plan to get early feedback.

User23
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?

jayaprabhakar
No, there's no code generation. In that sense, it's more like TLA+.

The code generation is not in the plan, at least, not for the next couple of years until a few prerequisites happen that's not in my control.

The primary reasons for not taking code generation are, 1. It complicates the model spec. My intention is, the spec should be as close to pseudo code as possible that is you ever write pseudo code on your design doc, it should be in fizz. 2. The past experience trying to do complete code generation all failed except for some trivial use cases (like protocol buffers)

-- For the last question, for evaluating expressions, FizzBee uses starlark go library (subset of Python).

[deleted]
(comment deleted)
sriram_malhar
This looks fantastic. Can't wait to translate some non-trivial TLA+ to test it out.
jayaprabhakar
Thank you. Please let me know how it goes. Also, I can work with you on modeling it if you need - I'll want to see where the language design is causing the issue
hwayne
I'd also love to see what comes of this!
westurner
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?

jayaprabhakar
FizzBee is an alternative to TLA+ designed to be the easiest to get started for every software engineer. To make it easiest to use, the language of specification is Python instead of using some kind of mathematical presentation language like TLA+. So it's a formal methods in Python not for Python.

FizzBee is a design specification language whereas Nagini and deal solver are implementation verification language. FizzBee is supposed to be before you start coding, or actually before sending out the design document for review to iron out design bugs. The latter two are supposed to be used to verify the implementation.

Dafny is actually an implementation language designed as verification aware programming language. It does code generation into multiple languages and inserts various preconditions and other assertions into the code. Again, it is suitable for verifying the design.

westurner
Is it advantageous to maintain separation between formal design, formal implementation, and formal verification formal methods?

Is there still a place for implementation language agnostic tools for formal methods?

icontract and pycontracts do runtime type checking and value constraints with DbC Design-by-Contract patterns that more clearly separate the preconditions and postconditions from the command, per Hoare logic. Both can read Python type annotations and apply them at runtime or not, both support runtime checking of invariants: values that shouldn't have changed when postconditions are evaluated after the function returns, but could have due to e.g. parallelism and concurrency and (network I/O) latency and pass by reference in distributed systems.

jayaprabhakar
The single biggest advantage of keeping formal design separate from the forms implementation/verification is you check your design before the implementation starts.

Anything that operates by checking the implementation can find implementation bugs. Even if they find design bugs it's too late.

As an analogy. You can document the code with comments. Comments explaining why you do what you do. This along with the code can be reviewed and be part of the revision control.

That said, do you still recommend writing separate design documents? If so why? This will also answer your question on why we will need a design spec that's separate from the implementation

westurner
Having also written lots of code with nothing but Tests as the Functional Spec I'm not sufficiently familiar with Formal Methods, though I should make myself learn. TIL that there are different tools for Design/Implementation/Verification instead of just code and decorators and IDK annotations as decorators and autocorrect.

(TODO: link to post about university-level FM programs)

Always wondered whether there's some advantage to translating to another language's AST for static and/or dynamic analysis or not. AFAIU Fuzzing is still necessary even given Formal Implementation?

Python is Turing complete, but does [TLA,] need to be? Is there an in-Python syntax that can be expanded in place by tooling for pretty diffs; How much overlap between existing runtime check DbC decorators and these modeling primitives and feature extraction transforms should there be? (In order to: minimize cognitive overload for human review; sufficiently describe the domains, ranges, complexity costs, inconstant timings, and the necessary and also the possible outcomes given concurrency,)

"FaCT: A DSL for Timing-Sensitive Computation" and side channels https://news.ycombinator.com/item?id=38527663

johndough
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.
jayaprabhakar
I agree, the body of the action and functions are Python, actually starlark (a subset of python). I'll update the description.
atomicnature
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.
jayaprabhakar
This kind of argument aren't new to formal methods. They have been present ever since high level programming language came to existence. Functional programming proponents have always argued how great functional languages are and how natural they are and how elegant their programs look. However, what really matters is what gets the work done.

From my understanding of the history of programming, people will always resort to multi-paradigm solutions. For programming, they will use objects oriented concepts, sprinkle with imperative code within their classes, occasionally use functional programming when that is actually elegant.

Despite that, TLA+ ended up having PlusCal which is almost an imperative style (not actually imperative) language.

erezsh
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?
jayaprabhakar
I don't know which part of the description have the impression that this could be used by itself in a real program. I'll update if the description either here or in the website had an incorrect statement.

FizzBee's goal is to be a specification language that happens before the implementation starts.

rsrsrs86
Alloy is much simpler than TLA+.

Is fizzbee a frontend to TLA+?

jayaprabhakar
FizzBee is a totally new implementation of the model checker. It does not cross compile to TLA+. That said, FizzBee is also modeled after and totally inspired by TLA+.
jonjacky
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.

hnhn34
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