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 th

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).