stateright
dylint
Our great sponsors
stateright | dylint | |
---|---|---|
8 | 7 | |
1,516 | 337 | |
1.8% | 2.4% | |
7.0 | 9.7 | |
14 days ago | 4 days ago | |
Rust | Rust | |
MIT License | Apache License 2.0 |
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.
stateright
- Distributed Async Executors?
-
Announcing `statig`: Hierarchical state machines for event-driven systems (using GAT’s)
stateright - which is meant for distributed state machines and includes a full on model checker
-
RiB Newsletter #27
Stateright.
-
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?
* https://www.philipzucker.com/Modelling_TLA_in_z3py/
-
Does "safety by default" scale?
Why make memory safety the exception? For example, https://github.com/stateright/stateright implements model checking for distributed systems at the library-level. If you could achieve the same effect with memory safety through the ecosystem, why wouldn't you?
-
Stateright: A model checker for implementing distributed systems
Regarding the last point — correct, Stateright aims to verify both.
It’s important to clarify that this doesn’t provide a proof of correctness, but it can dramatically improve confidence in both the design and implementation compared with fuzz testing, for example. This is done by exhaustively enumerating possible nondeterministic outcomes (e.g. due to message reordering) within specified constraints (e.g. up to S servers and C clients performing X operations…).
Examples:
SD Paxos: https://github.com/stateright/stateright/blob/master/example...
ABD (linearizable register algorithm): https://github.com/stateright/stateright/blob/master/example...
-
Rust and Julia
I believe they meant this: https://github.com/stateright/stateright
dylint
-
rustc-plugin: A framework for writing plugins that integrate with the Rust compiler
There is also https://github.com/trailofbits/dylint for writing custom lints.
-
Hey Rustaceans! Got a question? Ask here (10/2023)!
Apart from clippy (which uses rustc-internal APIs), there are two other projects which can be used to implement lints: rust-analyzer can be extended with more diagnostics, and dylint provides an interface to run custom lints for Rust.
- Dylint: Tool for running Rust lints from dynamic libraries
-
Programming Breakthroughs We Need
RE: Program is a model
There are some more advanced refactoring tools now available. These tools enable you to write code to detect bad code patterns and even automatically fix them. You can use them to write one-off transformations of code too. Rust has Dylint [1] and C# has Roslyn Analyzers [2]. Facebook has tooling [3] that helps writing CodeMods, enabling authors to generate changes for thousands of files at a time.
The thing I really would like to see is a smarter CI system. Caching of build outputs, so you don't have to rebuild the world from scratch every time. Distributed execution of tests and compilation, so you are not bottle-necked by one machine. Something that keeps track of which tests are flaky and which are broken on master, so you don't have to diagnose spurious build failures. Something that only runs the test that transitively depend on the code you change. Automatic bisecting of errors to the offending commit.
[1] https://github.com/trailofbits/dylint
[2] https://docs.microsoft.com/visualstudio/code-quality/roslyn-...
[3] one example: https://github.com/facebook/jscodeshift
-
Rust code quality and vulnerability scan tool
If you're looking for something like clippy but with custom lints, there's also dylint -- it is clippy, but with support for running dynamically loaded lints across multiple versions of Rust.
-
Missing tooling in Rust?
You might find dylint useful! It's exactly that: a tool to run custom clippy lints.
-
RiB Newsletter #27
Dylint. A tool for running Rust lints from dynamic libraries.
What are some alternatives?
tlaplus - TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
compiler-solidity - The zkEVM Solidity compiler.
mina-vrf-rs
py2many - Transpiler of Python to many other languages
solana - Web-Scale Blockchain for fast, secure, scalable, decentralized apps and marketplaces.
raft.tla - TLA+ specification for the Raft consensus algorithm
remote-apis - An API for caching and execution of actions on a remote system.
lam - :rocket: a lightweight, universal actor-model vm for writing scalable and reliable applications that run natively and on WebAssembly
rust-analyzer - A Rust compiler front-end for IDEs
raft
aquascope - Interactive visualizations of Rust at compile-time and run-time