Hacker News
- Compiling C to Safe Rust, Formalized https://arxiv.org/abs/2412.15042 157 comments
- Translation of Rust's core and alloc crates to Coq for formal verification https://formal.land/blog/2024/04/26/translation-core-alloc-crates 116 comments
- CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot https://github.com/sarsko/CreuSAT 72 comments
- Oxide: A Formal Semantics for Rust https://arxiv.org/abs/1903.00982 30 comments
- Rust Formal Verification Working Group https://internals.rust-lang.org/t/announcing-the-formal-verification-working-group/7240 9 comments
- A Formal Verification of Rust's Binary Search Implementation https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html 26 comments
- Some notes on Rust, mutable aliasing and formal verification https://graydon2.dreamwidth.org/312681.html 145 comments
Lobsters
- CreuSAT: A formally verified SAT solver written in Rust https://github.com/sarsko/CreuSAT 4 comments formalmethods , rust
- Rust's ownership model formally proven with Coq https://dl.acm.org/citation.cfm?doid=3177123.3158154 3 comments compsci , formalmethods , rust
- [2412.15042] Compiling C to Safe Rust, Formalized https://arxiv.org/abs/2412.15042 8 comments rust
- Writing a formal compiler in Rust None 2 comments programminglanguages
- What Rust Got Wrong on Formal Verification https://gavinhoward.com/2024/05/what-rust-got-wrong-on-formal-verification/ 2 comments ada
- What Rust Got Wrong on Formal Verification https://gavinhoward.com/2024/05/what-rust-got-wrong-on-formal-verification/ 99 comments programming
- CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot https://github.com/sarsko/CreuSAT 7 comments rust
- From Rust to SPARK: Formally Proven Bip-Buffers https://blog.adacore.com/from-rust-to-spark-formally-proven-bip-buffers 3 comments rust
- From Rust to SPARK: Formally Proven Bip-Buffers https://blog.adacore.com/from-rust-to-spark-formally-proven-bip-buffers 4 comments rust
- Oxide: A Formal Semantics for Rust https://arxiv.org/abs/1903.00982 41 comments rust
- KRust: A Formal Executable Semantics of Rust https://arxiv.org/abs/1804.10806 18 comments rust
- A Formal Verification of Rust's Binary Search Implementation https://kha.github.io/2016/07/22/formally-verifying-rusts-binary-search.html 17 comments rust
- Formalizing Rust https://www.ralfj.de/blog/2015/10/12/formalizing-rust.html 29 comments programming
- Formalizing Rust https://www.ralfj.de/blog/2015/10/12/formalizing-rust.html 33 comments rust
- Some notes on Rust, mutable aliasing and formal verification https://graydon2.dreamwidth.org/312681.html 4 comments programminglanguages
- Some notes on Rust, mutable aliasing and formal verification https://graydon2.dreamwidth.org/312681.html 5 comments rust
- Nine Rules to Formally Validate Rust Algorithms with Dafny https://medium.com/towards-data-science/nine-rules-to-formally-validate-rust-algorithms-with-dafny-part-1-5cb8c8a0bb92 7 comments rust
- Paper on formally verifying iterators in Rust https://hal.science/hal-03827702v2/document 10 comments rust
- Rustls, the TLS implementation in Rust, just got a formal audit! https://github.com/ctz/rustls/blob/master/audit/tls-01-report.pdf 64 comments rust
- Papers on Rust's influences, formal studies, etc. https://forge.rust-lang.org/bibliography.html 7 comments rust
- Borrow checking formalized, in only 9 lines, using Avalog (an experimental automated theorem prover for Avatar Logic written in Rust) https://github.com/advancedresearch/avalog/blob/master/source/borrowchk.txt 35 comments rust
- TLA+ formalization of queue lock algorithm implemented in Rust. https://sstewartgallus.com/git?p=qlock.git;a=blob;f=tla/stacklock.tla;h=2bc21659b870bb94af1ff093851d51481e8d1bf0;hb=head 6 comments rust
- Rust Paris meetup: Talks on Rust formalization, Rayon, Tokio https://air.mozilla.org/rust-paris-meetup-35-2017-01-19/ 4 comments rust
- Patina: A Formalization of the Rust Programming Language ftp://ftp.cs.washington.edu/tr/2015/03/uw-cse-15-03-02.pdf 26 comments rust
- Aeneas, a formal verification toolchain for translating Rust programs to functional models in a variety of proof assistants https://aeneasverif.github.io/ 6 comments rust
- Rustls, the TLS implementation in Rust, got a formal audit! Auditors "incredibly impressed" https://github.com/ctz/rustls/blob/master/audit/tls-01-report.pdf 120 comments linux
- RFC to formally establish the existence of pointer provenance in Rust, by Ralf Jung https://github.com/rust-lang/rfcs/pull/3559 45 comments rust
- Oxide: The Essence of Rust — a research paper formalizing the ownership model & the borrow checker https://arxiv.org/abs/1903.00982 3 comments rust
- How much does it matter that Rust isn't formally specified? And general conversation regarding the choice of using Rust versus other languages. https://www.reddit.com/r/rust/comments/77ze0k/how_much_does_it_matter_that_rust_isnt_formally/ 45 comments rust
- A Hoare Logic for Rust - by Redox dev Ticki (being used in possible formalization of redox kernel) http://ticki.github.io/blog/a-hoare-logic-for-rust/ 2 comments redox
- Category Theory formalized in Avalog V0.3.3 - An experimental implementation of Avatar Logic with a Prolog-like syntax, written in Rust https://github.com/advancedresearch/avalog/blob/master/source/category.txt 10 comments rust
- "Modular Formal Verification of Rust Programs with Unsafe Blocks", by Nima Rahimi Foroushaani and Bart Jacobs. "[W]e are trying to verify soundness of Rust unsafe code applying our Modular Symbolic Execution algorithm. This text outlines our ... progress thus far." [abstract + link to PDF, 23pp] https://arxiv.org/abs/2212.12976 26 comments rust
- Ralf Jung ...receives Honorable Mention for the 2020 ACM Doctoral Dissertation Award. ... Jung’s dissertation, “Understanding and Evolving the Rust Programming Language,” established the first formal foundations for safe systems programming in the innovative programming language Rust. https://www.acm.org/media-center/2021/july/dissertation-award-2020 8 comments rust