There are multiple senses of "correct" you may want to invoke.
A) - good predictions. If by "correct" you mean "has useful predictions", than cross validation (or better: validation on new external data), using a proper scoring rule is probably the way to go. A good proper scoring rule is the log predictive density - this is what is implemented in the loo
package which provides ways to approximate leave-one-out cross-validation in an efficient manner. See also A. Vehtari's excellent Cross validation FAQ
Often it also makes sense to evaluate predictions by a scoring rule derived from your application (e.g. in business contexts you may want to try to evaluate the dollar cost/benefit of predictions).
B) - matches data. If by "correct" you mean "matches the true data-generating process", then posterior predictive checks (PPC) are a good way to go. Note that in practice PPCs are almost exclusively used with samples, so there should be no problem. You just take the samples of a quantity from your posterior and compare this distribution to the observed value of the quantity. If the observed value is extreme in respect to the posterior, it signals a problem.
See the section on PPCs in the Bayesian workflow preprint for some simple examples and some context (full disclosure, I am a co-author). The bayesplot
package has further examples in their vignette on PPC.
C) correct computation. If by "correct" you mean "the computed posterior matches the theoretical posterior for the given model", then a strong (but computationally expensive) check is provided by simulation-based calibration checking (SBC, see Modrák et al., Bayesian analysis for a recent take on this, disclosure: I am the author). Checking prediction calibration (e.g. that 95% posterior credible interval contains the true value in 95% of the cases) can be understood as a special case of SBC - happy to elaborate more if that's what you are interested in. The linked paper surveys other possibilities. Since it was written, some closely related checks/extensions by Lemos et al. 2023, Yao & Domke 2023 came out.
Note that all of the three senses of "correct" are largely independent and one does not imply any of the others, i.e. your model may satisfy any arbitrary subset of those conditions.