Ein $70-Millionen-Seed ist auch 2026 eine Ansage. Bei &Truth ist er vor allem ein Argument: Formale Verifikation – Software mathematisch beweisen, statt sie zu testen – sei bisher an den Kosten gescheitert, nicht an der Theorie, und generative KI könne genau diese Kosten senken.
Das Unternehmen kam am 29. Oktober aus dem Stealth, als Public Benefit Corporation mit Sitz in Palo Alto und Singapur, gegründet Anfang 2026. Co-Gründer: Clark Barrett, Stanford-Professor und Co-Direktor des Stanford Center for AI Safety, als Co-CEO; Ilya Sergey, Gründer des VERSE Lab an der National University of Singapore, als Chief Science Officer; und Chris Hsu als Co-CEO und Executive Chairman. Investoren nennt das Unternehmen nicht.
Die Technik baut auf dem Lean-Beweissystem und Open-Source-Projekten wie CSLib auf. &Truth kombiniert ein eigenes Modell mit Beweisautomatisierung, um Code in jeder Programmiersprache zu lesen und Aussagen über Sicherheit, Schutz und Korrektheit zu erzeugen, die unabhängig prüfbar sind. Dazu kommt eine „Specification Factory“: Technik, die Geschäftsanforderungen in präzise formale Spezifikationen übersetzt – in der Praxis der schwierigere Teil, weil die meisten Codebasen zwar Code, aber keine brauchbaren Spezifikationen haben.
Die Demonstration, die die Runde trägt, kam von Stanford-Forscherin Chuyue Sun, die im August zu &Truth stieß. Ihr Team verifizierte mit KI einen Teil des Verschlüsselungscodes im Messenger Signal – in unter einem halben Tag und für weniger als 500 Dollar. Dieselbe Arbeit hätte laut Unternehmen drei erfahrene Ingenieure von Hand rund fünf Monate gekostet.
„Brücken, Gebäude, sie stürzen nicht ein, weil Menschen vor dem Bau Mathematik gemacht haben“, sagte Sergey. „Warum tun wir das nicht mit Code? Die Technologie zum mathematischen Schließen war da, nur schwer zu skalieren.“ Barrett zog die Parallele zu den jüngsten Erfolgen von KI bei offenen mathematischen Vermutungen: Dieselben formalen Methoden ließen sich auf Software anwenden.
&Truth ist Teil einer Welle. Der Rivale Harmonic, unterstützt unter anderem vom Venture-Arm von Nvidia, hat 295 Millionen Dollar eingesammelt und stellte diese Woche seinen Aristotle-Agenten vor, der C-Code und Verilog-Hardwaredesigns verifiziert; laut Berichten testen Tensordyne und Nvidia ihn. Anthropic und das Verifikations-Startup Theorem meldeten gemeinsam KI-gestützte Fehlersuche in Open-Source-Software und ein Verifikations-Add-on für Claude. Madan Musuvathi, früher bei Microsoft Research, gründete Truidic, um automatisierte Verifikation zu kommerzialisieren.
Skepsis gibt es reichlich, und sie ist verdient. Will Wilson, CEO des Fehlersuche-Startups Antithesis, nannte formale Verifikation für sich genommen eine Falle: Sein Haus habe Millionen in die Verifikation defensiver Systeme gesteckt und mit Testwerkzeugen trotzdem weitere Fehler gefunden. Vitalik Buterin warnte, Verifikation sei kein Allheilmittel gegen Sicherheitslücken. Byron Cook, Distinguished Scientist bei AWS, berichtet, automatisiertes Schließen habe Kundensorgen um Cloud-Sicherheit gedämpft – aber mittelgroße Unternehmen sagen, wochenlanges Warten auf Verifikation bremse die Entwicklung, und Verifikationsingenieure seien knapp.
Das ist die eigentliche Wette: Nicht, dass Beweise perfekt sind, sondern dass sie billig genug werden, um in normale Entwicklungsabläufe zu passen. Bei unter 500 Dollar und einem halben Tag für ein Stück Signal-Verschlüsselung ist die Rechnung zumindest interessant.
