Metas Oversight Board hat überraschend zusätzliche 13 Millionen US-Dollar von dem Internetkonzern bekommen. Damit sei der Betrieb des Aufsichtsgremiums bis 2028 gesichert, erklärte dessen Co-Chef Paolo Carozza in einer Stellungnahme. Darin versichert er auch, dass Meta bekräftigt habe, weiterhin mit der Einrichtung zusammenarbeiten zu wollen. Schwierige Fälle würden auch in Zukunft an das Board weitergeleitet und Beratung zu allgemeinen politischen Fragen angenommen. Zudem werde Meta weiterhin öffentlich auf Änderungsempfehlungen reagieren. Das Geld soll in den unwiderruflichen Treuhandfonds fließen. Die Summe hat unter anderem Reuters öffentlich gemacht.

Immer wieder Kritik an Meta

Bei dem Oversight Board handelt es sich um ein von Meta unabhängiges Gremium, bei dem sich Nutzerinnen und Nutzer über eine aus ihrer Sicht ungerechtfertigte Löschung von Inhalten beschweren können. Das Gremium ist dabei als nächste Eskalationsebene gedacht, insbesondere für schwierige oder grundsätzliche Fälle. Auch Meta-Dienste wie Facebook selbst können dieses Oversight Board darum bitten, Entscheidungen des Unternehmens auf den Prüfstand zu stellen. Vor sechs Jahren wurden die ersten Mitglieder benannt, aktuell gehören ihm unter anderem der Journalist Alan Rusbridger und die dänische Politikerin Helle Thorning-Schmidt an.

Laut der Nachrichtenagentur Reuters hat Meta zuletzt 2024 mindestens 30 Millionen US-Dollar für das Gremium zur Verfügung gestellt, die sollten dessen Betrieb bis 2027 sicherstellen. Nun gibt es für ein weiteres Jahr eine deutliche Aufstockung. Das Oversight Board hat immer wieder auch teils deutliche Kritik an Entscheidungen von Meta geübt. So hat das Gremium Anfang 2024 angemahnt, dass Metas Richtlinien für den Umgang mit KI-manipulierten Inhalten lediglich auf den Einsatz der Technik abzielen, dabei aber vernachlässigen, welche Wirkung Bilder haben können. Konkret ging es damals um ein angebliches Video des damaligen US-Präsidenten Joe Biden.

(mho)

„Subnautica 2“ hat offenbar kurz nach dem Early-Access-Start die Earn-Out-Klausel aus Kraftons Kaufvertrag mit Unknown Worlds ausgelöst. Laut Korea Economic Daily soll Publisher Krafton nun bis zu 250 Millionen US-Dollar an die ehemaligen Unknown-Worlds-Gesellschafter zahlen.

Der Korea Economic Daily zufolge sieht der Kaufvertrag vor: Sobald der monatliche Studioerlös von Unknown Worlds 69,8 Millionen US-Dollar übersteigt, zahlt Krafton 3,12 US-Dollar pro verdienten Umsatz-Dollar – maximal 250 Millionen US-Dollar insgesamt. Bei 4 Millionen verkauften Spielen und einem Kaufpreis von 30 US-Dollar kann man grob überschlagen, dass Unknown Worlds diese Maximalsumme schon geknackt haben dürfte.

„Subnautica“ war alleine in den ersten zwölf Stunden 2 Millionen Mal verkauft worden. Das Survival-Spiel führte zuvor lange die Wunschlisten-Charts bei Steam an und ist zudem auf Xbox Series X/S verfügbar. Es kann außerdem als Teil des Spieleabos Game Pass gespielt werden.

Krafton gegen Unknown Worlds

Im Sommer 2025 hatte Krafton den Unknown-Worlds-CEO Ted Gill sowie Mitgründer Charlie Cleveland und Max McGuire entlassen und den Early-Access-Start auf 2026 verschoben. Sie warfen Krafton später vor Gericht vor, die Earn-Out-Zahlung unterlaufen zu wollen. Der neue Early-Access-Termin fiel nämlich nicht mehr in den ursprünglich von der Earn-Out-Klausel festgelegten Zeitraum.

Im Verlauf des Gerichtsverfahrens am Delaware Court of Chancery (Az. 2025-0805-LWW) wurde bekannt, dass Krafton-Chef Changhan Kim unter anderem ChatGPT konsultiert hatte, um Wege zu finden, die Zahlung zu vermeiden. Das Gericht befand, dass Krafton keinen gerechtfertigten Grund für die Entlassungen nennen konnte. Im März 2026 ließ es den entlassenen CEO Ted Gill wieder einsetzen und verlängerte die Earn-Out-Frist bis 15. September 2026. Die ehemaligen Unknown-Worlds-Manager hatten angekündigt, die Zahlung mit den Studio-Mitarbeitern zu teilen.

