Der Begriff Formale Methoden (FM) fasst die Techniken der Modellierung und mathematischer, rigoroser Überprüfung von Computersystemen zusammen, um deren Stabilität und Zuverlässigkeit mathematisch nachweisen zu können. Überwiegend werden FM verwendet, um die Fehlerfreiheit von möglichst vollständig spezifizierten Modellen zu analysieren. Die Spezifizierung von KI-Modellen stellt die Gesamtheit der FM vor besondere Herausforderungen, die im Dokument beschrieben werden. KI-Modelle sollen bezüglich Erklärbarkeit, Robustheit und Sicherheit verifiziert werden. Es gibt gute Ansätze für den Nachweis der Korrektheit durch automatisierte Deduktion. Dies wird anhand eines exemplarischen Vorgehens in der Publikation beschrieben.