Hacker News Reader

I found TLA+ syntax unapproachable as a beginner. I did more digging and discovered Alloy[0], a "lightweight" formal verification system, which is much simpler, and has industry adoption as well. It's working nicely for me so far.

-----------

[0] http://alloytools.org/

The Bible of formal software logic, free of charge: https://softwarefoundations.cis.upenn.edu/

If you are more practical than religious, try this: https://functional-algorithms-verified.org

State Machines are the natural paradigm in TLA+. OOP is just poorly organized state machines. Try rewriting an OO program with state machines and you’ll have something that directly maps to TLA+, and it should demystify much of formal verification.