Laut einem Reddit-Post von Creative Producer Scott MacDonald arbeiten etwa 70 Personen an „Subnautica 2“. Im vergangenen Jahr schrieb Bloomberg, Unknown Worlds habe etwa 100 Angestellte.

(dahe)

Wie lange braucht man, um ein fehlerfreies Programm zu schreiben? Wenn das Programm nur eine einzige Zeile umfasst, sollte die Antwort lauten: gar nicht lange. „Hello World“ ist das erste Programm, das die meisten Entwicklerinnen und Entwickler in einer neuen Sprache schreiben. Es macht genau eine Sache: einen Text auf dem Bildschirm ausgeben. Fehler sind in einem solchen Programm kaum vorstellbar.

Und doch weist „Hello World“ in den meisten Programmiersprachen einen Bug auf. Der Entwickler Dan Gohman hat das 2022 in einem viel beachteten Blogbeitrag anhand des folgenden Codes demonstriert:

#include 
#include 
int main(void)
{
  puts("Hello World!");
  return EXIT_SUCCESS;
}

Linux bietet mit /dev/full eine Gerätedatei an, die sich wie eine volle Festplatte verhält. Leitet man die Ausgabe eines Hello-World-Programms dorthin um, schlägt der Schreibvorgang fehl, das Betriebssystem meldet „No space left on device“. Das Programm aber meldet Erfolg. In C, C++, Java, Ruby, Python 2, Node.js und Haskell verschluckt „Hello World“ den Fehler stillschweigend und gibt den Exit-Code 0 zurück, als wäre nichts geschehen. Andere Sprachen machen es besser: Python 3, Rust, Perl, Bash, OCaml, Tcl, C# und – durchaus bemerkenswert – Awk erkennen den Fehler korrekt und melden ihn. Dass ausgerechnet eine Skriptsprache aus den 1970er-Jahren gewissenhafter mit Fehlern umgeht als moderne Mainstream-Sprachen, ist eine der Pointen dieses Experiments.

Die Annahme, dass die Standardausgabe immer funktioniert, ist so tief eingebrannt, dass sie niemand hinterfragt. Dabei ist das Szenario keineswegs akademisch: Jedes Programm, das seine Ausgabe in eine Datei umleitet, kann auf eine volle Festplatte treffen. Wenn es den Fehler nicht erkennt und meldet, arbeitet der aufrufende Prozess stillschweigend mit unvollständigen Daten weiter. Wenn schon das einfachste denkbare Programm nicht fehlerfrei ist, was bedeutet das für echte Software?

Testen heißt nicht beweisen

In der professionellen Softwareentwicklung fehlt es nicht an Maßnahmen gegen Fehler. Unit-Tests, Integrationstests, statische Codeanalyse, Reviews, automatisierte CI/CD-Pipelines: Die Werkzeuge sind vielfältig und ausgereift, und die entsprechenden Prozesse oftmals schon seit vielen Jahren etabliert. Und trotzdem landen regelmäßig Bugs in produktiv laufendem Code. Das liegt in der Natur des Testens selbst.

Edsger Dijkstra brachte es bereits in den 1970er-Jahren auf den Punkt: Testen kann die Anwesenheit von Fehlern zeigen, niemals aber ihre Abwesenheit. Denn bei Tests handelt es sich lediglich um Stichproben. Sie prüfen ausgewählte, aber niemals alle denkbaren Fälle. Ein Test, der hundert Eingaben korrekt verarbeitet, sagt nichts über die hundertunderste. Selbst eine Testabdeckung von hundert Prozent, gemessen an den Codezeilen, bedeutet lediglich, dass jede Zeile mindestens einmal ausgeführt wurde. Sie sagt nichts darüber aus, ob alle relevanten Kombinationen von Eingaben, Zuständen und Umgebungsbedingungen abgedeckt sind. Bei einem Programm mit zwanzig booleschen Parametern gibt es bereits über eine Million mögliche Kombinationen. Kein Test der Welt deckt das vollständig ab.

