Ask HN: Do you use TLA+? | Hacker News Reader

Ask HN: Do you use TLA+?

49 pointsriddleronroof24 comments

It's surprising to me that so many crypto projects don't use TLA+. Besides the ones mentioned here (https://lamport.azurewebsites.net/tla/industrial-use.html), does your company use TLA+? Why? Why not?

View on HN

Can't speak for crypto projects. I used it to verify some incredibly complicated security fixes I made; you can find my models here:

https://gitlab.com/xen-project/people/gdunlap/tla

And the security advisory here:

https://xenbits.xenproject.org/xsa/advisory-299.txt

A description of the issue, sketches of the attacks, and the fixes can be found in the individual patches.

TLA+ was obviously very powerful, but it is incredibly quirky in so many ways. The scoping of variable in PlusCal is really strange: it looks like you can make variables with local scope, but then they turn out to have global scope.

You have to fight the tool to be able to use it outside of its special-purpose IDE or make it something that could be sensibly collaborated on over git. (See some of the makefile runes in the above repo to see the kind of thing I did.) Getting it to do parallel searches was difficult.

## TLA+

Wikipedia: https://en.wikipedia.org/wiki/TLA%2B

Src: https://github.com/tlaplus/tlaplus

Awesome: https://github.com/tlaplus/awesome-tlaplus

### Dr TLA+

Web: https://github.com/tlaplus/DrTLAPlus

Src: https://github.com/tlaplus/DrTLAPlus :

> Dr. TLA+ series - learn an algorithm and protocol, study a specification; [Byzantine] Paxos, Raft, Cosmos,

"Concurrency: The Works of Leslie Lamport" ( https://g.co/kgs/nx1BaB

https://westurner.github.io/hnlog/#comment-27442819 :

> Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all?

To answer "why not?": Because, like a lot of things I've tried to pilot at work, management doesn't see the value when compared against other techniques and the cost of training and maintaining the skillset.

I used it on a system to show:

1. Where a problem was occurring in a concurrent system's design, and how to fix it by changing the protocol the two processes used to communicate.

2. Where a problem was occurring in the data bus of a hardware system. Specifically, which part of the spec had been mis-implemented.

Both took as long or longer to do compared to the traditional techniques of hooking up an oscilloscope and looking at results, writing test-specific programs to exercise things, and writing tests to find other problems. It could have been faster if I weren't a TLA+ novice at the time, I think, but then I'd be the only one who understood it. It also wouldn't have been terribly useful for the majority of the time, think 1-2 problems (issues found or new designs) that it may have applied to. I'm willing to work on my own skills outside of work hours (though the last 3 years I've definitely slowed down on that), but the majority of my coworkers aren't (for various reasons, mostly valid, I was single at the time, most of them were married and many had kids, that's a lot of time that's no longer yours). Management isn't willing (mostly the right thing) to spend time and money on training that doesn't have an obvious payback when other techniques work as well (from their perspective) and don't require any extra training or skill maintenance effort.

I've used it a few times. It was the most useful either to "prove" the conditions for a bug[1], or to gain confidence that an algorithm I had worked on was safe under tricky conditions involving concurrency.

The main downside of TLA+/PlusCal is that it's so different from programming languages that very few engineers are familiar with it. Even PlusCal which is supposed to provide a Pascal-like syntax that gets translated to TLA+ can be tricky to use and has a few pitfalls that can be frustrating for beginners.

The tooling is improving, but some design choices are really not ideal. For example, you write PlusCal in a `.tla` file inside a comment block(!) and when you transpile it to TLA+ the generated code is written after your comment, in the same file[2]. This is just one of a number of baffling decisions that create a ton of friction when using these tools. Others on this page have mentioned issues with scope, this is certainly something I've had to fight with.

[1] The bug I wrote a model for was CASSANDRA-8287, "Row Level Isolation is violated by read repair": https://issues.apache.org/jira/browse/CASSANDRA-8287. The error trace describes a clear scenario under which this would happen.

[2] See this very simple model for an example of how PlusCal is written in a comment block followed by the TLA+ code that's generated from it: https://gist.github.com/nicolasff/bcc92627485c3d4d9e0c25eeea...

The "why not" list is long and applies to many niche technologies:

* No understanding of formal methods. Even someone is working on a problem that TLA+ would be great at, they don't even know that formal methods exist.

* People aren't given time to apply formal methods. Schedules don't allow for getting things correct. It's hard to persuade management to make space for formal methods for various reasons.

* Other methods of getting the right (or close to it) product and outcome exist. People are more comfortable with building things and testing them rather than using formal methods. They are willing to take a risk with that approach even if there is a strong argument for formal methods.

* People that know/use formal methods tend to gravitate towards niches. Rather than taking on the hard adoption challenges and impacting the culture across large organizations they tend to focus on success niches. Other software engineering mavens are applying arguably easier and less effective processes more successfully across a broad audience.

These don't focus on the product itself. TLA+ has challenges as others point out, but it's hard for it to succeed broadly when there isn't a strong desire for the capability. If the user experience got super slick, then there is a chance that it could become such low effort that people would do it, but this doesn't seem a likely outcome.

I think there's also a lot we can do to make formal methods easier to learn and use. One of the big things I'm pushing for Alloy is to get a proper CLI so people don't have to do everything through the IDE— this is a surprising source of friction for beginners.

As someone who started learning TLA+ in the new year, I'd also add:

* The class of bugs it excels at finding which humans can't just aren't that important for most cases!

I'm learning it by modeling one of our systems which I know has a race condition that sometimes results in a request being dropped, with the goal of having TLA+ prove it.

But if I actually filed this as a bug - three in every ~billion requests get dropped in a process that's already at best reporting 99.9% accurate anyway - it would go straight to the bottom of the backlog. Inconsistent CSS styling of our swagger probably costs us more than this.

It’d be more critical in some use cases. Things like DB’s or operating systems would find more value in TLA+. I’m doing embedded work and really want to learn TLA+ at some point.

I think you are spot on. Cryptocurrencies grew very fast to capture the market. They had no time to apply formal methods. But now they are rushing to do so. There are many job offers in the formal methods, a market that was previously close to zero, and they come mostly from blockchain projects.

Formal methods have been limited to industries that are very conservative and where code moves slowly. I used them in railway systems and real-time systems for avionics, more than a decade ago. Finding jobs out of that area was not easy.

I'm hoping that advances in synthesis, thanks to mixing DL transformers and the already great SAT/SMT solvers, help making formal methods less costly to apply and much more popular. here are lots of interesting and practical ideas in refinement types (e.g. Liquid Haskell), theorem proving (e.g. translators from OCaml to Coq), etc. that would benefit a lot from automation.

I've read Hillel Wayne's "Practical TLA+", which is a very good introduction, and watched a couple of talks on it. I also collect case studies of TLA+ usage. I find the concept really a good idea and would love to use it more.

My main issue is that because it's not an everyday tool and has somewhat complex semantics, it becomes hard to use. The syntax and tooling are quite arcane and different from everyday programming languages. That's particularly problematic as it is supposed to be a tool to think about complex issues with it. Translating back and forth between what a spec says syntactically and what it actually means semantically is just hard, and for a non-everyday user, I would expect to make more mistakes when writing a spec or interpreting one I wrote 2 months ago, than I will have with less formal methods that I can actually understand.

I wish this was easier and I suspect that having a more mainstream way to express things in TLA+ would get into that direction. I tried to write a toy parser for a language that translates to TLA+, but I didn't get very far yet.

I've tried it a few times.

I wanted to use it a couple days ago to help me understand how a bad state could be reached in a program I was debugging, but found out the tla toolbox no longer starts because it depends on something that's changed in the current java environment (anyone remember write once run anywhere? it was always a lie). I don't have the patience to fight more tools than I absolutely have to.

I guess that's my biggest obstacle to using TLA+. I would likely use it if I could just install it from my distro's package manager and have a single clean binary that can be invoked from the command line like a compiler, passing it the path to my model. I find the java gui ux to be repulsive.

What I fail to understand how the same industry which is against "Waterfall"[1]/BDUF[2] is pushing formal methods?

There are so many low-hanging fruits to try before using heavyweight formal methods, which will give you a much better ROI:

  Informal methods:
  - thinking before coding
  - writing stuff down
  - using pen and paper
  - HDD - Hammock-Driven Development
  - taking a walk, taking a shower
  - talking to yourself, talking to people, talking to computer, talking to rubber duck[3]
  - design reviews

  Lightweight formal methods:
  - Decision Tables
  - Business Rules
  - FSM and StateCharts
  - PBT (Property-based Testing)
  - DbC (Design-by-Contract)
  - Functional Programming with Algebraic Type Systems
  - purpose-built problem-specific DSLs
  - ABM (Agent-based modeling) and simulations

EDIT: Specifically for "Crypto" projects, modeling, simulations, and even Reinforcement Learning probably a better fit than formal specification tools like TLA+/Alloy.

It's a huge work to formally specify even a small "smart contract"[4].

I don't think that formal specification can model implicit state like the one present in EVM, DApps/JS, and off-chain / out-of-band entities like crypto "Exchanges"[5].

Instead of trying to formally specify a "smart contract" written in Turing-complete Solidity and compiled to Forth-like EVM opcodes, it's probably better to write contracts in purpose-built non-Turing-complete financial DSLs with the 1st-class citizen concepts of money, user accounts and transactions.

[1] So called "Waterfall", most people are calling any SDLC with an upfront design phases - "Waterfall", like for example Rational Unified Process (RUP) - which is iterative with overlapping phases.

[2] Big Design Up Front

[3] RDD - Rubber-duck Debugging

[4] which is actually an Agent with a wallet, not a contract in legal or even SW development sense

[5] better called unlicensed Broker-Dealers

Developers are lazy. They don't want to write technical specifications. They can barely be bothered to write a README with the design or make an ADR. They can't even be bothered to write tests half the time.

It's also hard to explain to your bosses that you won't have any actual code for 6 months.

Experienced lead devs will use it on projects where accuracy and reliability is paramount. Otherwise it's just seen as yak shaving.

How often do you floss?

> It's also hard to explain to your bosses that you won't have any actual code for 6 months.

Formal methods don't have to mean "stop the world and do nothing else". They're tools for thinking through (often) harder problems in a systematic way. They're applicable through every stage of development. During initial design and requirements gathering (where I've seen and used other methods, like describing systems via state chart and state machine models), during development to clarify some confusing portion of the system, in analysis of problems (like the ones I described in my other post), and so on.

> Developers are lazy. They don't want to write technical specifications. They can barely be bothered to write a README with the design or make an ADR. They can't even be bothered to write tests half the time.

I would be bothered if I was incentivized to write documentation instead of shipping features.

TLA+ is mentioned a lot here and many people point out how it's practically infeasible to use it in real world systems. Just curious, is there any alternative to write specifications which are more closer to common programming languages and can be used by an average programmer to formally prove correctness?

I've heard Alloy is easier to learn. That being said, Alloy and TLA+ are both languages for specifications, so they can't prove an implementation is correct.

Nobody mentioned Agda. I had to use Alloy in the university and it was easy, but it doesn't cover all bases as the previous commenter said.

We do use a lot of three letter acronyms, but are trying to curb it because it's confusing for new people.

Not sure if you're speaking generically, or about this specific post, but; TLA+[0] is not an acronym but a language name. TLA, however, is an acronym of "Temporal Logic of Actions"

[0]:https://lamport.azurewebsites.net/tla/tla.html

I think the use of TLA+ is very niche, just to prove that some really lower level algorithms for distributed systems work well, I think crypto might be a good use case like you mentioned, but I guess most companies wouldn’t benefit from it except if for fun

I would like to, I've been working on learning it in my spare time but it's a big learning curve. It takes a mental shift because it's not programming, it's math.

actually you just gave me an idea where can I apply TLA+ in my job right now, we were thinking hard of many kafka streams and retry mechanisms we need to use, and still guarantee order without being blocking, and I think TLA+ is the perfect tool for the job of checking if we are not missing any edge cases with our current plan

Reply on news.ycombinator.com