No. The whole point of the LCF approach is that only kernel functions can generate theorems. Usually this is done by having a Thm module with opaque thm type (so its instances can only be generated by this module) and embedding the base rules of your logical calculus as shallow functions into that Thm module. Thus, all thm objects are correct by construction (w.r.t. your calculus), and you only need to check the Thm module to verify this.

Tactics generate thms by calling functions of the Thm module in some fashion.

This does not resolve the issue of how to ensure that the "module" system is itself sound and has no unforeseen escape hatches. You have to assume that it is, or else include a complete programming language implementation as part of your TCB. If your system generates proof objects (possibly allowing for some kind of reflection, with the proof objects merely specifying some kind of computation) you can skip this and simply prove that the kernel itself is correct.