I just wanted to post similar comment.
But I don't think it's impossible. You 'simply' need to audit machine code of one version of
gcc (statically linked) and one version of kernel.
Then you publish this gcc and kernel along with source and then anyone can verify object code
by recompiling it with published certified gcc launched on certified kernel.
Via source code review and usage of certified tools you can then certify other versions of gcc
and kernel more easily.
Something like this should work I think.