At least in Isabelle/ML, it seems like in practice there are also untrusted "oracles" that a proof can invoke to generate "thm" objects [0], and it's not entirely trivial to automatically ensure that only trusted sources are used in a project [1], unless I am misunderstanding the linked thread.

Of course there's no free lunch, as you say, in making sure that high-level proofs are lowered into the trusted part correctly, but it's certainly a piece that should ideally be as simple as possible.

[0] https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2025-02/...

[1] https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2025-02/...

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.

The question: "does the ambient programming language do the right thing?" applies to other provers too. So if you assume the semantics of the implementation language is broken, or the compiler, or the computer executing the code, then those issues also need to be added to the TBC of Curry-Howard provers.

There is no free lunch.