One is always going to sit between two extremes. On one extreme we can't be 100% fully certain of anything. For example, we might be living in a computer simulation, or it might be that every axiom system we have ever dealt with (Peano Arithmetic, ZFC, DTT) are all inconsistent.
On the other extreme, a lot of thought and care has gone into building proof assistants and it would be reckless to say they obviously have fatal bugs just because they are software, or they are obviously no better than any other ad-hoc computer checked proof such as the original four color theorem proof.
The middle ground is that proof assistants are unparalleled in their attention to robust guarantees but they also try to be practical systems, and bugs do sometimes creep in. More and more work has goes into making bugs less likely.
There is a phrase in this field called trusted computing base meaning basically all the components you have to trust to trust your end result. This includes the software as well as the hardware.
The main line of defense in a proof assistant is a small kernel. While a proof assistants may provide a great deal of automation and user tools, those tools just construct (and communicate) the proof. The kernel is the part that actually checks the proof. HOL-Light famously has one of the smallest kernels at just about 400 lines of OCaml code. DTT kernels in say Lean and Coq are usually larger since the logic is more complicated, but even Lean's kernel for example tries to stay small and be very robustly checked.
Another advantage of a kernel is that if one day a bug is found (there were two bugs found in say the HOL Light kernel over time) then all proofs can be rechecked with the fixed kernel. This still requires that the proof hasn't bit rotted, etc, but it does provide a way to quickly recover from errors.
Also, the kernel can export the proof. Then the proof can be checked in another implementation of the kernel. Lean for example has a number of external checkers which reimplement Lean's kernel. If I understand correctly, they are regularly run over the exported term proofs of Lean's main mathematical library
mathlib. Also, it is possible (although I don't know it is done in practice) to check Lean's term proofs in Coq. Similarly, I think there are other similar tools for many of the other proof assistants. These tools don't guarantee that the full implementation of the logic is correct, but just that the current proofs follow the logic as implemented in all the checkers. This significantly reduces the possibility of a bug due to an error in implementing the logic.
As for the logics themselves, it is advisable to use standard logics which are well understood. While it can be nice to add new features, they run the risk of introducing inconsistencies. HOL-Light has actually formally verified that their logic is consistent. (They avoid Gödel's incompleteness theorem by verifying Con(HOL - Infinity) in HOL, and Con(HOL) in Con(HOL + large cardinals) or something like that.) Mario Carnerio's thesis gives a pen and paper proof of Lean's consistency including all the implementation features.
Other provers go further and try to verify the actual code implementing the prover. I don't know a lot about this, but CakeML and Coq in Coq are projects along this line.
A new project is Mario Carneiro's Metamath Zero which plans to be an external checker for all logics which has a formally verified
implementation done to the x86 byte code. Further, Mario has done a lot of thinking about what parts still need to be human inspected such as the axioms of the logic and the statements of the theorems and definitions used in the final result. (The statements of the lemmas and intermediate definitions don't matter to correctness if you trust the kernel.)
On a practical side, a major source of errors in math proofs is just missing cases, or thinking something is obvious when it isn't. Proof assistants force you to deal with those explicitly. This is even more an issue when verifying hardware and software since a proof of correctness of say an implementation of floating point arithmetic doesn't have the beauty of the proof of say FLT. While the latter is much more complicated, it is also built on a number of beautiful mathematical ideas. Whereas, forgetting one value in a table could make it so that your algorithm implementing floating point numbers is wrong. Therefore, proof assistants provide a larger value add for software and hardware verification than mathematical theorems.
Even if a kernel as a bug, to get a wrong result you usually have to be meticulously exploit that bug. This may involve invoking logical inconstancies like in Russel's paradox, or carefully abusing variables in an unnatural way. (Or it may even require you to exploit the programming language used under the kernel.) As such, it is unlikely that a proof written by a competent and trustworthy human would succumb to those bugs. Nonetheless, as automation and AI becomes more common in theorem proving, maybe it is more likely that an AI just trained to find proofs could learn to exploit a bug. Similarly, imagine if one is paying someone over the Internet to prove theorems for you. Can you really trust that they have the integrity to not exploit a bug? (Similarly for theorem proving competitions?) Last, what if someone no one has ever heard of claims to have a formal proof of the Reimann Hypothesis in Coq? I would strongly imagine that the Clay Foundation would put a lot of work into understanding the proof and ways to double check it rather than just except Coq's output. So the motivation and trustworthiness of the user, as well as the importance of the result, probably matters here as well.
Last, as a user you have to know how to use the system correctly. All these systems have back doors where you can use
CHEAT_TAC, etc to temporarily fill in a hole of the proof. You have to know how to look for those in the end. (And sometimes they are not named what you think they are. Lean has a few synonyms for
sorry.) Also, theorem provers usually provide the ability to add custom axioms, so you have to check which axioms are used in the proof. Even in Lean if you don't see any red squiggles, it could be because of an axiom, or even just that the Lean front end crashed.
Similarly, sometimes definitions don't behave as you think. An obvious example is that in many systems
1 / 0 = 0 for practical reasons. So your should understand the definitions you are working with (especially at edge cases).
Also, as a user you have to pick a system which a lot of quality work has gone into. Some proof assistants are just playgrounds for ideas and have known logical inconsistencies like
Type : Type. This is fine if you know how to avoid this, but take it into account. Whereas Lean, Isabelle, Coq, Metamath, Mizar, HOL-Light and many others have put a lot more work into making everything as air tight as they can.
So to summarize, if you know how to use the system, I wouldn't worry too much practically. Nonetheless, this is still an ongoing area of research, especially if you want to make your system robust against adversarial exploitation (or against skeptics who don't trust anything).