I would like to mention that Coq is also used to extract _verified implementations_ rather than model checking abstract algorithm design (as in TLA+). This prop

I would like to mention that Coq is also used to extract _verified implementations_ rather than model checking abstract algorithm design (as in TLA+). This property might be very desirable depending on situation. As for me this property looks very appealing.