Le profil Ravenscar est un sous ensemble du langage Ada dédié aux systèmes temps réel nécessitant une grande sûreté de fonctionnement.
L'idée est de permettre de prouver formellement les programmes écrits selon ce profil. Le profil Ravenscar en interdisant un certain nombre de caractéristiques du langage Ada, permet de rendre applicables les outils de preuve de programme.
Ce profil a aussi été appliqué à la spécification temps réel RTSJ du langage Java[1].