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.
So you're not arguing with my post.
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).