Gemini 4 Carbon ist jetzt allgemein verfügbar

Google hat den Zugang zu seinem leistungsfähigsten KI-Modell Gemini 4 Carbon ausgeweitet. Zahlende Entwickler können es nun über die Gemini-API in AI Studio und Android Studio nutzen, Unternehmen über Gemini for business sowie in der Entwicklungsumgebung Google Antigravity und im Sicherheitsagenten CodeMender. Abonnenten von Google AI Ultra erhalten schrittweise Zugang in der Gemini-App, im KI-Modus der Google-Suche und in Antigravity. Seit dem 28. Oktober war Carbon nur ausgewählten Organisationen aus der Cyberabwehr im Programm Fairwind zugänglich. Eine spezielle Variante für Cybersicherheit bleibt diesen Teilnehmern vorbehalten.

Bis zum 30. November kostet Carbon über die API 2 US-Dollar pro Million Eingabe-Tokens und 10 Dollar pro Million Ausgabe-Tokens, so viel wie Gemini 4 Argon. Danach verdoppeln sich die Preise auf 4 und 20 Dollar. Zudem testet Google in Antigravity die Funktion /swarm, die aus einem Prompt ein Team koordinierter Agenten erstellt.

Beweise bis auf Maschinenebene

Parallel hat Google DeepMind das Framework AlphaProof Code vorgestellt, in dem Fachleute gemeinsam mit KI-Agenten Software formal verifizieren, also mathematisch beweisen, dass sie festgelegte Anforderungen erfüllt. Angewendet wurde es auf libsignal, die Referenzimplementierung des Signal-Protokolls, das neben dem Messenger Signal auch WhatsApp und Google Messages zur Verschlüsselung nutzen. Menschen schrieben gemeinsam mit Agenten auf Basis von Carbon und Claude Opus 5.5 von Anthropic die Spezifikationen.

Agenten auf Basis von Carbon erzeugten anschließend mehr als sechs Millionen Zeilen Beweise in der Sprache Lean, die jeden Beweis maschinell prüft und ungültige ablehnt. Verifiziert wurden laut DeepMind zentrale kryptografische Schutzfunktionen bis hinunter auf die Ebene der Maschinenbefehle. Um zu prüfen, ob das Verfahren fehlerhaften Code erkennt, bauten die Forschenden zwei bereits behobene, echte Fehler wieder in eine isolierte Version des Codes ein.

„Angesichts zunehmender KI-gestützter Sicherheitsbedrohungen gibt uns die rigorose Verifikation der Implementierung des Signal-Protokolls noch mehr Vertrauen in die Datenschutzgarantien unseres Codes.“
Ehren Kret, Signal-CTO

Einschränkungen

Die Ergebnisse gelten für Googles eigenen Build des Codes, der über ein kleines Kommandozeilenprogramm ausgeführt wurde, nicht für die Apps von Signal selbst. Seitenkanalangriffe waren in Teilen der Analyse ausgenommen. Auch Anthropic hatte im Oktober berichtet, mithilfe von KI formale Beweise für 123 Open-Source-Bibliotheken auf Ebene des Maschinencodes erstellt zu haben. Formale Verifikation galt lange als zu aufwendig für den breiten Einsatz, da Beweise bislang weitgehend von Hand geschrieben werden mussten.

(red)