> It’s correct to flag this code. The check is performed manually outside of the function in question. If you call the function directly, the bug surfaces.

No, that’s just called a precondition. I’m not aware of a single program that doesn’t have functions like these, particularly internal APIs.

(It should go without saying, but it’s not even an issue in this case: it’ll cause an IndexError, but so will thousands of other APIs. Python very explicitly doesn’t have exceptions in its type contract; anything can always raise anything.)

> I would expect something more rigorous from verified code.

Nobody said that requests is “formally verified.” The only place where that claim is made is in the AI-generated blog post above.