Verification: how 'formal' is a tool like Java Modeling Language (JML) compared to certified libraries and model checking? (note: this is probably a beginner question, and English is not my first language)

Recently, I have read a paper that used the “Java Modeling Language” (JML), see for instance:

http://www.eecs.ucf.edu/~leavens/JML//index.shtml
http://www.eecs.ucf.edu/~leavens/JML/fmco.pdf  

a) certified Software
To my understanding, a sorting algorithm proven correct in the theorem prover Coq (and possibly extracted to an ocaml program) is "certified software" or formally verified software, as a mathematical proof of the correctness can be extracted and possibly manually verified.

b) model checking
software verified via model checking is not certified or formally verified software, as the model checker has to be trusted.

How does the "Java Modeling Language" (JML) compare for verification purposes?

Okay, I think I get it. It is not about software verification, as it is stated that:

The contracts are defined by program code
in the programming language itself, and are trans-
lated into executable code by the compiler. Thus,
any violation of the contract that occurs while the
program is running can be detected immediately.

I cannot find a real example of verification in the above paper, at least not in the sense of model checking or certified software, so I guess they just don't have an emphasis on formal methods.
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.