Formal Methods in Practice: Using TLA+ at ESpark | Hacker News Reader

Formal Methods in Practice: Using TLA+ at ESpark

medium.com

152 pointsluu19 comments

I just gotta say, it's _incredibly_ surreal seeing one of the people who inspired me to start studying formal methods link an article I wrote on formal methods.

Hi Hillel, Not sure if you can help but I am interested in TLA and was following your tla intro website, particularly this part: https://learntla.com/pluscal/toolbox/. I installed TLA+ Toolbox, added the example spec, translated and then tried to "run the model" however nothing happens. No output, the start and end time are still blank, no statistics etc. It is as if I never hit the run button. I don't see any errors in the console and I'm not exactly sure what I am doing so I may have missed something. FWIW the Model Overview view looks identical to the screenshot in the webpage.

Would you mind emailing me the screenshots at h@learntla? My immediate guess would be that "temporal properties" is unchecked, but I'd have to take a look.

Is TLA+ similar to Alloy[1]?

1. http://alloy.mit.edu/alloy/

Here's the comparison I found:

https://groups.google.com/forum/m/#!topic/tlaplus/C7Rmka3iSG...

Alloy is a nice tool. I've seen it in my field used to verify transaction handling in simple databases and part of a high-assurance VPN. Another person here said they check data structures with it.

In that they're both modeling languages, yes. Alloy is more geared toward algorithms, while TLA+ is more geared toward concurrent systems. This paper has a good comparison: https://arxiv.org/abs/1603.03599

TLA+ is not a model checker. It is a specification and proof language. However, it has verification tools that include a model checker (TLC) and a mechanical proof system (TLAPS), both support a large and useful subset of the language. There are also other TLA+ model checkers under development or already available with some effort. In many ways it is more similar to Coq and Isabelle than to Alloy. For one, it has proof of relative completeness: anything that can be proven about a system, can be proven in TLA+.

But because a model-checker makes a huge difference in productivity (it is usually the difference between worth it and not worth it), it TLA+ is similar to Alloy in terms of the effort required. Also, while it is harder to learn than Alloy, it is much easier to learn than Coq or Isabelle; partly due to design and partly due to the fact you can use it without learning how to be effective at writing formal, mechanically-chcekable proofs. It takes about two weeks to learn TLA+ well enough to start getting real work done.

OTOH, while TLA+ can in principle be used to prove general mathematical theorems, it was designed with a focus on discrete systems (i.e., software and hardware) and targeted at engineers, not mathematicians/logicians, so if you want to do general formal math, Isabelle or Coq would be a better choice.

Yes I misspoke, but, for the purposes of the article, the GP's question, and the use to which most readers here will put TLA+, it's tied at the hip to TLC and is used primarily for model checking.

The problem:

The apps, while critical to the effectiveness of the product, are also the most complicated component. Each student needs a different set of apps, which change as they complete lessons. We have to be able to track and adjust them in near-real time, so that students aren’t left without a next lesson. In extreme cases a student might need six apps in the morning and six completely different apps in the afternoon. We also have to be mindful of school budgets, so we have a limited number of the paid apps and shuttle them between students. Finally, since we need to do this at scale, the entire system has to run automatically with no teacher or admin intervention.

This seems to be re-inventing the Web, but with more DRM. It's a lot like running a corporate intranet. Ten years ago, this could all have been done easily with Java applets or Flash programs. The actual apps look like Flash projects.[1] Most of this could probably be done with some toolkit for generating browser games in HTML.

Does this thing really need to be this complicated? Or has it been overdesigned?

Mandatory XKCD: [2]

[1] https://www.youtube.com/watch?v=p6deAYxzlCc [2] https://xkcd.com/1367/

These are third party iOS apps; we don't make them, just curate them. We've at times looked into replacing all of the native apps with web apps but there just isn't enough quality stuff out there to make the switch possible.

What are the prerequisites for getting to a productive level at using formal methods (with or without TLA+) in a non-trivial way?

And what are some suggested resources for filling those prerequisites?

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):

https://www.amazon.com/Handbook-Practical-Logic-Automated-Re...

I agree with almost everything you say, but I have a few comments.

First, TLA+ is not a model checker. It is a specification and proof language that also has tools in the form of a model checker (more than one, actually) and a mechanical proof system.

Second, it is absolutely true that TLA+'s focus is not general mathematical theorem proving, and its intended audience are engineers, but it is not so much designed around concurrent hardware/software but that it is designed for algorithms in general. This means that it is also very appropriate for reasoning about concurrent or interactive (which is just a form of concurrency), whereas general mathematical tools that are often designed to reason about constructive functions rather than algorithms, and so can naturally reason about sequential algorithms, but need extra effort to reason about interaction or concurrency.

Finally, a strong focus of TLA+ is that it can serve as a refinement calculus, namely reason about the same system/algorithm at different abstraction levels, and explore the precise relationship between the different levels.

I agree that TLA+'s most practical advantage is that for its power, it is exceptionally easy to learn and apply in practice (much of this is due to the availability of a model checker). I also agree that ultimately, the specification, reasoning, and proof work in pretty much all formal tools is much more similar than different.

The hard stuff aseipp alludes to supposedly can be learned with these books:

https://www.cis.upenn.edu/~bcpierce/sf/current/index.html

http://adam.chlipala.net/cpdt/

A book on refinement calculus that connects high-level specs to low-level implementations:

http://lara.epfl.ch/w/_media/sav08:backwright98refinementcal...

My favorite illustration using Event-B of how requirements and specs can explode into many verification conditions for even something simple. You're explicitly handling both the stuff that's usually unstated and the needs of the tool.

http://eb2all.loria.fr/html_files/files/landingsystem.pdf

I know almost nothing about TLA+, but am greatly enjoying this book written by Lamport

http://lamport.azurewebsites.net/tla/book.html

One prerequisite is management sponsorship that understands the value of trying difficult things.

If you want freedom, air cover, and resources to apply formal methods to real production systems but haven't found that sponsor, try me: username at gmail.

Man it looks really cool to use this in an enterprise. It seems like you'd need a lot of support to introduce it into an Enterprise environment. Ramp-up time for learning and it looks like it runs really slow, so you'd need buy-in for the runtime too.

Any advice for those of us who'd like to introduce this to a team rather than play with it on our own?

Learn it on your own first before trying to foist it on others. I'm on the cusp of seriously introducing use of TLA+/PlusCal at the startup I'm at, and having worked through (and had success with) modeling a couple real-word concurrent systems I have designed here, I have a very different perspective how to use TLA and explain it to co-workers than when I first started using it.

(For example: it's tempting to think of variables as some sort of communication channel – they're not. And fairness can be hard to conceptualize until it's put to a real-world use.)

Definitely use PlusCal. It's a little more to learn, and a little more restrictive, than straight TLA+, but most TLA+ specs you write will end up looking like the output of PlusCal anyway, and the PlusCal version will be much more compact and easy-to-follow. Just remember that PlusCal is not like any other programming language; especially the "await" statement can throw newcomers off (it's not like "await" in other languages).

The way it worked out for me was to first learn it on my own, then model a buggy system at work, then demonstrate how it finds a bug. It's one thing to explain the ideas, another to see it actually run and produce an error trace that maps to a problem in the code.

Reply on news.ycombinator.com