> I would expect something more rigorous from verified code.

I think you just want the illusion of safety :p

A big advantage of verified code is that it enables you to write the sketchy and dangerous-looking code BECAUSE it's proven correct

In fact, skipping as many safety checks as possible is highly desirable. For performance, yes, but also because it's less code to maintain.

Our tools already do this to some extent, for performance. E.g. compilers that remove your bounds or type checks in the generated code when it can prove it's not needed.