Whiley est un langage de programmation conçu pour cibler la machine virtuelle Java (JVM). Il est développé et maintenu par le Whiley Development Group de l'Université de Queensland, en Australie.
Whiley est statiquement et fortement typé. Il supporte des types de données tels que les entiers, les nombres à virgule flottante, les caractères, les chaînes de caractères, les booléens et les null. Whiley supporte également les types de données définis par l'utilisateur et les paramètres de type.
Whiley possède un certain nombre de caractéristiques qui le rendent approprié pour la vérification. Celles-ci incluent un riche ensemble d'opérateurs logiques, des fonctions prédicats de première classe, et la possibilité de spécifier des hypothèses et des assertions sur le comportement du programme. Whiley est également conçu pour être simple et facile à apprendre.