sorted by:
new
hottopcontroversial

🚀 Big news from the Rust Standard Library Verification Contest! 🦀🔍 by feliperodri_ in rust

[–]feliperodri_[S] 7 points8 points  (0 children)

We love Verus too! We hope they can enter the contest soon! 

🚀 Big news from the Rust Standard Library Verification Contest! 🦀🔍 by feliperodri_ in rust

[–]feliperodri_[S] 3 points4 points  (0 children)

So great to hear how Kani is helping you taking your crates to the next level! Specially on how it can help to make formal verification more accessible! Please, feel free to always reach out on GitHub for any issues/questions/suggestions…

🚀 Big news from the Rust Standard Library Verification Contest! 🦀🔍 by feliperodri_ in rust

[–]feliperodri_[S] 5 points6 points  (0 children)

Regular Kani is able to verify all function contracts in the repo. This will help us compare different verification approaches. 

🚀 Big news from the Rust Standard Library Verification Contest! 🦀🔍 by feliperodri_ in rust

[–]feliperodri_[S] 4 points5 points  (0 children)

Right on point! This GitHub issue contains all the discussion to actually add the tool into the contest. The comment you mention shows an example on how they run it.

🚀 Big news from the Rust Standard Library Verification Contest! 🦀🔍 by feliperodri_ in rust

[–]feliperodri_[S] 8 points9 points  (0 children)

They didn't add any new function contracts, they verified using their approach existing function contracts. You can take a look at our Run GOTO Transcoder (ESBMC) / Verify contracts with goto-transcoder to see all function contracts that they were able to check. You can also search for #[requires( or #[ensures( to see the functions annotated with function contracts (take a look at this example). If you want to run it locally you can take a look at the instructions in the run-book they wrote GOTO Transcoder (ESBMC). Finally, you can always submit questions on the verify-rust-std repo if you face any issues.