formal-land/rocq-of-rust
View on GitHub ↗ ★ 1,197 Rocq Prover
Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.
3 mentions on Hacker News by 3 people: 1 story, 2 comments · first 2024-05-15 · latest 2025-05-14
20082026
-
…- there's some cool ideas here like transpiling Rust into languages for formal verification. See https://github.com/formal-land/coq-of-rust as an example. Formal verification was one of those things that was previously so annoying to do…
comment by mindwok · 2025-05-14 · in Type-constrained code generation with language models -
▲ 159
Coq-of-rust: Formal verification tool for Ruststory by todsacerdoti · 2025-03-14 · 42 comments
-
…masters students I know, etc.). [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib
comment by thaliaarchi · 2024-05-15 · in Translation of Rust's core and alloc crates to Coq for formal verification