Awesome Rust checkers

Contributions welcomed!

Table of contents

• Awesome Rust checkers
  • Table of contents
  • Linters
  • Static Checkers
  • Dynamic Checkers
  • Verifiers

Linters

Name	Description	Working on	Bug types	Technology	Maintenance
clippy	A bunch of lints to catch common mistakes and improve your Rust code. Paper: ICSE-Companion'24	HIR	Versatile	Pattern matching	★★★★★
dylint	Run Rust lints from dynamic libraries	HIR	Versatile	Pattern matching	★★★★★

Static Checkers

Name	Description	Working on	Bug Types	Technology	Maintenance
MIRAI	Rust mid-level IR Abstract Interpreter	MIR	Panic, Security bugs, Correctness	Abstract Interpretation	★★★★★
lockbud	Statically detect common memory and concurrrency bugs in Rust. Paper: Safety Issues in Rust, TSE'24	MIR	Double-Lock, Conflicting-Lock-Order, Atomicity-Violation, Use-After-Free, Invalid-Free, Panic Locations	Data-flow Analysis	★★★★★
RAP (formerly SafeDrop)	Rust Analysis Platform. Paper: SafeDrop, TOSEM'22	MIR	Use-After-Free, Double-Free	Data-flow Analysis	★★★★★
RCanary	Detecting Memory Leaks Across Semi-automated Memory Management Boundary in Rust. RCanary, TSE'24	HIR, MIR	Memory Leaks	Static Program Analysis, Model Checking	★★★☆☆
Rudra	Rust Memory Safety & Undefined Behavior Detection. Paper: Rudra, SOSP'21	HIR, MIR	Memory safety when panicked, Higher Order Invariant, Send Sync Variance	Data-flow Analysis	★★★☆☆
Yuga	Automatically Detecting Lifetime Annotation Bugs in the Rust Language. Paper: Yuga, ICSE'24	HIR, MIR	Lifetime Annotation Bugs	Data-flow Analysis	★★★★☆
MirChecker	A Simple Static Analysis Tool for Rust. Paper: MirChecker, CCS'21	MIR	Panic (including numerical), Lifetime Corruption (memory issues)	Abstract Interpretation	★★☆☆☆
FFIChecker	A Static Analysis Tool For Detecting Memory Management Bugs Between Rust and C/C++. Paper: FFIChecker, ESORICS'22	LLVM IR	Memory issues across the Rust/C FFI	Abstract Interpretation	★☆☆☆☆
RUPTA	Supports pointer/alias analysis for Rust, operating on Rust MIR. It currently offers callsite-based pointer analysis. Paper: RUPTA, CC'24	MIR	Not bugs, for callgraph construction	Callsite-based pointer analysis	★★★★★
Charon	Interface with the rustc compiler for the purpose of program verification. Paper: Charon	MIR, LLBC	An Analysis Framework for Rust	Convert MIR to LLBC for analysis	★★★★★
Cocoon	Static Information Flow Control in Rust. Paper: Cocoon, OOPSLA'24	Rust Soure Code	Secrecy Leaks	Rust’s type system and procedural macros	★★★★★
rustsp_analyzer	Fearless Unsafe. A More User-friendly Document for Unsafe Rust Programming Base on Refined Safety Properties. Paper: Fearless Unsafe	HIR	Safety Properties	Summarization	★★★★★
AtomVChecker	Statically detect memory ordering misuses for Rust. Paper: AtomVChecker, ISSRE'24	MIR	Atomic concurrency bugs and performance loss due to memory ordering misuse	Data-flow Analysis	★★★★★

Academic Papers (source code not found yet)

