3 ms·
> To ensure correctness in our design and implementation, we use TLA+ to formally prove our work. Hah, I'm sure it's not for the whole thing but I wonder how m
by makmanalp 8y ago
> To ensure correctness in our design and implementation, we use TLA+ to formally prove our work.
Hah, I'm sure it's not for the whole thing but I wonder how many vendors can claim anything close to that!
- ceohockey60 8y agoFwiw, they've open sourced their TLA+ proofs for percolator and raft merge. Worth checking out: https://github.com/pingcap/tla-plus https://github.com/pingcap/tla-plus
- rrdharan 8y agoBoth Microsoft (Leslie Lamport's current employer) and AWS, at least: https://en.wikipedia.org/wiki/TLA%2B#Industry_use https://en.wikipedia.org/wiki/TLA%2B#Industry_use
- staticassertion 8y agoSeems like good company to be in.
- makmanalp 8y agoThat Lamport and his current company are using TLA+ does not surprise me ;-) AWS is interesting. Before jepsen and similar stuff we used to have to take the vendor's word on a lot of claims. Hopefully the attitude there is changing towards more public self-verification (releasing stuff this) and then independent external verification!