[caffeine]

I just wish there was an ergonomic way of saying “Please check if the following code can possibly panic, and fail to compile if it can.”

That would allow critical sections that happen to use a library not to need to audit all the code in the library for panics.

[slavak]

You might be interested in Prusti: https://github.com/viperproject/prusti-dev