[brianjlogan]

Are you familiar with FizzBee. I think formal methods is already very hot right not with more demand for proving AI generated code isn't garbage.

(Even if you're hand writing people are going to assume or suspect it's LLM gen.)

[tombert]

I am!

The author of FizzBee reached out to me about a year ago on LinkedIn actually, because I gave a talk on TLA+ a few years ago.

I haven't really played with it yet (outside of the few examples on their site) because I'm already pretty entrenched in the TLA+/PlusCal world, but it is very likely that FizzBee might be a better fit for software engineering circles; the incremental testing is pretty neat, to a point where I kind of want to steal the that and port it over to TLA+/TLC. Probabilistic testing seems pretty cool too.

If I were getting into Formal Methods today for the first time, I would almost certainly be using FizzBee and/or Alloy.

[brianjlogan]

I have knowledge of FM primarily from HackerNews posts about it.

As someone lacking your academic background in it could you give me some advice on a good starting point, or perhaps papers/materials that are absolutely unskippable/foundational to understanding it, maybe a good learning exercise for utilizing FM?

[tombert]

FizzBee is likely a good place to start, but since I have never really used it I'm afraid I can't recommend good resources for it.

------

If you're just getting started, I recommend checking out my former advisor's book: https://www.amazon.com/Software-Engineering-Mathematics-Sei/...

I found this book to be fairly easy to read through, and gives you a rundown of a lot of the notation and concepts that pretty much all formal methods systems require.

------

TLA+ is a decent enough language. I recommend going through Lamport's video series on it to start: https://lamport.azurewebsites.net/tla/learning.html

I don't know what aspect of Formal Methods that you want to focus on; most of what I've done is with distributed systems stuff, but TLA+ can and has been used for low level things like circuit modeling. I can't tell you where to learn about that.

I think Hillel Wayne's learntla website is pretty good to get a few more practical examples: https://learntla.com/. I actually thought his Practical TLA+ book was a bit better for that though: https://www.amazon.com/Practical-TLA-Planning-Driven-Develop...

Both of those resources are more PlusCal focused. PlusCal is a C/Pascal-like language that compiles to "raw" TLA+. A lot of people like it more, I go back and forth.

If you care more about the more theoretical aspects of TLA+, Ron Pressler's "TLA+ in Practice and Theory" blog series is great: https://pron.github.io/tlaplus

Additionally, I recommend looking for the papers by Stefan Merz. Here's a good one to start, but he has a bunch: https://members.loria.fr/Stephan.Merz/papers/tla+logic.pdf

------

If your goal is to model concurrent systems, getting an understanding of CSP is worth doing. I liked Roscoe's book on it: https://link.springer.com/book/10.1007/978-1-84882-258-0

If you go deep into that, I recommend looking at the extension "tock-CSP" that adds timing semantics.

-------

If you're interested in the most theoretical aspects of formal methods, the only one I've done with any kind of intimate detail is Isabelle.

Isabelle is much more of a "math proof" thing than a "computer science" proof thing, but there are plenty of computer science things for it too. If you want to get started with the Isabelle/HOL language, the Concrete Semantics book is the normal recommended starting point: http://concrete-semantics.org/

------

This is mostly my history, there are many other paths but I can't really speak to those with any confidence. Hope this helped!

ETA:

Just to add, while I did go to school later for formal methods, I actually started learning this stuff while I was still a dropout from my undergrad. I eventually got my bachelors and masters and then entered a PhD program, but for TLA+ in particular I was learning it without any completed education, so this stuff is definitely approachable even without a ton of letters after your name.

[brianjlogan]

Thank you so much for this quality reply!

I shared earlier in the thread about the learning app I'm working on. I already have a learning path created in it for Formal Methods. I will be taking each of your points and tracking my progress to completing them.

Just wanted you to know your effort won't be unappreciated.

[tombert]

Yep!

I have an email in my profile, feel free to contact me. Happy enough to answer questions to the best of my ability in the future.