Per the Wikipedia page for Whiley[1] the languages akin to Dafny are mentioned when explaining what Whiley is: “The primary purpose of such a tool is to improve software quality by ensuring a program meets a formal specification. In other words, to help identify and eliminate software bug in the programs being developed. Whiley follows many attempts to develop such tools, including notable efforts such as SPARK/Ada, ESC/Java, Spec#, Dafny, Why3 and Frama-C.”

I'm thinking there must be a reason they do not mention F*, Coq, Agda, and Idris, perhaps because they are proof assistants[2] rather than automatic provers of programs with formal specifications. See also Isabelle and others. Regarding Idris (which you mention but is not on that page) and Epigram (which is noteworthy and again not on that page), neither are production ready and the latter is unmaintained.

[1] https://en.wikipedia.org/wiki/Whiley_(programming_language)#...

[2] https://en.wikipedia.org/wiki/Proof_assistant

> 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.

Ok. But that's not what I was getting at.

> I also recall some Java extension but can't find it atm.

You might be thinking of JML (Java Modeling Language): http://www.eecs.ucf.edu/~leavens/JML//index.shtml Apparently JML-annotated programs can passed to Why3 using a confusingly documented set of tools: http://krakatoa.lri.fr/

There is also the Cheker Framework for Java: http://types.cs.washington.edu/checker-framework/ But as far as I understand it's less general than all the other tools you mention.

Also, and probably even more likely than the ones I mentioned above, there is KeY for Java verification: http://www.key-project.org/index.php