Verus
§1 Provenance Lattuada, Hance, Cho, Brun, Subasinghe, Zhou, Howell, Parno, Hawblitzel. "Verus: Verifying Rust Programs using Linear Ghost Types" , OOPSLA 2023 (PACMPL 7). https://www.microsoft.com/en-us/research/publication/verus-verifying-rust-programs-using-linear-ghost-types/ Lattuada et al. "Verus: A Practical Foundation for Systems Verification" , SOSP 2024. https://dl.acm.org/doi/10.1145/3694715.3695952 ; PDF https://www.cs.utexas.edu/~hleblanc/pdfs/verus.pdf AutoVerus (Wang et al., OOPSLA October 2025), LLM-assisted proof generation. https://www.microsoft.com/en-us/research/publication/autoverus-automated-proof-generation-for-rust-code/ VeriStruct (Sun, Sun, Amrollahi, Zhang, Lahiri, Lu, Dill, Barrett, TACAS April 2026), AI-assisted verification of data-structure modules...