Whiley ist eine Programmiersprache, die auf die Java Virtual Machine (JVM) ausgerichtet ist. Sie wird von der Whiley Development Group an der University of Queensland, Australien, entwickelt und gepflegt.
Whiley ist statisch und stark typisiert. Es unterstützt Datentypen wie Ganzzahlen, Fließkommazahlen, Zeichen, Strings, Booleans und Null. Whiley unterstützt auch benutzerdefinierte Datentypen und Typparameter.
Whiley hat eine Reihe von Eigenschaften, die es für die Verifikation geeignet machen. Dazu gehören ein umfangreicher Satz logischer Operatoren, erstklassige Prädikatsfunktionen und die Möglichkeit, Annahmen und Behauptungen über das Programmverhalten festzulegen. Whiley ist außerdem einfach und leicht zu erlernen.