This question is difficult to answer in general, because TLA+ is a very particular kind of formal verification tool (it's a model checker designed more around concurrent hardware/software than e.g. pure mathematics or general proving, or equivalence checking, etc). There are a lot of verification tools out there, many of them substantially different in scope, intent, and design. It's a bit like asking "What prerequisites do I need to drive a (boat or a motorcycle)?" They're very different beasts, and it's a very big field.
On this note, "non-trivial" formal verification can often be very, very non-trivial, depending on how you approach it. And I mean that in the sense that actually writing the specifications and proving them can be extremely hard, depending on the tools -- even if the problem itself may 'seem' easy. Think "I have a 1000 line program that needs 10,000 lines of proofs". (1-2 orders of magnitude is probably a good ballpark estimate, if you're doing things with tools like Coq.)
Luckily, TLA+ in particular is pretty easy to learn and you can get productive in a few weeks I think, and it's geared more towards engineers than e.g. general mathematicians or whatever. This introduction is pretty good:
- https://learntla.com/introduction/
If you want a more general background... Go pick up some books on logic and computability. The things you learn here will apply deeply to nearly every approach to formal verification you can think of. Start with simple propositional logic, and you can move up to first-order logic, higher-order logics or type theory later on. This will help you understand logical systems, how to prove propositions, their relations, what can be decided etc, which will be deeply useful, forever.
If you want the book on this stuff, I strongly recommend the following one. It is dense but it is, in short, the bible of automated computer-based theorem proving, as far as I'm concerned, and has substantial code to back it up. (The author does formal verification of FPUs at Intel):
On this note, "non-trivial" formal verification can often be very, very non-trivial, depending on how you approach it. And I mean that in the sense that actually writing the specifications and proving them can be extremely hard, depending on the tools -- even if the problem itself may 'seem' easy. Think "I have a 1000 line program that needs 10,000 lines of proofs". (1-2 orders of magnitude is probably a good ballpark estimate, if you're doing things with tools like Coq.)
Luckily, TLA+ in particular is pretty easy to learn and you can get productive in a few weeks I think, and it's geared more towards engineers than e.g. general mathematicians or whatever. This introduction is pretty good:
If you want a more general background... Go pick up some books on logic and computability. The things you learn here will apply deeply to nearly every approach to formal verification you can think of. Start with simple propositional logic, and you can move up to first-order logic, higher-order logics or type theory later on. This will help you understand logical systems, how to prove propositions, their relations, what can be decided etc, which will be deeply useful, forever.If you want the book on this stuff, I strongly recommend the following one. It is dense but it is, in short, the bible of automated computer-based theorem proving, as far as I'm concerned, and has substantial code to back it up. (The author does formal verification of FPUs at Intel):
https://www.amazon.com/Handbook-Practical-Logic-Automated-Re...