Zum Inhalt springen
CASOON

Formale Verifikation wird zugänglich: Lean 4, TLA+ und der Weg in die Praxis

Entwicklung

Wie mathematische Beweissysteme aus der Akademie in die Produktentwicklung wandern

13 Minuten
Formale Verifikation wird zugänglich: Lean 4, TLA+ und der Weg in die Praxis
#Formale Verifikation #Lean 4 #TLA+ #Dafny
SerieSprachtheorie für Praktiker
Teil 3 von 6

„Testen zeigt die Anwesenheit von Fehlern, nicht ihre Abwesenheit.” Dieser Satz von Edsger Dijkstra beschreibt eine fundamentale Grenze: Egal wie viele Tests wir schreiben, wir können nicht alle möglichen Eingaben abdecken.

Formale Verifikation verspricht mehr: mathematische Beweise, dass Software korrekt ist. Lange war das Thema für Chipdesigner und Sicherheitsforscher reserviert. Aber die Werkzeuge werden zugänglicher – und die Anwendungsfälle relevanter.

Was ist formale Verifikation?

Formale Verifikation nutzt mathematische Methoden, um Eigenschaften von Software zu beweisen. Statt Beispiele zu testen, beweist man Aussagen über alle möglichen Eingaben.

Drei Hauptansätze:

  1. Model Checking: Systematisches Durchsuchen aller Zustände eines Systems
  2. Theorem Proving: Interaktive mathematische Beweise
  3. Static Analysis: Automatische Analyse ohne Ausführung

TLA+: Spezifikation verteilter Systeme

TLA+ (Temporal Logic of Actions) wurde von Leslie Lamport entwickelt und wird bei Amazon, Microsoft und anderen für kritische Systeme eingesetzt.

---- MODULE SimpleCounter ----
EXTENDS Integers
VARIABLE count

Init == count = 0

Increment == count' = count + 1

Next == Increment

Spec == Init /\ [][Next]_count

TypeInvariant == count \in Nat

THEOREM Spec => []TypeInvariant
====

Die Stärke von TLA+ liegt in der Modellierung von Nebenläufigkeit:

---- MODULE TransferMoney ----
EXTENDS Integers
VARIABLES balance_A, balance_B

Init == 
    /\ balance_A = 100
    /\ balance_B = 100

Transfer(amount) ==
    /\ balance_A >= amount
    /\ balance_A' = balance_A - amount
    /\ balance_B' = balance_B + amount

TotalBalance == balance_A + balance_B

Invariant == TotalBalance = 200
====

Der TLA+ Model Checker (TLC) findet Race Conditions, Deadlocks und Invarianzverletzungen, die Tests übersehen würden.

Amazon’s Erfahrung

Amazon Web Services nutzt TLA+ seit 2011 für kritische Systeme wie S3 und DynamoDB. In einem Paper berichten sie:

  • Schwere Bugs in Designs gefunden, die monatelang Code-Reviews überstanden hatten
  • Komplexe Optimierungen sicher implementiert
  • Onboarding neuer Entwickler beschleunigt durch präzise Spezifikationen

Lean 4: Theorem Proving trifft Programmierung

Lean 4 ist mehr als ein Beweisassistent – es ist eine vollwertige Programmiersprache, deren Programme gleichzeitig Beweise sind.

-- Eine Funktion mit Beweis ihrer Korrektheit
def double (n : Nat) : Nat := n + n

theorem double_is_twice : ∀ n : Nat, double n = 2 * n := by
  intro n
  simp [double]
  ring

Der Typ ∀ n : Nat, double n = 2 * n ist ein Theorem. Der Beweis (by intro n; simp; ring) überzeugt den Compiler, dass es gilt.

Praktisches Beispiel: Sichere Division

-- Division, die nur für nicht-null Divisoren kompiliert
def safeDiv (a : Nat) (b : Nat) (h : b ≠ 0) : Nat :=
  a / b

-- Nutzung erfordert Beweis
example : safeDiv 10 2 (by decide) = 5 := rfl

-- Das kompiliert nicht:
-- example : safeDiv 10 0 ??? = ???

Der Compiler erzwingt den Beweis, dass der Divisor nicht null ist. Division durch null ist nicht zur Laufzeit möglich, sondern zur Kompilierzeit ausgeschlossen.

Mathlib: Mathematik formalisiert

Die Mathlib-Bibliothek formalisiert weite Teile der Mathematik in Lean. Das ermöglicht:

  • Verifizierte numerische Algorithmen
  • Korrektheitsnachweise für kryptographische Protokolle
  • Maschinenprüfbare mathematische Beweise

Dafny: Verifikation für Entwickler

Dafny, entwickelt bei Microsoft Research, ist speziell für Software-Entwickler designed:

method BinarySearch(a: array<int>, key: int) returns (index: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures index >= 0 ==> index < a.Length && a[index] == key
  ensures index < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
{
  var lo, hi := 0, a.Length;
  while lo < hi
    invariant 0 <= lo <= hi <= a.Length
    invariant forall i :: 0 <= i < lo ==> a[i] < key
    invariant forall i :: hi <= i < a.Length ==> a[i] > key
  {
    var mid := (lo + hi) / 2;
    if a[mid] < key {
      lo := mid + 1;
    } else if a[mid] > key {
      hi := mid;
    } else {
      return mid;
    }
  }
  return -1;
}

Die requires-, ensures- und invariant-Klauseln werden vom Verifier geprüft. Wenn der Code kompiliert, ist die Korrektheit bewiesen.

Warum jetzt?

Mehrere Faktoren machen formale Verifikation praktischer:

1. Bessere Tooling

  • VSCode-Extensions mit Echtzeit-Feedback
  • Schnellere Solver (Z3, CVC5)
  • Inkrementelle Verifikation

2. LLM-Unterstützung

GPT-4 und Claude können:

  • TLA+ Spezifikationen aus informellen Beschreibungen generieren
  • Lean-Beweise vorschlagen
  • Invarianten erraten

3. Steigende Komplexität

  • Verteilte Systeme sind schwer zu testen
  • Kryptographie erfordert Korrektheitsnachweise
  • Regulatorische Anforderungen (Automotive, Medizin)

4. Proof Carrying Code

WebAssembly und andere Formate ermöglichen verifizierte Binaries:

  • Der Beweis reist mit dem Code
  • Empfänger können Korrektheit prüfen ohne zu vertrauen

Einstiegspunkte

Für verteilte Systeme: TLA+

  • Learn TLA+ – Interaktives Tutorial
  • AWS-Paper: „Use of Formal Methods at Amazon Web Services”

Für algorithmische Korrektheit: Dafny

Für tiefes Verständnis: Lean 4

Die Zukunft: Verifikation als Standard

Die Vision: Kritische Codepfade werden verifiziert, nicht nur getestet. Das bedeutet nicht, dass jede Zeile bewiesen wird – aber Invarianten, Sicherheitseigenschaften und Protokolle.

Die Werkzeuge sind bereit. Die Frage ist, ob die Industrie die Investition wagt. Angesichts der Kosten von Software-Fehlern – Cloudausfälle, Sicherheitslücken, finanzielle Verluste – wird die Antwort zunehmend „ja” lauten.

Weiterführende Ressourcen