I specifically mentioned in my post that problems related to _proof search_ are undecidable. Coq's tactics for proof search are unreliable. They rely on timeouts and tend to fail ("omega can't solve this system").

So you're not arguing with my post.

The question you were answering was not talking about proof search. It was merely asking whether it was possible to do verification in the same language that the program is written in. And, contrary to your response, it is possible to do verification in the same language as the program is written in. Coq is an example of that.

Yes, proof search is undecidable. But that's not what we're talking about in this thread. seL4 isn't verified by proof search. The proofs were provided by humans (with limited automation).