Anthropic hat am 22. Oktober eine Forschungsarbeit zur formalen Prüfung von Software veröffentlicht. Gemeinsam mit Theorem liess das Unternehmen Claude Sicherheitseigenschaften für 123 Open-Source-Bibliotheken beweisen. Für KMU mit eigener Software oder externen Entwicklern ist die entscheidende Frage: Welche konkrete Zusicherung lässt sich daraus für das eingesetzte Programm ableiten?
Ein Beweis hat einen definierten Geltungsbereich
Die Originalarbeit beschreibt Beweise für ausgewählte Einstiegspunkte unter festgelegten Bedingungen. Dazu gehören statisch gebaute RISC-V-Programme unter einem Modell von Linux und begrenzte Eingabegrössen. Anthropic weist ausdrücklich darauf hin, dass damit weder jede Funktion noch jede reale Betriebsumgebung abgedeckt ist. Die Veröffentlichung ist ein Forschungsergebnis des Anbieters, kein Sicherheitszertifikat für Ihre Anwendung.
Der unabhängige technische Hintergrund hilft bei der Einordnung: Das Projekt Rocq erklärt, wie ein kleiner Prüfkern formale Beweise kontrolliert. Die KI erzeugt also einen überprüfbaren Beweistext. Ob dessen Aussage zur betrieblichen Anforderung passt, bleibt eine eigene Frage. Das NIST-Rahmenwerk für sichere Softwareentwicklung behandelt daneben organisatorische Vorbereitung, Schutz der Software und den Umgang mit verbleibenden Schwachstellen. Beide Quellen erläutern Methoden; sie bestätigen nicht unabhängig das neue Forschungsergebnis.
Nächster Schritt
Was heisst das für KI-Regeln und Nachweise?
- Nutzung sichtbar machen: Welche Teams nutzen welche KI-Tools?
- Daten und Freigaben klären: Was darf in ChatGPT, Copilot oder andere Tools?
- Nachweise vorbereiten: Regeln, Rollen und Unterweisung dokumentieren.
DACH-Hinweis: 10min KI Brief bleibt für KMU im gesamten DACH-Raum lesbar; konkrete Praxisangebote sind zuerst CH-first formuliert.
Was heisst das für Ihr KMU?
Unsere Empfehlung: Nehmen Sie beim nächsten Gespräch mit Ihrem Softwarepartner genau eine kritische Funktion heraus, beispielsweise den Import einer Lieferantendatei. Lassen Sie schriftlich festhalten, welche Eigenschaft abgesichert werden soll: Darf das Programm bei beschädigten Dateien abstürzen? Müssen ungültige Beträge erkannt werden? Das sind unterschiedliche Anforderungen.
Verlangen Sie zu einem angebotenen KI-Beweis drei Angaben: die geprüfte Programmversion, die angenommene Laufzeitumgebung und die ausgeschlossenen Fälle. Ergänzen Sie ein Beispiel, das ausserhalb der Zusicherung liegt. So wird sichtbar, ob der Nachweis Ihre konkrete Installation betrifft oder nur ein vereinfachtes Modell.
Bewahren Sie diese Angaben zusammen mit dem Abnahmeprotokoll auf. Bei einem Update kann die zuständige Person dann prüfen, ob Version oder Annahmen geändert wurden. Ein alter Beweis sollte nicht stillschweigend für neue Software weitergelten. Bestehende Praxistests und die Bearbeitung gemeldeter Fehler bleiben Teil der Abnahme.
Dieser kleine Beschaffungsschritt setzt weder eigene Forschung noch einen neuen KI-Vertrag voraus. Er hilft, das Wort «bewiesen» in eine überprüfbare Leistungszusage zu übersetzen, bevor Sie dafür bezahlen.
Mit Büro-KI strukturieren Sie Anforderungen und Prüffragen für einen begrenzten KI-Praxistest.
