Microsoft: Wenn KI Millionen Zeilen Code umschreibt, wird Vertrauen zum Engpass

Agenten verändern einige der größten Codebasen

Nach Angaben von Microsoft baut und betreibt das Unternehmen KI-Agenten, die einige der größten Codebasen der Welt umwandeln, darunter Windows und Azure. Die Arbeit reicht von der Migration einer Codebasis mit 400 Millionen Zeilen auf eine neue Compiler-Toolchain bis zur Modernisierung von altem C- und C++-Code nach Rust, zunehmend abgesichert durch formale Verifikation.

Der Beitrag stammt von Sriram Rajamani und Tim Bozarth, beide Corporate Vice Presidents bei Microsoft. Er ist der erste einer Serie darüber, was das Unternehmen entwickelt und was es dabei gelernt hat. Microsoft kombiniert nach eigenen Angaben seit 2024 KI-Agenten mit statischer Analyse, Tests und formaler Verifikation.

Das Unternehmen beschreibt einen Wandel in der Art, wie die Systeme gebaut werden. Zunächst habe man Workflows fest codiert, die LLMs als Unterroutinen aufriefen. Bis Mai 2025 seien Agenten laut Microsoft bessere Planer gewesen als die eigenen Pipelines, und die Aufgabe der Ingenieure habe darin bestanden, die Werkzeuge zu bauen, die Agenten aufrufen. Die wertvollsten dieser Werkzeuge sagen einem Agenten und den Ingenieuren dahinter, ob eine Änderung korrekt ist.

Migration: ein kleines Expertenteam, verstärkt durch Agenten

Microsoft definiert Migration als eine Transformation, die auf eine gesamte Codebasis angewendet wird, um ein bestimmtes technisches Ziel zu erreichen, etwa das Aktualisieren von Abhängigkeiten, die Einführung eines neuen Compilers, das Beheben von Funden der statischen Analyse oder den Umstieg auf eine neue Plattform. Zu den Fallstudien gehören die Unterstützung der Clang/LLVM-Toolchain in der gesamten Windows-Codebasis, die mehrere hundert Millionen Zeilen Code umfasst, die Behebung von Funden der Analysewerkzeuge CodeQL, PREfast und Roslyn sowie die Portierung von Diensten von x86 auf ARM.

Das Unternehmen hat eine bewusste Entscheidung darüber getroffen, wer die Arbeit erledigt: Ein sehr kleines Team von Migrationsexperten soll eine große Migration vorantreiben, statt die Verantwortung auf die gesamte Entwicklungsorganisation zu verteilen. Der Prozess läuft in Stufen ab:

• Agenten lernen aus stichprobenartig ausgewählten Funden eine Kandidaten-Wissensbasis.
• Ein Reviewer-Agent bewertet jede vorgeschlagene Korrektur nach Korrektheit, Minimalität, Übereinstimmung mit den Konventionen der Datei und Wartbarkeit.
• Experten genehmigen die Wissensbasis statt einzelner Korrekturen.
• Agenten wenden sie anschließend auf die gesamte Codebasis an, wobei das Feedback des Reviewers die Wissensbasis in jeder Stufe weiter verfeinert.

Das Bündeln ähnlicher Korrekturen für die Prüfung entlastet die Reviewer zusätzlich. Menschliche Aufmerksamkeit ist laut Microsoft zur knappsten Ressource im agentischen Software Engineering geworden, und die Werkzeuge seien darauf ausgelegt, sie dort einzusetzen, wo sie am meisten zählt.

Der Umstieg von altem C und C++ auf Rust

Microsoft weist darauf hin, dass Sprachen wie C und C++ es leicht machen, Speichersicherheitsfehler einzubauen, und schwer, sie wieder loszuwerden. Ein Neuschreiben in Rust verspreche Sicherheit durch Konstruktion, aber nur, wenn die Neufassung exakt bewahrt, was der ursprüngliche Code tat. Bei realen Systemen in dieser Größenordnung sei eine manuelle Neufassung selten praktikabel, und eine automatisierte sei nur nützlich, wenn man ihr vertrauen könne.

Das Unternehmen skizziert eine zeitliche Entwicklung. Im Januar 2025 ließ sich der erzeugte Rust-Code nicht kompilieren. Im Juni 2025 kompilierte er, lief aber nicht korrekt und bestand die Tests nicht. Im September 2025 hatte Microsoft mit manueller Anleitung funktionierende Übersetzungen von rund 30.000 Zeilen. Seit Februar 2026 modernisiere man große Codebasen mit erheblicher Automatisierung.

Mit jedem Schritt verlagerte sich der Engpass, vom Kompilieren über das Bestehen von Tests bis zum validierten Verhalten im großen Maßstab. Microsoft sagt, die Migration Feature für Feature funktioniere besser als die zeilenweise Übersetzung einer Komponente, weil ein Feature eine Einheit nutzersichtbaren Verhaltens sei, die sich mit szenariobasierten Tests durchgängig validieren lasse. Differenzielles Testen vergleicht das Verhalten von Quell- und Zielcode, und vor dem Agenten zurückgehaltene Tests messen die Robustheit. Zuletzt habe das Unternehmen begonnen, formale Spezifikationen aus dem Quellcode zu extrahieren, in die Zielsprache zu übertragen und mit Verus zu beweisen, dass der modernisierte Code sie erfüllt.

Spezifikationsgetriebene Entwicklung und was sie signalisiert

Microsoft argumentiert, dass Agenten Änderungen schneller erzeugen können, als Menschen sie beurteilen können, und dass lokal plausibler Code dennoch architektonische Annahmen, verteilte Protokolle, Sicherheitsgrenzen oder betriebliche Invarianten verletzen kann. Tests und Reviewer fingen einige Probleme ab, doch keines von beiden halte Schritt, so das Unternehmen. Seine Antwort: die Absicht explizit machen, sodass sich die Aufmerksamkeit der Entwickler vom Schreiben von Code auf die Verwaltung der Spezifikationen verlagert, die Agenten leiten und deren Ergebnisse validieren.

Als ersten Schritt nutzt Microsoft Agenten, um aus bestehenden Codebasen formale Spezifikationen abzuleiten, etwa in TLA+. Werkzeuge wie TLC prüfen dann, ob Ausführungsspuren der Implementierung von der Spezifikation zugelassen werden. Wird eine Spur nicht zugelassen, kann die Ursache ein Implementierungsfehler, eine ungenaue Spezifikation oder ein ungültiger Test sein, und die Agenten überarbeiten, was jeweils falsch ist. Das Unternehmen fügt hinzu, dies zeige, dass die Spezifikationen das beobachtete Verhalten zulassen, während die Frage, ob sie erfassen, was das System tun soll, schwieriger sei. Zudem entwickle man einen Compiler von TLA+ nach F* und von TLA+ nach Lean, um Eigenschaften für alle Konfigurationen zu beweisen.

Für Entwicklungsteams lautet die Botschaft von Microsoft: Die Skalierung KI-gestützter Codeänderungen hängt von Verifikationswerkzeugen und gezielt platzierter menschlicher Prüfung ab, nicht allein von der Codegenerierung.