Die meisten Entwicklerinnen und Entwickler kennen den Effekt aus eigener Erfahrung: Sie haben sich Mühe gegeben, sorgfältig getestet, alle bekannten Szenarien abgedeckt. Dann nutzt die Kundin oder der Kunde die Software zum ersten Mal, und innerhalb von Minuten ist ein Fehler aufgetreten, den niemand vorhergesehen hat. Das liegt nicht daran, dass das Team schlecht getestet hätte. Es liegt daran, dass Kundinnen und Kunden andere Annahmen mitbringen, andere Reihenfolgen ausprobieren, andere Eingaben machen und auf anderem Wege zu den gleichen Funktionen gelangen. Sie testen nicht systematisch, sondern benutzen die Software. Und genau das deckt Fehlerklassen auf, die in keinem Testplan stehen.

Ein Beispiel aus der Praxis illustriert das auf lehrreiche Weise. Mein Unternehmen entwickelt eine Datenbank, deren API und UI über HTTP erreichbar sind. Selbstverständlich wurde alles vor der Veröffentlichung der ersten Version ausgiebig getestet, einschließlich der Konfiguration verschiedener Netzwerk-Ports. Der Standardport 3000, übliche Alternativen wie 8080 und 5000, diverse hohe Portnummern: Alles funktionierte einwandfrei. API-Aufrufe über curl und Postman, Integrationstests, manuelle Tests – es gab keinerlei Auffälligkeiten.

Nur wenige Stunden nach der Veröffentlichung trudelte der erste Bugreport ein: „Die UI lädt nicht auf Port 6000“. Also suchte das Team im gesamten Code nach dem Fehler. Das Routing im Webserver war korrekt. Die CORS-Header waren korrekt. Alles sah richtig aus. Erst die Netzwerkanalyse im Browser brachte die Lösung: Die Anfragen verließen den Browser erst gar nicht. Sie wurden blockiert, bevor sie das Netzwerk erreichten.

Alle Browser der Chrome-Familie blockieren nämlich die Ports 6000 bis 6063 aus Sicherheitsgründen, weil dort traditionell das X-Window-System (X11) lauscht, dessen Netzwerkprotokoll historisch anfällig für Angriffe war. Diese Entscheidung wurde vor Jahren getroffen, vergraben im Quellcode der Browser und in Spezifikationen. Aus Sicht des Betriebssystems gibt es keinen Unterschied zwischen Port 5999 und Port 6000. Aus Sicht des Browsers schon. Kein Test hatte diesen Fall abgedeckt, weil niemand Anlass hatte, danach zu suchen. Es war, wie der Hello-World-Bug, ein Fehler in der Lücke zwischen dem eigenen System und den Annahmen über die Umgebung.

Solche Fehler haben ein gemeinsames Muster: Sie entstehen dort, wo niemand hinschaut, weil es vermeintlich keinen Grund gibt, dorthin zu schauen. Und genau deshalb lassen sie sich durch Tests nicht zuverlässig finden, denn Tests prüfen stets nur das, woran jemand zuvor gedacht hat.

Das Halteproblem

Die Frage liegt nahe, ob es nicht ein Werkzeug geben könnte, das ein Programm vollständig analysiert und zuverlässig feststellt, ob es fehlerfrei ist. Nicht durch Stichproben wie Tests, sondern durch systematische Prüfung aller möglichen Ausführungspfade. Ein perfekter Bug-Detektor, der jedes Programm entgegennimmt und mit Sicherheit feststellt, ob das Programm fehlerfrei ist oder nicht. Die Vorstellung ist verlockend. Jede Softwarefirma würde ein solches Werkzeug sofort kaufen, und es würde die Branche grundlegend verändern.

Der britische Mathematiker Alan Turing bewies 1936, dass ein solches Werkzeug nicht existieren kann. Er zeigte das nicht einmal anhand der Frage nach Bugs, sondern anhand einer viel einfacheren Frage: Lässt sich für ein beliebiges Programm und eine beliebige Eingabe entscheiden, ob das Programm irgendwann anhält oder endlos weiter läuft? Diese Frage ist als das Halteproblem bekannt, und Turings Beweis, dass sie nicht allgemein beantwortbar ist, gehört zu den folgenreichsten Erkenntnissen der theoretischen Informatik.

Die Beweisidee lässt sich ohne Formalismen leicht skizzieren. Angenommen, es gäbe ein Analyseprogramm H, das für jedes Programm P und jede Eingabe E korrekt vorhersagt, ob P bei Eingabe E anhält. Dann ließe sich ein neues Programm D konstruieren, das H als Baustein verwendet und wie folgt arbeitet: D nimmt ein Programm P als Eingabe, fragt H, ob P bei Eingabe P anhält, und tut dann das Gegenteil. Wenn H vorhersagt, dass P anhält, läuft D endlos weiter. Wenn H vorhersagt, dass P endlos läuft, hält D an.

