Well, seL4 has verifications of it's mixed-criticality hard-real-time guarantees (sufficiently tight bounds on scheduling latency (and such) to be useful) and data diode functionalities, and it's isolation properties have been verified not just at a fine-grained specification level but at a high-level human-readable level of invariant description. It doesn't cover timing and maybe some kinds of similar, other, side channels, but it's still extremely useful.
Formal verification shines in two situations: complicated optimized algorithms with a naive reference implementation you want to confirm equivalent, and high-level behavioral invariants of complex systems (like seL4's capability system, or a cluster database's consistency during literally all possible failover scenarios).
> with a naive reference implementation you want to confirm equivalent
I'm guessing you know this but in type theories like Agda you can just specify that the input and output to an algorithm has the desired properties, rather than needing to specify any reference algorithms. For example, you can just state that an implementation takes a list of X and that it outputs a sorted list of X. Nothing more is necessary in cases like that in such a system, no code, just the single type.
Well, yes, that falls under the second case: behavioral invariants of complex systems.
And the reference for "sorting" could likely be a deterministic bogosort and certainly a primitive bubblesort.
Even if you're just looking at sorting stability, you're past what your simple "sorted" type would cover.
Most things are far less trivial than "sorted list", including (almost?) all interesting practical applications of formal verification in the life of a "normal" software engineer.
Formal verification shines in two situations: complicated optimized algorithms with a naive reference implementation you want to confirm equivalent, and high-level behavioral invariants of complex systems (like seL4's capability system, or a cluster database's consistency during literally all possible failover scenarios).