Verification: how 'formal' is a tool like Java Modeling Language (JML) compared to certified libraries and model checking?
This is a strange comparison. Your question is comparable to asking "how expressive is the ANSI C language specification compared to stdlib and compilation". The comparisons don't make sense.


The Java Modelling Language can be used as a specification language to specify properties of code. The language alone does not solve the problem of verifying whether these properties are satisfied.
A model checker allows you to check if a system with a transition system semantics satisfies a logical formula. The formula is typically written in a propositional temporal or modal logic though first-order and other extensions exist. Nonetheless, most model checkers used in practice do not support specification languages with quantifiers. I do not know of a model checker that supports a specification language as rich as JML. 
A certified library contains code that provides certain guarantees. Those guarantees may have been provided using a theorem prover, or a model checker, or by doing a  manual proof. 


If you want a mathematical comparison, to me, it's like comparing the formulae of first order arithmetic (a language), the principle of induction (a proof technique) and a collection of theorems in a number theory textbook. They are related concepts but they do not achieve the same goal so comparing them does not make sense.