Was würde nun passieren, wenn D sich selbst als Eingabe erhielte? Wenn H vorhersagt, dass D anhält, dann läuft D endlos weiter, also lag H falsch. Wenn H hingegen vorhersagt, dass D endlos läuft, dann hält D an, also lag H wieder falsch. In beiden Fällen irrt sich H. Das Analyseprogramm H kann also nicht existieren, weil seine Existenz zu einem logischen Widerspruch führt.

Das Halteproblem mag abstrakt klingen, aber seine praktische Bedeutung ist weitreichend. Jede Entwicklerin und jeder Entwickler ist ihm bereits begegnet, ohne es vielleicht so zu nennen: eine Endlosschleife, die nur unter bestimmten Bedingungen auftritt. Ein rekursiver Aufruf, der in einem Sonderfall nicht terminiert. Ein Deadlock, der sich erst unter Last manifestiert. All das sind Instanzen des Halteproblems. Die Frage „Wird mein Programm in diesem Fall jemals fertig?“ ist nicht generell beantwortbar. Und wenn es nicht einmal möglich ist, zuverlässig festzustellen, ob ein Programm jemals zu einem Ergebnis kommt, dann ist es erst recht nicht möglich, zuverlässig festzustellen, ob es das richtige Ergebnis liefert.

Was sich nicht entscheiden lässt

Das Halteproblem ist kein Einzelfall. Der Mathematiker Henry Gordon Rice bewies 1953 ein Theorem, das die Tragweite von Turings Ergebnis drastisch erweitert: Jede nicht-triviale Eigenschaft des Verhaltens eines Programms ist unentscheidbar. Nicht-trivial bedeutet hier, dass es mindestens ein Programm gibt, das die Eigenschaft besitzt, und mindestens eines, das sie nicht besitzt.

Die praktischen Konsequenzen sind erheblich. „Behandelt dieses Programm alle Fehlerfälle korrekt?“ ist eine nicht triviale Eigenschaft, also unentscheidbar. „Greift dieses Programm jemals auf unerlaubten Speicher zu?“ ist unentscheidbar. „Gibt dieses Programm für alle gültigen Eingaben die spezifizierte Ausgabe zurück?“ ist unentscheidbar. „Sendet dieses Programm jemals Daten an eine nicht autorisierte Adresse?“ ist unentscheidbar. Für keine dieser Fragen kann ein allgemeines Analysewerkzeug existieren, das für jedes beliebige Programm die korrekte Antwort liefert.

Das Theorem von Rice erklärt, warum die Suche nach dem einen Werkzeug, das alle Bugs findet, zum Scheitern verurteilt ist. Es handelt sich nicht um ein technisches Problem, das sich mit mehr Rechenleistung oder besseren Algorithmen lösen ließe. Es ist eine mathematische Grenze, so unverrückbar wie die Tatsache, dass sich ein Kreis nicht quadrieren lässt.

Das bedeutet nicht, dass statische Analyse nutzlos wäre. Linter und Werkzeuge zur statischen Codeanalyse finden sehr wohl Fehler, und sie finden sie zuverlässig. Aber sie beschränken sich auf bestimmte Muster, auf bekannte Fehlerklassen und eingeschränkte Programmstrukturen. Sie tauschen Vollständigkeit gegen Anwendbarkeit ein. Ein Analysator, der Null-Pointer-Dereferenzierungen in Java findet, löst nur ein sorgfältig eingegrenztes Teilproblem. Das ist nützlich und wichtig, aber es ist etwas fundamental anderes als ein Werkzeug, das garantiert alle Bugs findet.

Was formale Verifikation leisten kann

Angesichts dieser Grenzen stellt sich die Frage, wieso es formal verifizierte Software gibt. Der Mikrokernel seL4 etwa wurde mathematisch als korrekte Implementierung seiner Spezifikation bewiesen. Der C-Compiler CompCert wurde verifiziert, dass er die Semantik des Quellcodes beim Kompilieren korrekt erhält. Diese Projekte existieren, und sie funktionieren. Widersprechen sie nicht dem, was gerade dargelegt wurde?

