Peter Smith in "An Introduction to Gödel's Theorems" presents a broadly Hilbertian argument (in the sense of Hilbert's program) on page 276 (2nd edition):
Theorem 37.2 If $I$ is consistent and extends $Q$, and if contentual mathematics extends no further than $\Pi_1$ propositions of arithmetic, then $I$ is real-sound.
Proof: This is just half of Theorem 11.7 in our new jargon, since $\Pi_1$-soundness implies real-soundness if contentual mathematics extends no further than the $\Pi_1$ propositions of arithmetic.
Theorem 11.7 is: If $T$ extends $Q$, $T$ is consistent iff it is $\Pi_1$-sound. Here $Q$ is of course Robinson arithmetic.
An issue I have with Smith's argument is that to really make sense in a Hilbertian framework, shouldn't it be finitarily acceptable? Let's say formalizable in PRA, following Tait. Can we formalize Theorem 11.7 in PRA? In particular, does PRA have a partial truth predicate like PA? This seems necessary to formalize and work with $\Pi_1$-soundness.