For systems like Coq that are based on type theory, this question is trickier to answer than you might expect.

First of all, what does it take to "know" the consistency strength of some system? Classically, the most thoroughly studied logical systems are based on first-order logic, using either the language of elementary arithmetic or the language of set theory. So if you are able to say, "System X is equiconsistent with ZF" (or with PA, or PRA, or ZFC + infinitely many inaccessibles, etc.), then most people will feel that they "know" the consistency strength of X, because you have calibrated it against a familiar hierarchy of systems.

Coq, however, is based on something called the Calculus of Inductive Constructions (CIC). Without going into a detailed explanation of what this is, let me just mention that the core of CIC doesn't have any axioms, but typically people add axioms as needed. For example, if you want classical logic, then you can add the law of the excluded middle as an axiom. To get more power you can add more axioms (though you have to be careful because certain combinations of axioms are known to be inconsistent). But trying to line up the various systems you can get this way against more familiar set-theoretic or arithmetic systems is a tricky business. Typically, we cannot expect an exact calibration, but we can interpret various fragments of set theory in type theory and vice versa, showing that the consistency of CIC plus certain axioms is sandwiched between two different systems on the set-theoretic side. If you want to delve into the details, I'd recommend the paper Sets in Coq, Coq in Sets by Bruno Barras as a starting point.

fullformal system of Coq described/proved" (I couldn't find such, found articles covering parts of the code...) $\endgroup$ – joro Jun 15 '11 at 7:53