&Truth sammelt 70 Millionen US-Dollar Seed-Kapital für den Aufbau einer universellen Verifikationsmaschine für Code ein

&Truth, eine gemeinwohlorientierte Kapitalgesellschaft, die Technologien entwickelt, mit denen sich mathematisch beweisen lässt, dass Software sicher ist, trat am 29. Oktober 2026 aus dem Stealth-Modus und gab eine Seed-Finanzierung in Höhe von 70 Millionen US-Dollar sowie den Plan bekannt, eine nach eigenen Angaben universelle Verifikationsmaschine für Code zu entwickeln.

In ihrer Ankündigung zum Start erklärte das Unternehmen, es sei Anfang 2026 gegründet und mit 70 Millionen US-Dollar Seed-Kapital von einer Gruppe finanziert worden, die es als prägende Führungspersönlichkeiten aus den Bereichen KI-Sicherheit und Risikokapital beschrieb. Die Verifikationsmaschine werde so entwickelt, dass sie Code in jeder Programmiersprache lesen und mathematisch beweisen könne, dass dieser sicher, geschützt und korrekt sei – mit Beweisen, die jeder unabhängig überprüfen könne.

Automatisierung von Beweisen auf Basis von Lean

Formale Verifikation gibt es seit Jahrzehnten, sie war jedoch bislang unzugänglich und teuer, hieß es in der Ankündigung, weil Fachleute Beweise manuell formulieren mussten und sich die Anwendung deshalb auf eine Handvoll kritischer Systeme beschränkte. KI beschleunige die Arbeit an formalen Beweisen inzwischen um das Hundertfache oder mehr, erklärte das Unternehmen; seine Technologie zur Automatisierung von Beweisen beschleunige den Prozess nochmals um das Hundertfache und verkürze die Erstellung von Beweisen von Jahren oder Monaten auf Stunden oder Minuten.

Das Unternehmen stellte außerdem eine Technologie vor, die es als „Spezifikationsfabrik“ bezeichnet. Sie ermögliche es Unternehmen und Entwicklern, menschliche Absichten und geschäftliche Anforderungen in großem Maßstab in präzise formale Spezifikationen zu übersetzen. So entstünden Garantien, die sich unabhängig überprüfen ließen, statt sich auf Tests oder Aussagen von Anbietern zu stützen.

&Truth baut auf Lean, einem quelloffenen Beweissystem, und Mathlib auf, einer Bibliothek mit mehr als zwei Millionen Zeilen mathematischer Definitionen und Theoreme, sowie auf quelloffenen Technologien wie CSLib. Ziel sei laut dem Unternehmen ein universelles formales Vokabular für Software: mathematische Modelle von Programmiersprachen und Systemen, Beweistechniken sowie präzise Spezifikationen, die eine automatisierte Verifikation über verschiedene Sprachen hinweg ermöglichen. &Truth erklärte, mit der Lean Focused Research Organization zusammenzuarbeiten und seine grundlegenden Bibliotheken als Open Source zu veröffentlichen.

Mitgründer und Co-CEO Clark Barrett erklärte, Lean und Mathlib hätten der KI eine präzise Sprache für mathematisches Denken gegeben, während der Software eine vergleichbare Grundlage fehle. Mitgründer und Chief Science Officer Ilya Sergey sagte, Vertrauen in Software solle auf unabhängig überprüfbaren Beweisen beruhen und nicht auf dem Wort eines Unternehmens.

Gründer und zwei Unternehmensstandorte

Barrett ist Corbel-Professor für Informatik an der Stanford University, Gründungs-Co-Direktor des Stanford Center for AI Safety, Direktor des Stanford Center for Automated Reasoning, Mitentwickler von CSLib und Projektleiter der automatisierten Reasoning-Engine cvc5. Sergey gründete das VERSE Lab an der National University of Singapore und entwickelte die quelloffenen Verifikationswerkzeuge Veil und Velvet mit. Mitgründer, Co-CEO und Executive Chairman Chris Hsu gehört dem Lean FRO Strategic Advisory Board an und ist Präsident der Infinitude Foundation. Zuvor war er CEO von Kilometre Capital und Managing Director der Citadel Investment Group.

In der Ankündigung wurden außerdem Gregory Malecha genannt, der zuvor bei BlueRock Security die Arbeit an formalen Methoden leitete und maßgeblich an der Architektur des Verifikations-Frameworks BRiCk beteiligt war; Sebastian Ullrich, Mitarchitekt von Lean 4 und Mitgründer der Lean Focused Research Organization; Linus Lee, ehemaliger geschäftsführender Gesellschafter bei Kilometre Capital; sowie Drew Harman, ehemaliger Chief Commercial Officer bei Fastino Labs und Operating Partner bei Insight Partners und Shasta Ventures. &Truth erklärte, auf jahrzehntelanger Forschung zu formaler Verifikation und automatisiertem Reasoning an der Stanford University und der National University of Singapore aufzubauen.

