> I'm thinking there must be a reason they do not mention F* , Coq, Agda, and Idris The ones they do mention are all imperative languages with added deductive

> I'm thinking there must be a reason they do not mention F* , Coq, Agda, and Idris The ones they do mention are all imperative languages with added deductive verification in a Hoare calculus style (think loop invariants). The ones you mention are functional languages with a different style of proof (think inductive proofs). Of course there are overlaps between the two styles (notably in Why3), but there are pronounced differences between them.