I like the "small kernel" approach of HOL Light (or was it already LCF?),
Yes, LCF already I think.
and think that it is really very useful and "trust-encouraging". But I
think it still requires quite some trust, assumptions, and knowledge about
the implementation, when you say that thousands of additional lines of
code "are safe" provided the small kernel is.
Why? When in HOL I have an object of ML type "thm", I _know_
that the statement of that theorem will be provable in the
HOL logic. (Provided that there are no bugs in the kernel,
of course.) It's the power of abstract datatypes. So what
are the assumptions and knowledge of the implementation
that you're referring to?