> single verification use case where all I want to check is the absence of panic.

Basically any decoder/deserializer. It might be sufficient to handle the correctness in tests but panics are the most severe thing you want to avoid.

How well `#[no_panic]` actually works in practice?

There might be cases where e.g. index access violation never happen but compiler might still think that it happes. I could be impossible to restructure code without adding some performance overhead.

#[no_panic] has false-positives, but no false-negatives. If it’s present, the code won’t panic and can’t panic.

Index access violation that “never happens” is the root of every buffer overflow, so I’m absolutely OK with the minimal overhead behind the bounds check for actual safety