#113
in
Rust
> those applications need the proof for correctness so that more dangerous code---say, what would need `unsafe` in Rust---can be safely added
There are actually already tools built for this very purpose in Rust (see Kani [1] for instance).
Formal verification has a serious scaling problem, so forming programs in such a way that there are a few performance-critical areas that use unsafe routines seems like the best route. I feel like Rust leans into this paradigm with `unsafe` blocks.
The blog post about verifying ChatGPT code with Kani is very interesting. [0]
It introduced me to model checking with Kani [1], which seems to be very similar to fuzzing, but with a different goal and underlying algorithm. Fuzzy testing involves random byte sequences whereas Kani's approach is exhaustive, while using some techniques to reduce the search space if possible.
[0]: https://medium.com/@carlmkadie/check-ai-generated-code-perfe...
Looks like that the project has changed its name from "rmc" (Rust Model Checker) to this. Various sources point to rmc as https://github.com/model-checking/rmc (redirected to https://github.com/model-checking/kani) and https://model-checking.github.io/rmc/ (404). Anyone knows why?