Dear Oleg,

thank you for the references. This is very useful and I will take the 
references into account in the project with Chris Stone, see 
http://math.andrej.com/rz. Our tool is slanted towards specification 
construction (not verification) from mathematical defintions. We plan to 
use it for real number computation and computable mathematical analysis.

In fact, I think Chris mentioned SPARK the other day and how we should 
have a look at it.

Best regards,

Andrej