You're looking for foundational, proof-carrying code with verified logins. I can't find the verified logic right now, though. Examples:

https://www.cs.princeton.edu/~appel/papers/fpcc.pdf

https://hol-light.github.io/

I'll also add that mutation testing has found specification errors, too.

https://github.com/EngineeringSoftware/mcoq

I've heard that called "validation". In other words, you verify that your solution meets the problem specification, but you validate that your specification is actually what you need.