Inom datavetenskap är en formell specifikation en matematisk beskrivning av ett mjukvaru- eller hårdvarusystem som kan implementeras enligt den beskrivningen. Den anger vad systemet ska göra, inte hur det ska göra det. Om det finns en systemspecifikation är det möjligt att tillämpa formella verifieringsmetoder för att visa att systemet uppfyller (eller kommer att uppfylla) specifikationen. Det är alltså möjligt att kontrollera om en viss designad modell kommer att uppfylla kraven efter implementering. Om programvaruverifiering undersöker ett programs överensstämmelse med en specifikation, undersöker validering om ett program eller en specifikation överensstämmer med användarkraven .