Die Antwort liegt in den Einschränkungen, die formale Verifikation voraussetzt. seL4 umfasst etwa 10.000 Zeilen C-Code. Der Beweis seiner Korrektheit erforderte einen Aufwand, der auf etwa zwanzig Personenjahre geschätzt wird. Das ist ein Verhältnis von ungefähr zwei Personenjahren pro tausend Zeilen Code, das für eine typische Geschäftsanwendung mit Hunderttausenden oder Millionen von Codezeilen schlicht nicht tragbar ist. Selbst in Branchen, in denen Softwarefehler Menschenleben kosten können, wird formale Verifikation nur auf kleine, besonders kritische Komponenten angewendet.

Formale Verifikation beweist zudem immer nur die Korrektheit relativ zu einer Spezifikation. Sie sagt: „Dieses Programm verhält sich exakt so, wie die Spezifikation es beschreibt.“ Sie sagt nicht: „Die Spezifikation beschreibt das Richtige.“ Wenn die Spezifikation einen Fehlerfall nicht berücksichtigt, etwa die Möglichkeit, dass stdout auf eine volle Festplatte zeigt, oder dass ein Browser bestimmte Ports blockiert, dann ist das verifizierte Programm korrekt im formalen Sinne und trotzdem fehlerhaft im praktischen. Die Spezifikation zu schreiben ist selbst ein kreativer Akt, der denselben Unvollständigkeiten unterliegt wie die Softwareentwicklung insgesamt. Das Problem verschiebt sich also lediglich, es löst sich nicht auf.

Formale Verifikation hat außerdem eine Grenze, die direkt aus dem Halteproblem folgt: Sie lässt sich nicht vollständig automatisieren. Für jeden Beweis sind menschliche Einsichten nötig, Invarianten und Induktionsargumente, die eine Maschine nicht allgemein selbst finden kann. Das macht formale Verifikation zu einem mächtigen Werkzeug für sicherheitskritische Kernkomponenten, aber nicht zu einer skalierbaren Lösung für Software im Allgemeinen.

Fehlerfreiheit ist kein realistisches Ziel

Vom Hello-World-Bug über die Port-6000-Überraschung bis zum Halteproblem zeigt sich ein durchgängiges Bild: Vollständige Fehlerfreiheit in Software ist kein erreichbares Ziel. Das liegt nicht an mangelnder Sorgfalt oder unzureichenden Werkzeugen. Es liegt an mathematischen Grenzen, die für alle Programme gelten, und an der Natur von Tests als Stichproben, die niemals alle Lücken zwischen Annahmen und Realität schließen können.

Diese Erkenntnis ist kein Grund für Fatalismus, aber sie verlangt einen Wechsel der Perspektive. Die Frage sollte nicht lauten „Wie eliminieren wir alle Bugs?“, sondern „Wie gehen wir damit um, dass Bugs unvermeidlich sind?“. Die Antworten darauf sind bekannt: Defense in Depth, also mehrere unabhängige Schutzschichten statt einer einzigen, sodass der Fehler in einer Schicht von einer anderen aufgefangen wird. Monitoring und Alerting, um Fehler in Produktion schnell zu erkennen, statt darauf zu hoffen, dass es keine gibt. Fehlertolerante Architekturen, die mit dem Ausfall einzelner Komponenten umgehen können, ohne dass das Gesamtsystem zusammenbricht. Und schnelle Recovery-Prozesse, weil die Frage nicht ist, ob etwas schiefgeht, sondern wann.

Netflix hat mit dem Chaos-Monkey-Ansatz vorgemacht, wie das aussehen kann: Wenn regelmäßig absichtlich Komponenten abgeschaltet werden, ist das System gezwungen, mit Ausfällen umzugehen, und die Fehlertoleranz wird zum integralen Bestandteil der Architektur statt zum nachträglichen Zusatz.

Wer akzeptiert, dass Fehlerfreiheit eine Illusion ist, kann paradoxerweise also zuverlässigere Software bauen: durch Systeme, die mit Fehlern rechnen und trotzdem funktionieren. Die Mathematik hat der Softwarebranche eine harte Grenze gesetzt. Aber innerhalb dieser Grenze liegt noch sehr viel Raum für bessere Software, solange niemand den Fehler macht, Perfektion für ein erreichbares Ziel zu halten.

Das Halteproblem ist jedoch nicht die einzige fundamentale Grenze, an die Softwareentwicklung stößt. Sobald mehrere Rechner zusammenarbeiten sollen, taucht eine andere harte Grenze auf, die ebenso unveränderlich ist und in der Praxis ebenso oft unterschätzt wird. Der nächste Teil dieser Serie untersucht, warum verteilter Konsens so schwer ist und unter bestimmten Bedingungen sogar nachweislich unmöglich.

(who)