Ask HN: Do You Use TLA+

• tlaplus

  38 2,210 9.1 Java

  TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

  

## 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?

• awesome-tlaplus

  1 124 5.0

  A curated list of TLA+ resources.

  

## 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?

• InfluxDB

  www.influxdata.com featured

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• DrTLAPlus

  1 777 1.8 TLA

  Dr. TLA+ series - learn an algorithm and protocol, study a specification

  

## 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?

• people

  1 - -

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.

Suggest a related project