Our great sponsors
| raft | zre_raft | |
|---|---|---|
| 2 | 5 | |
| 8 | 2 | |
| - | - | |
| 0.0 | 0.0 | |
| over 1 year ago | over 2 years ago | |
| Python | Python | |
| MIT License | MIT License |
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.
raft
-
Paxos vs Raft: Have We Reached Consensus on Distributed Consensus?
Author seems to be using https://github.com/ailidani/paxi for actual implementation and proof.
I'm more of a python/rust guy. There have been some attempts to make model checkers in rust: https://github.com/stateright/stateright
The issue is that rust is a very large language and it's hard to get it right.
I have a python implementation of raft over here:
https://github.com/adsharma/raft/tree/master/raft/states
That's small enough to be self contained and perhaps run through a model checker some day and transpiled to many statically typed languages.
The issue with TLA+ proofs such as:
https://github.com/fpaxos/raft.tla
is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec.
So how do we check and transpile?
-
Rqlite: The lightweight, distributed relational database built on SQLite
https://github.com/adsharma/raft
Bug reports welcome
zre_raft
-
Rqlite: The lightweight, distributed relational database built on SQLite
Bob: /status
Etc
-
Ask HN: How do we know Signal or Telegram don't store our data on their servers?
If this is a concern for you, consider using the signal protocol without a server.
CLI prototype. Can be generalized into a nice phone app.
-
Automated Symbolic Verification of Telegram's MTProto 2.0
Even if the clients are open source and if the verification of the protocol using ProVerif is sound, there is the possibility of a divergence between the "proof" and the implementation.
This is why it's important to have them in the same code base.
I've heard about attempts at inria to implement signal/double ratchet using F-star and verify the correctness. But no such implementation seems to be publicly available.
One of the things I'm interested in is to see if it's possible to bring these verification technologies to more mainstream programming languages such as python.
https://github.com/adsharma/zre_raft/blob/main/zre_raft/zre_...
is something I'd love to verify.
-
Donate to Signal
As a token of support, I implemented signal protocol in 250 lines of python.
https://github.com/adsharma/zre_raft/blob/main/zre_raft/zre_...
Hope more programmers understand how this works, implement it correctly and create apps we haven't thought about yet.
What are some alternatives?
paxi - Paxos protocol framework
rqlite - The lightweight, distributed relational database built on SQLite.
k3s - Lightweight Kubernetes
Signal-iOS - A private messenger for iOS.
stateright - A model checker for implementing distributed systems.
raft.tla - TLA+ specification for the Raft consensus algorithm
Telegram-iOS - Telegram-iOS
py2many - Transpiler of Python to many other languages
OpenSSL - TLS/SSL and crypto library
Signal-Server - Server supporting the Signal Private Messenger applications on Android, Desktop, and iOS