It's a different proof assistant that can convert Coq's (and other P.A.) proofs into its own language and check them. It's not a guarantee of course, both Coq and Dedukti could have a similar bug. But it certainly helps having independent implementations being able to check the same proofs.
We're talking proofs here tho, and you aren't allowed to prove something by "throwing enough input at it", isn't it like saying that unit tests are proofs of the correctness of a program?
Well perhaps you could actually prove the correctness of coq itself.
In any case it's just a matter of reliability in the traditional sense: we're going to end with a small set of statements that will have to be verified by humans upon which we can rest everything else. Those statements will need enough people looking at them to get a level of certainty we're comfortable with.
I believe the risk of a major flaw going unnoticed is astronomically low, and the good thing is this certainty propagates all the way to modern proofs if we take care to go through formal verification.
That's no different from how regular math works. The whole point of this article is that mathematics is not formally verified today -- mathematicians just spot check and probe suspicious parts using informal analysis.
It's a different proof assistant that can convert Coq's (and other P.A.) proofs into its own language and check them. It's not a guarantee of course, both Coq and Dedukti could have a similar bug. But it certainly helps having independent implementations being able to check the same proofs.