Name	Description	Working on	Bug Types	Technology
Rupair	Rupair: Towards Automatic Buffer Overflow Detection and Rectification for Rust. Rupair, ACSAC'21	AST, MIR	Buffer Overflow	Data-flow Analysis
CRUST	CRUST: Towards a Unified Cross-Language Program Analysis Framework for Rust. CRUST, QRS'22	CRustIR based on MIR	Security (CFI vilation, Meta Data Leaking, Format String Attack), Memory issues(Out-of-bounds, Use-after-Free, Double-Free, Stack-Overflow, Buffer-Overflow), Arithmetic (Divide-by-zero, Integer-Overflow)	Program Analysis Framework
ACORN	ACORN: Towards a Holistic Cross-Language Program Analysis for Rust. ACORN	Wasm	Security (Tainted Variable, Dangerous Function, Format String Attack), Memory issues (Out-of-bounds, Use-after-Free, Double-Free, Stack-Overflow, Buffer-Overflow), Arithmetic (Divide-by-zero, Integer-Overflow)	Program Analysis Framework
Yu Zhang	Static Deadlock Detection for Rust Programs. Yu Zhang	MIR	Deadlock	Data-flow Analysis
Kaiwen Zhang	Automatically Transform Rust Source to Petri Nets for Checking Deadlocks. Kaiwen Zhang	MIR	Deadlock	Petri Nets
RustC4	Leveraging Large Language Model to Assist Detecting Rust Code Comment Inconsistency. ASE'24	AST	Code Comment Inconsistency	LLM
craft	Automated Fault Tree Generation for Rust Programs. EDCC'24	-	Fault Tree	Static Program Analysis
PanicFI	An Infrastructure for Fixing Panic Bugs in Real-World Rust Programs. PanicFI	HIR, AST	Fixing Panic Bugs	Pattern Matching

Dynamic Checkers

Name	Description	Working on	Bug Types	Technology	Maintenance
miri	An interpreter for Rust's mid-level intermediate representation	MIR	Undefined Behavior	Abstract Interpretation	★★★★★
cargo-careful	Execute Rust code carefully, with extra checking along the way	-	Undefined Behavior	Enable Debug Assertion in std	★★★★★
cargo-fuzz	Command line helpers for fuzzing	-	-	Fuzzing	★★★★★
Loom	Concurrency permutation testing tool for Rust.	Source Code	Concurrency Bugs	Permutation testing	★★★★★
ERASAN	Efficient Rust Address Sanitizer. Paper: IEEES&P'24	-	Memory Access Bugs	Fuzzing	★★★★★
Automated-Fuzzer	Simple tool to create broken files and checking them with special apps	-	Panic	Fuzzing	★★★★★
RULF	Fuzz Target Generator for Rust libraries. Paper: RULF, ASE'21	-	Out-of-bound, Panic (including arithmetic)	Fuzzing	★★★☆☆
RPG1	RPG: Rust Library Fuzzing with Pool-based Fuzz Target. Paper: RPG, ICSE'24	-	Out-of-bound, Panic (including arithmetic)	Fuzzing	★★☆☆☆
SyRust	Automatic Testing of Rust Libraries with Semantic-Aware Program Synthesis. Paper: SyRust, PLDI'21	-	-	Program Synthesis	★☆☆☆☆
NADER	Automatic Context-Aware Safety Enhancement for Rust. Paper: OOPSLA'21	MIR, Source Code	Unchecked Indexing	API Replacing	★☆☆☆☆
casr2	collect crash (or UndefinedBehaviorSanitizer error) reports, triage, and estimate severity. Paper: Casr-Cluster, ISPRAS'21, Ivannikov Memorial Workshop'24	Crash Reports from ASan, UBSan, GDB	-	Analyze crashes	★★★★★
FRIES	Fuzzing Rust Library Interactions via Efficient Ecosystem-Guided Target Generation. Paper: FRIES, ISSTA'24	MIR	Rust API interactions	Fuzzing	★★★☆☆
rustsmith	A randomized program fuzzer for the Rust programming language. Paper: rustsmith, ISSTA'23 rustsmith, thesis	AST	Rust compiler bugs	Differential testing	★★★☆☆
rustlantis	UB-free and deterministic rustc fuzzer. Paper: rustlantis, OOPSLA'24	MIR	Rust compiler bugs	Differential testing	★★★★★
RuMono	A fully automated Rust fuzz driver generator. Paper: RuMono, TOSEM'24	-	Generic APIs	Fuzzing	★★★★★

Academic Papers (source code not found yet)

