people
awesome-tlaplus
people | awesome-tlaplus | |
---|---|---|
1 | 1 | |
- | 124 | |
- | 4.0% | |
- | 5.0 | |
- | 4 months ago | |
- | - |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
people
-
Ask HN: Do You Use TLA+
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.
awesome-tlaplus
-
Ask HN: Do You Use 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?
What are some alternatives?
DrTLAPlus - Dr. TLA+ series - learn an algorithm and protocol, study a specification
tlaplus - TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.