[tzs]

In the case of formal verification done with proof assistants or similar, I believe the way it works is something like this.

The people who develop such software start out writing a verifier for a much system of logic or programming than what the final system will handle. This first system is sufficiently simple that the verifier that can verify programs in that system is very small and straightforward, so that if several humans look at it and can't see any bugs it is almost certainly correct.

Then they write a verifier for a more expressive system. This verify isn't as small or straightforward and so even if humans don't see any bugs we can't be confident that there none. They then use the first verifier to verify the second verifier. The formal proof of correctness might be long and difficult to develop because it can only use the reduced logic of the first verifier, but once they manage that and the first verifier verifies it, they can be confident that the second verifier is correct.

If the system the second verifier still isn't expressive enough to verify the things they ultimately want to handle they write an even more expressive system, and use the second verifier to verify that.

Repeat until you've got the system you wanted in the first place.