fiat
Rudra
| fiat | Rudra | |
|---|---|---|
| 1 | 11 | |
| 145 | 1,297 | |
| 1.4% | 2.4% | |
| 6.9 | 5.5 | |
| 13 days ago | about 2 months ago | |
| Coq | Rust | |
| GNU General Public License v3.0 or later | 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.
fiat
-
Magma, a project I hope will make provably correct software possible for everyone
Yeah once this project is actually real it could be used for that ha :) Your description kinda reminds me fiat: https://github.com/mit-plv/fiat which generates code from just a correctness specification.
Rudra
- Rudra – static analyzer to detect common undefined behaviors in Rust programs
- Rudra: Finding Memory Safety Bugs in Rust at the Ecosystem Scale [pdf]
-
Does Rust not need extra linting and sanitizing tools like C++?
If you’re writing unsafe Rust, you might consider cargo miri and Rudra as additional static analyzers which can find bugs rustc won’t
-
Open Rust-related systems research problems suitable for PhD?
In my opinion, much of Rust-specific PhD research likely to be publishable and/or high impact either falls into verification (e.g Prusti, Cruesot) or bug-finding (e.g. Rudra, SyRust). Ralf Jung and his collaborators have done exceptional work in the verification space.
-
Introducing Fortify: A simple and convenient way to bundle owned data with a borrowing type
Perhaps Rudra as well.
- Magma, a project I hope will make provably correct software possible for everyone
-
Is There Anyway To Analyze Unsafe Rust Code For Vulnerabilities?
Haven't used it myself, but I remembered a tool called Rudra was recently posted about in the sub
-
Scylla – Real-Time Big Data Database
Not sure proves your point, but maybe doesn't disprove your point strongly enough. I am not qualified to argue from experience about how Rust is ideally suited in the ways you think it is not. But from everything I have seen, it can do a whole lot of what C++ is also good at. Rust safety is not all or nothing and a codebase could definitely prioritize ergonomics over correctness.
Two things that I saw in the last couple weeks that might start to sway you.
https://github.com/sslab-gatech/Rudra#readme
GhostCell: Separating Permissions from Data in Rust
- Rudra, Rust Memory Safety and Undefined Behavior Detection
- Rudra: Rust Memory Safety and Undefined Behavior Detection
What are some alternatives?
electrolysis - Simple verification of Rust programs via functional purification in Lean 2(!)
magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
prusti-dev - A static verifier for Rust, based on the Viper verification infrastructure.
tectonic - A modernized, complete, self-contained TeX/LaTeX engine, powered by XeTeX and TeXLive.
project-safe-transmute - Project group working on the "safe transmute" feature
line-combination-proofs
rust-verification-tools - RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.
rust - Rust for the xtensa architecture. Built in targets for the ESP32 and ESP8266
advisory-db - Security advisory database for Rust crates published through crates.io