I've been trying to get into formal specification & verification too, but with Z notation (which is specifically for specification) instead, together with a couple of different theorem-provers. It's for a pet project to help me learn, so not something I would be using for serious work (not right away at least), but I find the Z notation quite readable and there is quite a bit of support and free tooling for it available online. Being quite new to formal methods, I think TLA+ would be overkill for learning.
You mentioned good tools available for Z - do you have any recommendations? I have tried in the past using VDM (alternative to Z, similar level) for writing down specifications precisely, but could never find adequate tools for maintaining/checking proofs/derivations.
Revanche1367 · · focus · HN ↗
<a href="https://en.wikipedia.org/wiki/Z_notation" rel="nofollow">https://en.wikipedia.org/wiki/Z_notation
jz391 · · focus · HN ↗