search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.12k stars 83 forks source link

Create std contracts regression for features/verify-rust-std #3094

Open celinval opened 5 months ago

celinval commented 5 months ago

Proposed change: Create a regression that checks std library contracts. I propose we use stubs to verify the contracts without having to fork the standard library for now.

Motivation: The standard library is a great verification candidate and being able to add contracts to some of their public API can benefit Kani users directly and indirectly.

celinval commented 2 months ago

Changing this to create a job to verify the standard library fork (https://github.com/model-checking/verify-rust-std).

The job itself should take the branch as an input parameter. We could use that to automatically merge main into features/verify-rust-std branch, and potentially create a "unstable" release.