PlusCal is not able to handle process spawn operation, as far as I know. So if you are to model real system where clients come and go, you have to write your spec in pure
TLA+ which is unmaintainable, because it is just a logical assembler.
State explosion problem.
Java as implementation language. So you are using your CPU cycles not the best way.
Built-in proof system is not able to and was not supposed to check your proof. To do this you have to use some other tools like Coq (fix me if I am wrong)
Nearest competitors in that nich: Spin (yeah!), Alloy, EventB. Just let you know that there are alot of model checkers out there.
Java is very efficient, and TLC uses parallelism and even distributed parallelism (and can store states to disk).
This is first I hear of Spin, and I'll be sure to give it a try, but TLA+'s is considered easier to use and/or more expressive than many other solutions, and has the added advantage of being used in the industry (as far as formal verification tools go, that is).
I would very much like to hear more about Spin.
About Spin. If you compare the user base of Spin with the user base of TLA+ I bet you will wonder how many users out there were using verification tools all those years. Lamport released his tool like 20 years later than SPIN started to spread. He did a great job, but there is no innovation in my opinion.
I think that serious industry players like Intel, Google or NASA are using all spectre of verification tools, including self written tools. Intel is using there own tool for some of their chip verification AFAIK. My colleague went into Intel to help develop verification scripts using this tool.
TLA+ has been promoted by Amazon with their latest technical report. Yes, it has more expressive types (records,tuples,sets), but it comes with a cost of lowering your verification performance rate. There are many subtle tradeoffs to make.
We tried to use several formal verification tools in our latest distributed project. We tried Spin, TLA+, mCRL2, Coq. There is its own philosophy, pros and cons behind each tool, but in our case Spin made the best job: we had to invest not so much time but found many concurrency bugs in our distributed algorithm. Its pros is that it has very basic data types and not very good parallelism support nor in multi thread nor in multi-node form.
Coq,Agda: Manual/Semi-manual correctness proof of your system. You can reason about even "infinite" systems with this approach using relatively little computation resources. But to do so you have to gain a _deep_ insight about your system behaviour, computation semantics, network semantics (if distributed system is checked) and other properties. If you are lucky you can proof property under question, even it assumes very large moving parts. If not then you cant tell that this property can be proved at all. So these are more like platforms for quasi-manual deduction.
F* is trying to take up a niche between manual proof and quasi-automatic proof using SMT solver for those of theorems which can be proved this way. The problem is that SMT solvers are generally suck, there is no sound theory behind it, so it is more like guessing in my opinion.
Does anyone know how the TLA model checker works? I wasn't able to find this information. Does it use a SAT/SMT solver? Or brute force search?
Generally the model checker alone works just fine, though.