This seems like the perfect time to misquote Groucho Marx: "This is so simple a child of 5 could prove it. Somebody bring me a child of 5!"
In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes.
This will, however, not protect against deeper issues that are common to all N provers. e.g. Potential biases or mistaken assumptions in the formal verification comunity.
At the end of the day, it is an engineering decision. How much of the available resources are you willing to through at the practical problem of making your implementation approach asymptotically to the theoretical limits. The fact that those limits is indeed a peg or two below perfection is an independent issue.
I strongly advise that to deal with both mistakes and subversion. Mutually-suspicious parties in various countries using different logics, compilers, hardware, etc. with a common, executable spec that's basically state machines or functions. That way they get same output from same input.
So, when I saw Milawa was verified first-order, I immediately looked for other verifications of first-order provers (found 1). Then the idea would be diverse implementations of executable parts of that stack with diverse reviews of logic combinations they did. Exhaustive testing done by each party. Even do implementations of key parts of TCB in other logics to check results. The prover with its code is trustworthy when everyone got the same results on same logics, code, shared tests, and individual tests. Plus have paper copies of the resulting text files with hashes stashed away somewhere in case a nation-state wants to throw money at countering diversity via hacking host systems. ;)
Then we rinse and repeat for more complex provers. The fun never stops in this game.
In practice, even much simpler theorems would already raise our confidence a lot. E.g., the inference rules of Coq can be stated in a couple of pages of text, but the kernel checker that you need to trust is 14k lines of OCaml. A proof that the checker actually correctly implements the inference rules would already catch the majority of the bugs that happen in practice. Because of Gödel we then can't hope for a proof in Coq that there is no way to use those inference rules to derive False, but that's less of a concern.