8 ms·

Introduction to TLA+ Model Checking in the Command Line

176 points by mbellotti 8y ago

tombert 8y ago
I am glad to see that I am not the only person who hates the TLA Toolbox. TLA+ is brilliant, but I always feel like an outsider using Vim to edit my specs.
- RBerenguel 8y ago
  I do it in emacs, have been meaning to write a mode for a while, but.. time.
- cmarinas 8y ago
  I rarely use the Toolbox (especially since I couldn't find a pre-built Toolbox for ARM processors). I'm happy with vim or emacs and I usually have a script (that also does some massaging on the PlusCal-generated code): https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/tree/check.sh https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/ker...
- mcguire 8y ago
  Frama-C is similar; every one says to use the gui, but I find it horrible and just use the command line while feeling like a cave man.
- hwayne 8y ago
  If it helps at all, I do that a lot too, and have started working on extending my vim plugin[1] to also do configuration and run TLC. Honestly the big blocker here is learning how vimscript better. [1] https://github.com/hwayne/tla.vim/ https://github.com/hwayne/tla.vim/
  - tombert 8y ago
    Out of curiosity (and I'm speaking largely out of ignorance on this), have you considered making this plugin NeoVim specific and doing it in another language you are more comfortable with? EDIT: Also, just realize that you are the person who wrote the Practical TLA+ book...I loved it! Thanks for writing it!
onefuncman 8y ago
Have any cloud providers or open source projects started publishing their proofs of correctness yet? Is it cheaper to hire someone who knows TLA+ or to find a consultant?
- Twirrim 8y ago
  I haven't seen Amazon publish any, but various teams in AWS use TLA+ for critical parts of their infrastructure. A service I worked for there used it for an "absolutely must not make a mistake" component. Even with the initial learning curve of TLA+, two engineers were able to define the application logic, identify bugs and come to a final model in comparatively short order. Once they'd got that final model they found it relatively easy to translate that in to the final service code. By the time they were done, they realised they'd actually spent less time in total, TLA & coding, than they'd anticipated just building the component from scratch without TLA+.
  - SEJeff 8y ago
    The architect of AWS, James Hamilton, is a huge fan of formal verification and has spoken about it at length. https://perspectives.mvdirona.com/2014/07/challenges-in-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi... http://lamport.azurewebsites.net/tla/amazon-excerpt.html http://lamport.azurewebsites.net/tla/amazon-excerpt.html
    - Twirrim 8y ago
      Indeed. As I recall, he was really happy to hear my team was using it for the component.
- nickpsecurity 8y ago
  SPIN has long been used for similar stuff in academia and industry. They have published a lot of their specs and results. http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html http://www.imm.dtu.dk/~albl/promela.html http://www.imm.dtu.dk/~albl/promela.html There were many projects using Pi Calculus, too. One of my project ideas is something that converts TLA+ to SPIN and Pi Calculus to use their tools and works. Or just otherwise integrates them.
yodsanklai 8y ago
I've considered using the command-line when I started using TLA+, but the manual discouraged it and I use it only occasionally so I didn't want to invest too much time on it. I'd love to see a TLA+ package for vscode [1]. It seems there is more and more TLA+ adoption, it is surprising there aren't better environments to use it. The TLA Toolbox is awful (well, to be fair to the people that developed it, it does the job and maybe it's ok for some category of users). EDIT: [1] there's one actually, https://github.com/TeamTilapia/vscode-tilapia https://github.com/TeamTilapia/vscode-tilapia
- RBerenguel 8y ago
  Thanks for the link. I always prefer emacs above anything, but VS Code is not bad at all.
  - yodsanklai 8y ago
    It doesn't seem to be maintained, and it's not packaged either. Not sure it's worth installing.
- pron 8y ago
  I like the Toolbox. - It shows you the ASCII and pretty printed spec side-by-side. - It plots TLC data as it runs and presents live coverage data in a nice way. Soon it will also show TLC performance profiles as color maps. (https://twitter.com/lemmster/status/1082787089140183040 https://twitter.com/lemmster/status/1082787089140183040) - It makes running TLC in the cloud (single-node or distributed) very easy. (https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/ https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/) - I don't know of any other way of using TLAPS. (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/A_simple_proof.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...) Then again, I'm really not a fan of either vim or emacs, despite having used the latter as my main editor for some years. I think this may be because I value tools that present more information in a convenient way that allows me to inspect and analyze my text over tools that allow editing more quickly (when I write code, I spend 80% of my time in Sourcetrail and only use the editor to punch-in characters), but I don't know.
hamilyon2 8y ago
Thank you, hn and mbellotti. I was getting ready to learn tla+ but IDE seemed like impenetrable wall to me.
- nickkell 8y ago
  You still might want to use the IDE at first, mainly because resources like Lamport's video lectures use it.
jakeogh 8y ago
The TLA+ Video Course by Leslie Lamport: https://news.ycombinator.com/item?id=16956778 https://news.ycombinator.com/item?id=16956778
usermac 8y ago
I've watched TLA+ creators videos and was impressed positively. It is lovely to see such logic in action with powerful results.
yolodeveloper 8y ago
Sorry, I still am wobbly on the matter of how TLA+ is different from QuickCheck and it's clones? The idea that "you don't test a use-case, you test many inputs that may work differently" is solved by fuzzing/test factories. So TLA+ without the fuzzing, leaves what, temporal stuff? Did I miss anything?
- virgilp 8y ago
  TLA is about testing the design, not the implementation. Read the TLA homepage, I promise it's fun.
- pron 8y ago
  TLA+ is a language that allows you to specify your system in any level of detail. As such, it is more expressive than any programming language is or could ever be. TLA+ does indeed have a model checker, but model checkers don't "try many inputs." They check the entire state-space, covering potentially infinitely many executions.
  - lmm 8y ago
    > TLA+ is a language that allows you to specify your system in any level of detail. As such, it is more expressive than any programming language is or could ever be. I don't see that this necessarily follows? In most programming languages it's normal to have high level functions that describe your program in broad strokes and lower-level functions that describe your program in more detail. If you're talking about the ability to check aspects of program correctness without necessarily implementing an executable program, several languages support a technique of using "undefined" or similar to typecheck a "program" that can't actually run, or maybe can't even be built.
    - pron 8y ago
      It does follow from the need for arbitrary nondeterminism (basically, the unconstrained use of existential quantifiers) for arbitrary-level specification, and the absolute inability to compile/interpret such uses in any feasibly efficient manner. In TLA+ you could describe an algorithm that "somehow" performs some operation, without specifying how. E.g. in TLA+ you can say "this component somehow sorts a list efficiently," if the particular sorting algorithm is not central to what you want to specify. The requirement that descriptions of computation be mechanically translated into something you can run is an extremely constraining one (both theoretically and in practice -- most high-level descriptions of computational systems cannot be mechanically turned into executables). If you remove it, you get something that is not a programming language, but that is strictly more expressive. So, if all specifications of computations (programs) in your language can be interpreted/compiled into an executable, it necessarily follows that it is less expressive than TLA+. While programming languages could add constructs for such specifications (contracts/dependent types) they cannot compile them into an executable. This means that you get a language that really contains two separate languages (and they must be separate for compilation to work), one for nondeterministic specification and one for deterministic specification, with only the latter used to describe actual computation, and resulting in a language that is both an exceptionally complex specification language and an exceptionally complex programming language -- basically the worst of both worlds. That such language have only ever been used for software that's substantially smaller and simpler than jQuery is the empirical manifestation of that (not that such use cases aren't important, but that you can only effectively fully specify tiny programs does imply that their expressivity is limited).
yolodeveloper 8y ago
Another question is whether translation from TLA to, say Haskell or Scala is on the roadmap? That would be a killer feature but I've never heard this being something that is planned for implementation.
- carterschonwald 8y ago
  I’ve actually found translation between tla plus and Haskell or agda pretty straight forward using what I call the coinductive approach (which could also be called purely functional OOP done right), I have some examples I shared on reddit two years ago https://www.reddit.com/r/haskell/comments/4aju8f/simple_example_of_emulating_copattern_matching_in/ https://www.reddit.com/r/haskell/comments/4aju8f/simple_exam...
- virgilp 8y ago
  It would be impossible. The whole point of TLA is to test & document the high-level design. You can only generate complete implementation for toy problems (and that is a feature)
  - pron 8y ago
    I wouldn't say that's "the whole point." You can specify at any level you choose, even electronic circuits (in fact, TLA+ has been successfully used in the design of microprocessors). It's just that the most effective general-purpose use of formal methods, given our current technology, is in a high-level design (where high-level is relative to whatever your domain is), as formal methods are constrained by a certain amount of detail, and therefore it is best to use that budget on the actual tricky/subtle parts of the problem, rather than waste it on stuff that's fairly simple (translating the spec into code, which is simple but contains a lot of "uninteresting" detail).
    - virgilp 8y ago
      I would still say that, though. For complex/ non-"toy" systems, the required level of detail increases so much, that if you specify it all in something like TLA+, even ignoring the performance aspects, it probably becomes too hard to understand it all and you lose most of the advantage that TLA+ is supposed to give you. It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model. And the fact that it was used to design microprocessors doesn't say that it can or should be used to specify all the details. I bet nobody ever attempted to do the layout from the TLA+ model; it's just like in software, TLA+ was used to design geo-distributed databases... but not to write any piece of the code; just to check that the general design is right.
pron 8y ago
For those who care to provide constructive criticism, the TLA+ Toolbox issue tracker is just a click away (https://github.com/tlaplus/tlaplus/issues https://github.com/tlaplus/tlaplus/issues) and - since today - even has a UX label.

176 points by mbellotti 8y ago

I am glad to see that I am not the only person who hates the TLA Toolbox. TLA+ is brilliant, but I always feel like an outsider using Vim to edit my specs.

RBerenguel 8y ago
I do it in emacs, have been meaning to write a mode for a while, but.. time.
cmarinas 8y ago
I rarely use the Toolbox (especially since I couldn't find a pre-built Toolbox for ARM processors). I'm happy with vim or emacs and I usually have a script (that also does some massaging on the PlusCal-generated code): https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/tree/check.sh https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/ker...
mcguire 8y ago
Frama-C is similar; every one says to use the gui, but I find it horrible and just use the command line while feeling like a cave man.
hwayne 8y ago
If it helps at all, I do that a lot too, and have started working on extending my vim plugin[1] to also do configuration and run TLC. Honestly the big blocker here is learning how vimscript better. [1] https://github.com/hwayne/tla.vim/ https://github.com/hwayne/tla.vim/
- tombert 8y ago
  Out of curiosity (and I'm speaking largely out of ignorance on this), have you considered making this plugin NeoVim specific and doing it in another language you are more comfortable with? EDIT: Also, just realize that you are the person who wrote the Practical TLA+ book...I loved it! Thanks for writing it!

onefuncman 8y ago

Have any cloud providers or open source projects started publishing their proofs of correctness yet? Is it cheaper to hire someone who knows TLA+ or to find a consultant?

Twirrim 8y ago
I haven't seen Amazon publish any, but various teams in AWS use TLA+ for critical parts of their infrastructure. A service I worked for there used it for an "absolutely must not make a mistake" component. Even with the initial learning curve of TLA+, two engineers were able to define the application logic, identify bugs and come to a final model in comparatively short order. Once they'd got that final model they found it relatively easy to translate that in to the final service code. By the time they were done, they realised they'd actually spent less time in total, TLA & coding, than they'd anticipated just building the component from scratch without TLA+.
- SEJeff 8y ago
  The architect of AWS, James Hamilton, is a huge fan of formal verification and has spoken about it at length. https://perspectives.mvdirona.com/2014/07/challenges-in-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi... http://lamport.azurewebsites.net/tla/amazon-excerpt.html http://lamport.azurewebsites.net/tla/amazon-excerpt.html
  - Twirrim 8y ago
    Indeed. As I recall, he was really happy to hear my team was using it for the component.
nickpsecurity 8y ago
SPIN has long been used for similar stuff in academia and industry. They have published a lot of their specs and results. http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html http://www.imm.dtu.dk/~albl/promela.html http://www.imm.dtu.dk/~albl/promela.html There were many projects using Pi Calculus, too. One of my project ideas is something that converts TLA+ to SPIN and Pi Calculus to use their tools and works. Or just otherwise integrates them.

yodsanklai 8y ago

I've considered using the command-line when I started using TLA+, but the manual discouraged it and I use it only occasionally so I didn't want to invest too much time on it. I'd love to see a TLA+ package for vscode [1]. It seems there is more and more TLA+ adoption, it is surprising there aren't better environments to use it. The TLA Toolbox is awful (well, to be fair to the people that developed it, it does the job and maybe it's ok for some category of users). EDIT: [1] there's one actually, https://github.com/TeamTilapia/vscode-tilapia https://github.com/TeamTilapia/vscode-tilapia

RBerenguel 8y ago
Thanks for the link. I always prefer emacs above anything, but VS Code is not bad at all.
- yodsanklai 8y ago
  It doesn't seem to be maintained, and it's not packaged either. Not sure it's worth installing.
pron 8y ago
I like the Toolbox. - It shows you the ASCII and pretty printed spec side-by-side. - It plots TLC data as it runs and presents live coverage data in a nice way. Soon it will also show TLC performance profiles as color maps. (https://twitter.com/lemmster/status/1082787089140183040 https://twitter.com/lemmster/status/1082787089140183040) - It makes running TLC in the cloud (single-node or distributed) very easy. (https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/ https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/) - I don't know of any other way of using TLAPS. (https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/A_simple_proof.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...) Then again, I'm really not a fan of either vim or emacs, despite having used the latter as my main editor for some years. I think this may be because I value tools that present more information in a convenient way that allows me to inspect and analyze my text over tools that allow editing more quickly (when I write code, I spend 80% of my time in Sourcetrail and only use the editor to punch-in characters), but I don't know.

hamilyon2 8y ago

Thank you, hn and mbellotti. I was getting ready to learn tla+ but IDE seemed like impenetrable wall to me.

nickkell 8y ago
You still might want to use the IDE at first, mainly because resources like Lamport's video lectures use it.

jakeogh 8y ago

The TLA+ Video Course by Leslie Lamport: https://news.ycombinator.com/item?id=16956778 https://news.ycombinator.com/item?id=16956778

usermac 8y ago

I've watched TLA+ creators videos and was impressed positively. It is lovely to see such logic in action with powerful results.

yolodeveloper 8y ago

Sorry, I still am wobbly on the matter of how TLA+ is different from QuickCheck and it's clones? The idea that "you don't test a use-case, you test many inputs that may work differently" is solved by fuzzing/test factories. So TLA+ without the fuzzing, leaves what, temporal stuff? Did I miss anything?

virgilp 8y ago
TLA is about testing the design, not the implementation. Read the TLA homepage, I promise it's fun.
pron 8y ago
TLA+ is a language that allows you to specify your system in any level of detail. As such, it is more expressive than any programming language is or could ever be. TLA+ does indeed have a model checker, but model checkers don't "try many inputs." They check the entire state-space, covering potentially infinitely many executions.
- lmm 8y ago
  > TLA+ is a language that allows you to specify your system in any level of detail. As such, it is more expressive than any programming language is or could ever be. I don't see that this necessarily follows? In most programming languages it's normal to have high level functions that describe your program in broad strokes and lower-level functions that describe your program in more detail. If you're talking about the ability to check aspects of program correctness without necessarily implementing an executable program, several languages support a technique of using "undefined" or similar to typecheck a "program" that can't actually run, or maybe can't even be built.
  - pron 8y ago
    It does follow from the need for arbitrary nondeterminism (basically, the unconstrained use of existential quantifiers) for arbitrary-level specification, and the absolute inability to compile/interpret such uses in any feasibly efficient manner. In TLA+ you could describe an algorithm that "somehow" performs some operation, without specifying how. E.g. in TLA+ you can say "this component somehow sorts a list efficiently," if the particular sorting algorithm is not central to what you want to specify. The requirement that descriptions of computation be mechanically translated into something you can run is an extremely constraining one (both theoretically and in practice -- most high-level descriptions of computational systems cannot be mechanically turned into executables). If you remove it, you get something that is not a programming language, but that is strictly more expressive. So, if all specifications of computations (programs) in your language can be interpreted/compiled into an executable, it necessarily follows that it is less expressive than TLA+. While programming languages could add constructs for such specifications (contracts/dependent types) they cannot compile them into an executable. This means that you get a language that really contains two separate languages (and they must be separate for compilation to work), one for nondeterministic specification and one for deterministic specification, with only the latter used to describe actual computation, and resulting in a language that is both an exceptionally complex specification language and an exceptionally complex programming language -- basically the worst of both worlds. That such language have only ever been used for software that's substantially smaller and simpler than jQuery is the empirical manifestation of that (not that such use cases aren't important, but that you can only effectively fully specify tiny programs does imply that their expressivity is limited).

yolodeveloper 8y ago

Another question is whether translation from TLA to, say Haskell or Scala is on the roadmap? That would be a killer feature but I've never heard this being something that is planned for implementation.

carterschonwald 8y ago
I’ve actually found translation between tla plus and Haskell or agda pretty straight forward using what I call the coinductive approach (which could also be called purely functional OOP done right), I have some examples I shared on reddit two years ago https://www.reddit.com/r/haskell/comments/4aju8f/simple_example_of_emulating_copattern_matching_in/ https://www.reddit.com/r/haskell/comments/4aju8f/simple_exam...
virgilp 8y ago
It would be impossible. The whole point of TLA is to test & document the high-level design. You can only generate complete implementation for toy problems (and that is a feature)
- pron 8y ago
  I wouldn't say that's "the whole point." You can specify at any level you choose, even electronic circuits (in fact, TLA+ has been successfully used in the design of microprocessors). It's just that the most effective general-purpose use of formal methods, given our current technology, is in a high-level design (where high-level is relative to whatever your domain is), as formal methods are constrained by a certain amount of detail, and therefore it is best to use that budget on the actual tricky/subtle parts of the problem, rather than waste it on stuff that's fairly simple (translating the spec into code, which is simple but contains a lot of "uninteresting" detail).
  - virgilp 8y ago
    I would still say that, though. For complex/ non-"toy" systems, the required level of detail increases so much, that if you specify it all in something like TLA+, even ignoring the performance aspects, it probably becomes too hard to understand it all and you lose most of the advantage that TLA+ is supposed to give you. It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model. And the fact that it was used to design microprocessors doesn't say that it can or should be used to specify all the details. I bet nobody ever attempted to do the layout from the TLA+ model; it's just like in software, TLA+ was used to design geo-distributed databases... but not to write any piece of the code; just to check that the general design is right.

pron 8y ago

For those who care to provide constructive criticism, the TLA+ Toolbox issue tracker is just a click away (https://github.com/tlaplus/tlaplus/issues https://github.com/tlaplus/tlaplus/issues) and - since today - even has a UX label.