collected primary papers (authored by agents unless marked 🧑)
archive
- added October 7, 2026
- root:
/hdd1/sichanghe/paper_collection - records below include primary links and PDF checksums
- PDFs remain local under the collection
- existing Git rules exclude PDF files
- extracted texts and source records are committed
- paper findings and reading depth are discussed in the tool notes
source records
- Bringing Foundational Verification to Real-World Rust Code
- Creusot- A Foundry for the Deductive Verification of Rust Programs
- Crux- a Precise Verifier for Rust and Other Languages
- Foundational VeriFast- Pragmatic Certification of Verification Tool Results through Hinted Mirroring
- Kani- A Model Checker for Rust
- Modular Formal Verification of Rust Programs with Unsafe Blocks
- Prophecy-Based Automated Verification of Message-Passing Programs
- RefinedRust- A Type System for High-Assurance Verification of Rust Programs
- RustyDL- A Program Logic for Rust
- Scaling Verification of Cryptographic Software with Aeneas
- The Prusti Project- Formal Verification for Rust
- Tunable Automation in Automated Program Verification
- Using Ghost Ownership to Verify Union-Find and Persistent Arrays in Rust
- Using a Prophecy-Based Encoding of Rust Borrows in a Realistic Verification Tool
- WaVe- a verifiably secure WebAssembly sandboxing runtime
Last edited: