How does Ada/Spark compare to theorem provers like Agda and Lean, in terms of guarantees?

I’m not really into languages like this. Anybody got some resources regarding how strict the guarantees can get in either of these types of environments?