Name	Description	Working on	Bug Types	Technology
CrabSandwich	CrabSandwich: Fuzzing Rust with Rust. CrabSandwich, Fuzzing'23	LLVM IR	Out-of-bounds, Panic	Fuzzing
Zhiyong Ren	Detect Stack Overflow Bugs in Rust via Improved Fuzzing Technique. Zhiyong Ren, SEKE'21	AST, HIR, MIR, LLVM IR	Stack Overflow	Fuzzing
Rustcheck	Safety Enhancement of Unsafe Rust via Dynamic Program Analysis. Rustcheck, QRS-C'23	MIR	Memory vulnerabilities	Static Program Analysis, Instrumentation
RUSTY	A Fuzzing Tool for Rust. Poster@ACSAC'20	-	Vulnerabilities	Fuzzing, Concolic Testing, Property-based Testing
Rust-twins	Automatic Rust Compiler Testing through Program Mutation and Dual Macros Generation. ASE'24	AST, HIR	Rust compiler crashes and differences	Differential testing, mutation, macroize components, LLM
SafeFFI	Poster: Ensuring Memory Safety for the Transition from C/C++ to Rust. NDSS'24	LLVM IR	Memory safety in C/C++ and Rust Mixed Code	Existing sanitiers: HWASAN, SoftBound/CETS

1. The link may be incorrect. See here.
2. casr analyze the results of dynamic checkers instead of performing dynamic analysis itself. Thanks zjp-CN for recommending casr.

Verifiers

Name	Description	Working on	Bug Types	Technology	Maintenance
kani	The Kani Rust Verifier is a bit-precise model checker for Rust. Paper: kani, ICSE-SEIP'22	MIR	Memory safety, User-specified assertions, Panics, Unexpected behavior (e.g., arithmetic overflows)	Model Checking	★★★★★
prusti	A static verifier for Rust, based on the Viper verification infrastructure. Paper: prusti, NFM'22	Viper	Panic (inluding arithmetic), User-specified assertions	Symbolic Execution	★★★★☆
crux-mir	A static simulator for Rust programs. Paper: crux	-	-	Symbolic Testing	★★★★☆
verus	Verified Rust for low-level systems code. Paper: verus, OOPSLA'23, SOSP'24	-	-	SMT-based Verification5	★★★★★
flux	flux is a refinement type checker for Rust. Paper: flux, PLDI'23	-	-	-	★★★★★
Aeneas	A verification toolchain for Rust programs. Paper: Aeneas, ICFP'22, ICFP'24	LLBC (for safe Rust only)	-	-	★★★★★
RustBelt	Formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Paper: RustBelt, POPL'18	𝜆Rust	-	-	★★★★★
RustHorn	A CHC-based automated verifier for Rust RustHorn, TOPLAS'21	MIR	-	-	★★★★☆
Creusot	A deductive verifier for Rust code. Creusot, ICFEM'22	WhyML	Panics, overflows, Assertion failures	Deductive Verification	★★★★★
RustHornBelt	A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. Paper: RustHornBelt, PLDI'22	𝜆Rust	-	-	★★☆☆☆
RefinedRust1	A Type System for High-Assurance Verification of Rust Programs. Paper: RefinedRust, PLDI'24	Radium	-	-	★★★★★
VeriFast2	Research prototype tool for modular formal verification of C and Java programs. Paper: VeriFast, NFM'11	-	-	Symbolic Execution	★★★★★
mendel-verifier	Capability-based verifier for safe Rust clients of interior mutability. Paper: Poli, Thesis	Viper	Interior Mutability	Symbolic Execution	★★★★★
silver-sif-extension	Extension of the Viper language with modular product programs and information flow specifications. Paper: Thesis	Viper	Differential Privacy	Symbolic Execution	★★★★★

Academic Papers (source code not found yet)

Name	Description	Working on	Bug Types	Technology
GillianRust	A hybrid approach to semi-automated Rust verification. GillianRust	Unsafe Code Supported	-	Separation Logic based Hybrid Verification5
UnsafeCop	Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model checking. UnsafeCop, FM'24	-	Memory safety issues	Bounded Model Checking
SAFE	Automated Proof Generation for Rust Code via Self-Evolution. SAFE	Rust Code With Docstring, Verus	-	Verus Verifier, LLM
PanicCheck	Broadly Enabling KLEE to Effortlessly Find Unrecoverable Errors. PanicCheck, ICSE-SEIP'24	LLVM IR	Panic	KLEE

1. Thanks to jedbrown for recommending RefinedRust and other Rust-related verification tools.
2. Rust support is WIP in VeriFast. Thanks zjp-CN for recommending VeriFast.

Thanks to the following awesome works:

1. https://github.com/analysis-tools-dev/static-analysis?tab=readme-ov-file#rust
2. https://github.com/analysis-tools-dev/dynamic-analysis?tab=readme-ov-file#rust
3. A Survey of Rust Language Security Research
4. RefinedRust: A Type System for High-Assurance Verification of Rust Programs
5. Verifying the Rust Standard Library