התחום של "אימות פורמלי" עוסק בהוכחות, אוטומטיות או אוטמטיות למחצה, של נכונות מערכות תוכנה או חומרה כנגד מפרט הכתוב בשפה פורמלית. הבסיס המתמטי/חישובי של התחום נקרא 'לוגיקה חישובית' (Computational Logic). למשל, בעזרת שפה הנקראת Temporal logic, אשר פותחה בסוף שנות ה 70 על ידי פרופ' אמיר פנואלי ממכון ויצמן, ניתן לתאר את ההתנהגות הרצויה של המערכת לאורך זמן, וכן לתאר תנאי 'בטיחות', כלומר מה אסור למערכת לעשות. כל עוד מספר המצבים אשר המערכת יכולה להיכנס אליהם הוא סופי, ניתן להוכיח באופן אוטומטי שהמערכת מספקת מפרט מסוג זה, או למצוא דוגמה נגדית, כלומר 'באג' במערכת. המאבק היום יומי של העוסקים בתחום זה הוא להאיץ את טכניקות ההוכחה האוטומטית, כדי שניתן יהיה לבדוק בזמן סביר מערכות הולכות וגדלות. היום כל יצרני המעבדים (אינטל, IBM, AMD וכו') וכן מספר חברות תוכנה (כגון מיקרוסופט) מעסיקים מומחים בתחום זה, כדי לשפר את אמינות המוצרים שלהם.
תת התחום אשר נקרא Satisfiability Modulo Theories (SMT) התפתח באמצע שנות ה 2000. הוא עוסק בפתירת נוסחאות לוגיות מורכבות השייכות למחלקה הקרויה בשפת הלוגיקאים 'לוגיקה מסדר ראשון' (First Order Logic). רבות מהבעיות בתחום של 'אימות פורמלי' שהוזכר לעיל ניתנות לפתירה על ידי יצירה של נוסחאות מסוג זה ופתירתן בעזרת כלי SMT. היכולות של כלי SMT הופכות אותם לשימושיים גם הרבה מעבר לאימות פורמלי, ובפרט משתמשים בהם לעתים דחופות לצורך פתירת בעיות אופטימיזציה קומבניטורית.
פרס Computer Aided Verification (CAV) לשנת 2021 ניתן לקבוצת חוקרים אשר הייתה מאוד פעילה בתחום זה בשנים בו הוא נוצר לראשונה, קרי שנות ה 2000.