add VerusBelt, etc

Author: CodeSentryAI

README.md

@@ -41,6 +41,7 @@ A curated list of awesome Rust analysis and verification tools, including linter
 | [MirChecker](https://github.com/lizhuohua/rust-mir-checker) | A Simple Static Analysis Tool for Rust. Paper: [MirChecker, CCS'21](https://dl.acm.org/doi/10.1145/3460120.3484541) | MIR | Panic (including numerical), Lifetime Corruption (memory issues) | Abstract Interpretation | 2024-05-24 |
 | [FFIChecker](https://github.com/lizhuohua/rust-ffi-checker) | A Static Analysis Tool For Detecting Memory Management Bugs Between Rust and C/C++. Paper: [FFIChecker, ESORICS'22](https://dl.acm.org/doi/10.1007/978-3-031-17143-7_33) | LLVM IR | Memory issues across the Rust/C FFI | Abstract Interpretation | 2022-05-31 |
 | [RUPTA](https://github.com/rustanlys/rupta) | Supports pointer/alias analysis for Rust, operating on Rust MIR. It currently offers callsite-based pointer analysis. Paper: [RUPTA, CC'24](https://dl.acm.org/doi/10.1145/3640537.3641574), [Stack Filtering, CGO'25](https://dl.acm.org/doi/pdf/10.1145/3696443.3708921) | MIR | Not bugs, for callgraph construction | Callsite-based pointer analysis | 2025-06-17 |
+| [Pincer](https://github.com/rustanlys/pincer) | Static analyzer for unsafe Rust memory-safety bugs. Paper: [Pincer, OOPSLA'26](https://dl.acm.org/doi/abs/10.1145/3798266) | MIR | Use-after-free, Double-free, Dangling pointer | Demand-driven IFDS alias analysis, Typestate analysis | 2026-04-14 |
 | [Cocoon](https://github.com/PLaSSticity/Cocoon-implementation) | Static Information Flow Control in Rust. Paper: [Cocoon, OOPSLA'24](https://dl.acm.org/doi/pdf/10.1145/3649817) | Rust Source Code | Secrecy Leaks | Rust's type system and procedural macros | 2024-03-20 |
 | [rustsp_analyzer](https://github.com/Artisan-Lab/rustsp_analyzer) | Fearless Unsafe. A More User-friendly Document for Unsafe Rust Programming Base on Refined Safety Properties. Paper: [Fearless Unsafe](https://arxiv.org/pdf/2412.06251) | HIR | Safety Properties | Summarization | 2025-01-01 |
 | [AtomVChecker](https://github.com/AtomVChecker/rust-atomic-study/tree/main/section-5-detection/AtomVChecker) | Statically detect memory ordering misuses for Rust. Paper: [AtomVChecker, ISSRE'24](https://ieeexplore.ieee.org/document/10771495) | MIR | Atomic concurrency bugs and performance loss due to memory ordering misuse | Data-flow Analysis | 2025-06-27 |
@@ -59,11 +60,11 @@ A curated list of awesome Rust analysis and verification tools, including linter
 
 | Name | Description | Working on | Bug Types | Technology | Last Commit Time |
 | -----| ----------- | ---------- | ----------| -----------| ----------- |
-| [miri](https://github.com/rust-lang/miri) | An interpreter for Rust's mid-level intermediate representation | MIR | Undefined Behavior | Abstract Interpretation | 2026-06-06 |
+| [miri](https://github.com/rust-lang/miri) | An interpreter for Rust's mid-level intermediate representation. Paper: [Miri, POPL'26](https://dl.acm.org/doi/abs/10.1145/3776690) | MIR | Undefined Behavior | Abstract Interpretation | 2026-06-06 |
 | [cargo-careful](https://github.com/RalfJung/cargo-careful) | Execute Rust code carefully, with extra checking along the way | - | Undefined Behavior | Enable Debug Assertion in std | 2026-04-01 |
 | [cargo-fuzz](https://github.com/rust-fuzz/cargo-fuzz) | Command line helpers for fuzzing | Binary | Crashes, Panics, Memory errors | Fuzzing | 2026-05-26 |
 | [Loom](https://github.com/tokio-rs/loom) | Concurrency permutation testing tool for Rust. | Source Code | Concurrency Bugs | Permutation testing | 2026-02-20 |
-| [Shuttle](https://github.com/awslabs/shuttle) | A library for testing concurrent Rust code. Paper [A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/asplos277-pct.pdf) | Source Code | Concurrency Bugs | Randomized testing | 2026-05-22 |
+| [Shuttle](https://github.com/awslabs/shuttle) | A library for testing concurrent Rust code. Paper: [A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/asplos277-pct.pdf) | Source Code | Concurrency Bugs | Randomized testing | 2026-05-22 |
 | [ERASAN](https://github.com/S2-Lab/ERASan) | Efficient Rust Address Sanitizer. Paper: [IEEES&P'24](https://www.computer.org/csdl/proceedings-article/sp/2024/313000a239/1WPcYZde4BW) | - | Memory Access Bugs | Fuzzing | 2025-06-30 |
 | [Automated-Fuzzer](https://github.com/qarmin/Automated-Fuzzer) | Simple tool to create broken files and checking them with special apps | - | Panic | Fuzzing | 2026-05-19 |
 | [RULF](https://github.com/Artisan-Lab/RULF) | Fuzz Target Generator for Rust libraries. Paper: [RULF, ASE'21](https://dl.acm.org/doi/abs/10.1109/ASE51524.2021.9678813) | - | Out-of-bound, Panic (including arithmetic) | Fuzzing | 2023-11-09 |
@@ -108,6 +109,7 @@ A curated list of awesome Rust analysis and verification tools, including linter
 | [RustHorn](https://github.com/hopv/rust-horn) | A CHC-based automated verifier for Rust [RustHorn, TOPLAS'21](https://dl.acm.org/doi/full/10.1145/3462205) | MIR | - | - | 2024-08-27 |
 | [Creusot](https://github.com/creusot-rs/creusot) | A deductive verifier for Rust code. [Creusot, ICFEM'22](https://inria.hal.science/hal-03737878/file/main.pdf) | WhyML | Panics, overflows, Assertion failures | Deductive Verification | 2026-06-05 |
 | [RustHornBelt](https://gitlab.mpi-sws.org/iris/lambda-rust/-/tree/masters/rusthornbelt) | A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code. Paper: [RustHornBelt, PLDI'22](https://dl.acm.org/doi/10.1145/3519939.3523704) | 𝜆Rust | - | - | 2023-02-14 |
+| [VerusBelt](https://zenodo.org/records/19613067) | A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System. Paper: [VerusBelt, PLDI'26](https://iris-project.org/pdfs/2026-pldi-verusbelt.pdf), [Artifact](https://zenodo.org/records/19613067) | Rocq, Iris | Soundness of Verus proof-oriented extensions | Semantic Foundation | 2026-03-18 |
 | [RefinedRust<sup>1</sup>](https://gitlab.mpi-sws.org/lgaeher/refinedrust-dev) | A Type System for High-Assurance Verification of Rust Programs. Paper: [RefinedRust, PLDI'24](https://dl.acm.org/doi/10.1145/3656422) | Radium | - | - | 2025-01-03 |
 | [VeriFast<sup>2</sup>](https://github.com/verifast/verifast) | Research prototype tool for modular formal verification of C and Java programs. Paper: [VeriFast, NFM'11](https://doi.org/10.1007/978-3-642-20398-5_4) | - | - | Symbolic Execution | 2026-05-10 |
 | [mendel-verifier](https://github.com/viperproject/mendel-verifier) | Capability-based verifier for safe Rust clients of interior mutability. Paper: [Poli](https://arxiv.org/abs/2405.08372), [Thesis](https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/703796/Poli2024.pdf?sequence=3&isAllowed=y) | Viper | Interior Mutability | Symbolic Execution | 2024-07-16 |
@@ -134,7 +136,7 @@ A curated list of awesome Rust analysis and verification tools, including linter
 | [cargo-geiger](https://github.com/geiger-rs/cargo-geiger) | Detects usage of unsafe Rust in a Rust crate and its dependencies | Source Code | Unsafe code usage | Static Analysis | 2025-08-31 |
 | [cargo-vet](https://github.com/mozilla/cargo-vet) | Supply-chain security for Rust - audit your dependencies for trustworthiness | Cargo.lock, Source | Untrusted dependencies | Supply Chain Auditing | 2026-04-19 |
 | [cargo-auditable](https://github.com/rust-secure-code/cargo-auditable) | Make production Rust binaries auditable - embed dependency info into binaries | Binary | Dependency vulnerabilities in production binaries | Binary Auditing | 2026-05-28 |
-| [cargo-scan](https://github.com/PLSysSec/cargo-scan) | A tool for auditing Rust crates - scans for unsafe patterns and security-sensitive operations | Source Code, MIR | Unsafe patterns, Security-sensitive operations | Static Analysis | 2026-06-05 |
+| [cargo-scan](https://github.com/PLSysSec/cargo-scan) | A tool for auditing Rust crates - scans for unsafe patterns and security-sensitive operations. Paper: [Auditing Rust Crates Effectively, ESOP'26](https://link.springer.com/chapter/10.1007/978-3-032-22723-2_15) | Source Code, MIR | Unsafe patterns, Security-sensitive operations | Static Analysis | 2026-06-05 |
 | [cargo-udeps](https://github.com/est31/cargo-udeps) | Find unused dependencies in Cargo.toml | Cargo.toml | Unused dependencies | Dependency Analysis | 2026-04-29 |
 | [cargo-semver-checks](https://github.com/obi1kenobi/cargo-semver-checks) | Scan your Rust crate for semver violations | Rust ABI | Semver violations | Static Analysis | 2026-05-31 |
 | [cargo-safety](https://github.com/alexkehayias/cargo-safety) | Provides safety checks for Rust projects by finding all uses of unsafe code in dependencies | Source Code | Unsafe code usage | Static Analysis | 2018-01-07 |
@@ -151,8 +153,11 @@ A curated list of awesome Rust analysis and verification tools, including linter
 | CRUST | CRUST: Towards a Unified Cross-Language Program Analysis Framework for Rust. [CRUST, QRS'22](https://ieeexplore.ieee.org/document/10062430) | 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](https://csslab-ustc.github.io/publications/2023/acorn.pdf) | 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](https://arxiv.org/abs/2401.01114) | MIR | Deadlock | Data-flow Analysis |
+| Yu Zhang | Two Birds One Stone: Effective Static Detection of Resource and Communication Deadlocks in Rust Programs. [Automated Software Engineering'26](https://arxiv.org/abs/2401.01114) | MIR | Resource deadlock, Communication deadlock | Data-flow Analysis |
 | Kaiwen Zhang | Automatically Transform Rust Source to Petri Nets for Checking Deadlocks. [Kaiwen Zhang](https://arxiv.org/abs/2212.02754) | MIR | Deadlock | Petri Nets |
 | RustC4 | Leveraging Large Language Model to Assist Detecting Rust Code Comment Inconsistency. [ASE'24](https://dl.acm.org/doi/10.1145/3691620.3695010) | AST | Code Comment Inconsistency | LLM |
+| RustC4++ | RustC4++: Improving Rust Code-Comment Inconsistency Detection via Hybrid LLM and Static Analysis. [OOPSLA'26](https://dl.acm.org/doi/epdf/10.1145/3800689) | AST | Code Comment Inconsistency | LLM, Static Analysis, SMT |
+| HALURust | HALURust: Exploiting Hallucinations of Large Language Models to Detect Vulnerabilities in Rust. [arXiv'25](https://arxiv.org/abs/2503.10793) | Source Code | Vulnerabilities | LLM, Static Analysis |
 | craft | Automated Fault Tree Generation for Rust Programs. [EDCC'24](https://doi.ieeecomputersociety.org/10.1109/EDCC61798.2024.00022) | - | Fault Tree | Static Program Analysis |
 | PanicFI | An Infrastructure for Fixing Panic Bugs in Real-World Rust Programs. [PanicFI](https://www.arxiv.org/pdf/2408.03262) | HIR, AST | Fixing Panic Bugs | Pattern Matching |
 | rustc++ | rustc++: Facilitating Advanced Analysis of Rust Code. [rustc++](https://dl.acm.org/doi/epdf/10.1145/3722041.3723102) | MIR, LLVM IR | Enhance MIR & pass metadata for analysis | Metadata |
@@ -168,6 +173,7 @@ A curated list of awesome Rust analysis and verification tools, including linter
 | Rust-twins | Automatic Rust Compiler Testing through Program Mutation and Dual Macros Generation. [ASE'24](https://wzyang.cn/files/Rust_twins.pdf) | AST, HIR | Rust compiler crashes and differences | Differential testing, mutation, macroize components, LLM |
 | LiteRSan | LiteRSan: Lightweight Memory Safety Via Rust-specific Program Analysis and Selective Instrumentation. [arxiv](https://arxiv.org/pdf/2509.16389) | MIR, LLVM IR | Memory access bugs | Fuzzing |
 | FRIES | Fuzzing Rust Library Interactions via Efficient Ecosystem-Guided Target Generation. [FRIES, ISSTA'24](https://dl.acm.org/doi/pdf/10.1145/3650212.3680348) | MIR | Rust API interactions | Fuzzing |
+| PanicKiller | Don't Panic! Finding Bugs Hidden Behind Rust Runtime Safety Checks. [CCS'25](https://dl.acm.org/doi/pdf/10.1145/3719027.3765142) | LLVM IR | Bugs hidden behind runtime safety checks | Cross-IR analysis, Dynamic taint analysis, Fuzzer |
 
 ### Verification Papers (no source code yet)
 
@@ -177,7 +183,7 @@ A curated list of awesome Rust analysis and verification tools, including linter
 | UnsafeCop | Towards Memory Safety for Real-World Unsafe Rust Code with Practical Bounded Model checking. [UnsafeCop, FM'24](https://link.springer.com/chapter/10.1007/978-3-031-71177-0_19) | - | Memory safety issues | Bounded Model Checking |
 | SAFE | Automated Proof Generation for Rust Code via Self-Evolution. [SAFE](https://arxiv.org/abs/2410.15756) | Rust Code With Docstring, Verus | - | Verus Verifier, LLM |
 | PanicCheck | Broadly Enabling KLEE to Effortlessly Find Unrecoverable Errors. [PanicCheck, ICSE-SEIP'24](https://doi.org/10.1145/3639477.3639714) | LLVM IR | Panic | KLEE |
-| [Converos](https://www.usenix.org/system/files/atc25-tang.pdf) | Converos: Practical Model Checking for Verifying Rust OS Kernel Concurrency. [ATC'25](https://www.usenix.org/system/files/atc25-tang.pdf) | PlusCal/TLA+ | Concurrency | Conformance Checking |
+| Converos | Converos: Practical Model Checking for Verifying Rust OS Kernel Concurrency. [ATC'25](https://www.usenix.org/system/files/atc25-tang.pdf) | PlusCal/TLA+ | Concurrency | Conformance Checking |
 
 ---