Der US-Hauptsitz von &Truth befindet sich in Palo Alto, der internationale Hauptsitz in Singapur. Dort werde das Büro nach Angaben des Unternehmens seine Aktivitäten in den Bereichen Forschung, Entwicklung, Produkt und Marktbearbeitung deutlich ausweiten. Low Jin Yong, Senior Vice President und Co-Leiter von Digital Industry Singapore, erklärte in der Ankündigung, der Hauptsitz werde die Kompetenzen Singapurs in den Bereichen Vertrauen und Sicherheit vertiefen und das Land als Standort für Unternehmen stärken, die vertrauenswürdige KI entwickeln.

Auf der Website des Unternehmens findet sich außerdem eine Podiumsdiskussion mit Leonardo de Moura, dem Erfinder von Lean und VP sowie Distinguished Scientist bei AWS, und Simone Severini, Mitglied des Lean FRO Strategic Advisory Board und Distinguished Engineer bei Google.

Begleitende Essays erläutern die Beweggründe des Unternehmens

In einem Begleitessay vom 29. Oktober 2026 erläuterte Hsu die Entwicklungen, die eine Verifikation nach Ansicht des Unternehmens dringend erforderlich machen. Er verwies auf Äußerungen von Google-CEO Sundar Pichai, wonach inzwischen 75 % des neuen Codes bei Google von KI generiert und von Ingenieuren freigegeben würden, sowie auf die Tests von Veracode aus dem Jahr 2026, bei denen KI-Modelle bei fast der Hälfte der Programmieraufgaben versagten, bei denen Sicherheit eine Rolle spielte. Der Essay verweist außerdem auf eine Angriffskampagne im September 2026, bei der ein Angreifer Hunderte von KI-Agenten einsetzte, um über Schwachstellen in weit verbreiteter Software zur Druckerverwaltung in 395 Organisationen in 48 Ländern einzudringen, sowie auf einen Rekordwert von 14.959 im September 2026 veröffentlichten Software-Schwachstellen – laut Essay dreieinhalbmal so viele wie im Vorjahr.

Der Essay schildert frühere Meilensteine der formalen Verifikation: Der ursprüngliche Beweis für den seL4-Mikrokernel erforderte rund 20 Personenjahre Expertenarbeit für etwa 8.700 Codezeilen; 2015 wurde seL4 im Rahmen des DARPA-Programms HACMS in Boeings unbemannten Hubschrauber Little Bird integriert, dessen Flugsteuerung ein professionelles Red Team trotz wochenlangen Zugriffs nicht überwinden konnte; und im September 2026 formalisierte ein von Anthropic entwickeltes KI-Modell innerhalb von 11 Tagen in Lean den vollständigen Beweis von Fermats letztem Satz. Außerdem wird erwähnt, dass Kim Morrison, Senior Research Software Engineer bei Lean FRO, bereits früher im Jahr 2026 Anthropics Claude mit minimaler menschlicher Anleitung nutzte, um eine Lean-Version der zlib-Kompressionsbibliothek zu erstellen und zu beweisen, dass sie stets exakt die Daten wiederherstellt, die sie komprimiert hat.

Der Essay zitiert Lean-Erfinder Leonardo de Moura: „Tests schaffen Vertrauen. Beweise geben Sicherheit.“

In einem zweiten Essay, der am 29. Oktober 2026 veröffentlicht wurde, erläutert Sergey die Funktionsweise der Programmverifikation. Er beginnt mit Alan Turings Aufsatz „Checking a Large Routine“ aus dem Jahr 1949, in dem dieser vorschlug, dass Programmierer ihren Code mit präzisen Aussagen versehen, die ein Prüfprogramm einzeln verifizieren könnte. Der Essay beschreibt Spezifikationen, Schleifeninvarianten und in Lean geprüfte Beweise und erklärt, dass &Truth Entwicklern unabhängig überprüfbare Nachweise ermöglichen will, etwa einen formalen Beweis in Lean – und zwar zu Kosten, die Verifikation zu einem routinemäßigen Bestandteil der Entwicklung machen.

&Truth beschreibt seine langfristige Vision als einen Wandel vom „Vibe-Coding“ zum „Veri-Coding“: Dabei wird KI-generierter Code vor der Bereitstellung mathematisch verifiziert, arbeiten KI-Agenten in nachweislich eingegrenzten Umgebungen, wird veraltete Software sicher modernisiert und kritische Infrastruktur durch unabhängig überprüfbare mathematische Garantien geschützt.