Google affirme que ses agents IA ont fini de convertir Zircon, le noyau de son système d’exploitation Fuchsia, du langage C++ au langage Rust. L’annonce figure dans un billet de Google Research publié le 13 novembre 2026 et signé par Vahab Mirrokni, vice-président de Google Research.
Un quart du code avait déjà été porté vers Rust. En deux semaines, les agents ont réécrit le reste et ajouté environ 800 000 lignes de Rust. Le résultat réussit tous les tests automatiques du noyau, dits unitaires, et démarre sur des processeurs arm64. Le même billet annonce un décodeur vidéo réécrit en Rust plus rapide que l’original en C++, et une preuve mathématique de 50 millions de lignes vérifiée par machine.
Six semaines plus tôt, le 30 septembre, Google écrivait que ses agents « travaillent » à la migration du noyau, et sa version Rust du décodeur restait plus lente que le C++. Aucune vérification extérieure de ces chiffres n’a été publiée.
Un noyau contrôlé par ses tests d’origine
Selon la documentation de Fuchsia, Zircon est « la plateforme centrale qui fait fonctionner Fuchsia ». Il comprend un noyau et les quelques services qui démarrent le système, dialoguent avec le matériel et lancent les programmes. Le nouveau code est en Rust dit « sûr », la partie du langage qui exclut les erreurs de mémoire. Google ne précise pas qui a porté le premier quart du code.
Les agents s’appuyaient sur Gemini 4 Argon, le modèle de pointe annoncé par Google le 30 septembre (voir notre fiche sur Gemini 4 Argon). Ils étaient coordonnés par /teamwork, une fonction d’Antigravity, l’outil de programmation par agents de Google. Cette fonction répartit une longue tâche entre de nombreux agents aux rôles distincts.
Selon Google, les grands portages échouent quand les agents prennent des raccourcis. Ils remplacent des dépendances, les modules dont le code a besoin, par des coquilles vides, ou modifient les tests pour faire passer un code défaillant.
La nouvelle méthode de Google bloque ces raccourcis : un module n’est traité qu’une fois ses dépendances compilées, et chaque module en bout de chaîne est relié à « la suite de tests d’origine, non modifiée ». Google la promet dans Antigravity « bientôt ».
Un décodeur vidéo plus rapide que l’original
Le décodeur libgav1 de Google transforme les vidéos compressées au format AV1 en images. Les agents ont réécrit ce logiciel open source du C++ vers environ 170 000 lignes de Rust. Selon Google, le résultat est identique à l’original au bit près sur « une large suite de tests de conformité ».
La première version Rust tournait environ quatre fois moins vite que le C++. Les agents ont alors reçu des outils de profilage, qui mesurent où un programme passe son temps, et la consigne de « maximiser la vitesse sur des clips vidéo d’essai ». Sur ces clips, la version finale est 20 à 30 % plus rapide que l’original en C++ et en assembleur (le langage du processeur) optimisé à la main. L’écart vaut sur puces x86_64 comme ARM.
Sur le forum Hacker News, un participant a demandé ce qu’auraient donné les mêmes outils sur le code C++ ; le billet n’en dit rien.
La situation au 30 septembre
Le billet de lancement de Gemini 4 Argon, signé le 30 septembre par Koray Kavukcuoglu, de Google DeepMind, donnait l’état précédent. Les agents y « travaillent à migrer des bases de code C/C++ vers Rust dans tout Google », jusqu’à « plus de 800 000 lignes pour le noyau Zircon de Fuchsia ». Ces réécritures passent par « un audit automatisé et manuel rigoureux, des tests d’émulation et une relecture avant leur mise en production ».
Pour le décodeur, les agents étaient partis d’« un portage Rust existant ». Ils y avaient remplacé 32 000 lignes de code SIMD, qui traite plusieurs valeurs en une instruction. Ils avaient rendu ce portage 2,7 fois plus rapide, « ce qui le rapproche du C++ optimisé ». Le portage du 13 novembre est reparti du C++ : les deux séries de chiffres ne forment pas une seule courbe.
Côté mémoire, les agents avaient repéré des modifications qui libéreraient, une fois déployées, « plus de 300 Tio de mémoire » dans les centres de données de Google. L’économie totale était estimée entre 500 Tio et 1 Pio, soit jusqu’à environ un million de gigaoctets. Selon le billet du 13 novembre, les économies repérées depuis dépassent ce maximum.
Des preuves mathématiques contrôlées par Lean
En mathématiques, le contrôle revient à Lean, un assistant de preuve. Une démonstration y est formalisée, c’est-à-dire écrite sous forme de code, et Lean ne l’accepte que si chaque étape logique tient.
La preuve de 50 millions de lignes concerne la conjecture de Courtade-Kumar, formulée en 2013. Cette conjecture porte sur une suite de bits aléatoires envoyée dans un canal bruité, qui en inverse certains au hasard. Elle affirme qu’aucune règle qui résume l’entrée en un seul bit ne conserve plus d’information que la simple copie d’un des bits d’entrée. Des chercheurs de Google, de l’université chinoise de Hong Kong, de l’USC et de Carnegie Mellon l’ont démontrée dans un article mis en ligne le 21 septembre.
Selon Google, Gemini a d’abord trouvé des contre-exemples à une version plus large. L’équipe de Hong Kong a ramené le problème à une optimisation à 14 variables, puis les modèles Gemini ont établi l’essentiel des nouvelles bornes. L’équipe a enfin formalisé toute la preuve en Lean.
Deux autres équipes ont publié leur propre preuve sur arXiv, le site de prépublications scientifiques, le 21 septembre et le 22 septembre. Une quatrième a suivi le 3 novembre.
Un article du 4 novembre, signé Piaoyang Cui, Yiming Liu et David Woodruff, décrit le mieux la part des agents. Il porte sur la multiplication de matrices booléennes, des tableaux de zéros et de uns. À STOC 2024, un congrès d’informatique théorique, cinq chercheurs avaient franchi une barrière vieille de cinquante ans pour les algorithmes dits combinatoires de ce calcul. Ils demandaient si une borne nettement meilleure était possible, et l’article répond oui.
Sa section « AI Disclosure », sur l’usage de l’IA, précise que les humains ont choisi le problème et l’orientation. Les agents Gemini 4 « ont développé les preuves et les constructions algorithmiques à toutes les phases du projet ». Les humains ont vérifié et retouché le texte.
D’autres travaux revérifient des preuves anciennes. Les conjectures de Weil portent sur le nombre de solutions d’équations polynomiales ; la preuve de Pierre Deligne, publiée en 1974, a achevé de les démontrer. Selon Google, ses agents en ont produit « de façon entièrement autonome » une formalisation Lean d’environ 1,8 million de lignes, en 28 800 appels d’agents. La start-up Axiom Math avait publié sa propre formalisation en Lean le 6 novembre.
Selon Google, les agents ont aussi trouvé et corrigé une lacune dans une preuve publiée récemment, en formalisant la conjecture de Bochner-Riesz en dimension 3. Ce problème relève de l’analyse harmonique, qui décompose des fonctions en ondes. Sur Hacker News, Vahab Mirrokni résume ce volet par « au moins 10 problèmes ouverts de mathématiques et d’informatique théorique résolus ». Un article soumis le 6 novembre par des chercheurs de Google DeepMind et de Google Quantum AI décrit des agents qui ont trouvé des programmes quantiques jusqu’à 290 fois moins coûteux, prouvés corrects avec Lean.
Chimie, jeu de go et puces de Google
En chimie, 30 agents associés à un simulateur de spectres ont déterminé la structure de molécules à partir de mesures de résonance magnétique nucléaire, qui renseignent sur l’agencement des atomes. Selon Google, leur première réponse était exacte pour 95 % des molécules complexes d’un jeu de test, presque le double du score d’un agent seul.
Au go, sur le petit plateau de 9×9, des agents ont amélioré seuls, pendant moins de huit jours, un programme AlphaZero de base, qui apprend en jouant contre lui-même. Des humains fixaient les puces allouées et les règles d’évaluation.
Le programme a gagné environ 2 600 points Elo, l’échelle de niveau des joueurs, pour atteindre 1 885. Ce score se situe entre le programme open source KataGo réglé à 16 et à 32 visites (positions examinées) par coup. Vahab Mirrokni parle d’un « niveau Elo moyen ».
Chez Google, un processus d’agents a livré deux changements de planification qui ont réduit de 24 % les interruptions forcées de tâches sur certains types de TPU, les puces d’IA de l’entreprise.
Les limites de l’annonce
Le billet ne renvoie à aucun code du noyau converti ni du décodeur. L’arborescence publique de Fuchsia, son code source en ligne, contient bien des fichiers Rust dans le noyau Zircon, dont le fichier principal évoque une « conversion initiale vers Rust ». Google ne dit pas lesquels sont l’œuvre des agents.
Le dépôt de libgav1 demande toujours « un compilateur C++17 » et ne contient aucune version Rust. Le billet ne dit pas si le noyau tourne dans un produit.
Une suite de tests ne contrôle que ce qu’elle couvre, et Lean ne vérifie une preuve que par rapport à l’énoncé qu’on lui donne. Google le reconnaît : une preuve Lean ne tranche la question qu’« une fois que des mathématiciens ont confirmé que l’énoncé formel correspond au problème d’origine ».
Google indique que tout ce travail a été mené « en collaboration avec des experts humains ». Leur rôle reste le plus souvent imprécis, sauf dans l’article sur les matrices.
Notre analyse
En six semaines, le noyau est passé du chantier en cours au démarrage sur du vrai matériel. Selon Google, la meilleure version Rust du décodeur, plus lente que le C++ en septembre, le devance désormais.
Le noyau, le décodeur et la preuve reposent sur le même montage : de nombreux agents proposent des solutions, et des contrôles automatiques retiennent celles qui marchent. Ces contrôles ignorent qui a écrit le code ; Google les appelle des « falsificateurs ». Ce sont par exemple une suite de tests non modifiée, le vérificateur Lean ou un compteur matériel de performance.
Ce montage explique les volumes : un programme contrôle les 50 millions de lignes de la preuve. Le même schéma a servi à l’émulateur AWS écrit par des agents qu’Amazon a publié le 11 novembre pour imiter ses services en ligne.
Trois questions échappent à tout vérificateur. Les spécifications données aux agents étaient-elles les bonnes ? Le noyau Rust passera-t-il les audits de Google avant toute mise en production ? Quelqu’un hors de Google pourra-t-il reproduire ces résultats ?
Restent à surveiller l’arrivée de la méthode de réécriture dans Antigravity, l’identification éventuelle par Google du code des agents dans l’arborescence de Fuchsia et la publication du décodeur Rust.
Sources
- Advancing science & engineering with Antigravity’s /teamwork, Vahab Mirrokni, Google Research, 13 novembre 2026
- Gemini 4 Argon: our next era of frontier intelligence, Koray Kavukcuoglu, Google, 30 septembre 2026
- Combinatorial Boolean Matrix Multiplication in n³/2^Ω(√log n) Time, Piaoyang Cui, Yiming Liu et David P. Woodruff, arXiv, 4 novembre 2026 (révisé le 10 novembre 2026)
- A Proof of the Most Informative Boolean Function Conjecture, Zijie Chen, Amin Gohari, Adel Javanmard, Honghao Lin, Vahab Mirrokni, Chandra Nair et David P. Woodruff, arXiv, 21 septembre 2026
- Zircon, documentation de Fuchsia, consulté le 15 novembre 2026
- zircon/kernel, arborescence source de Fuchsia, Git at Google, consulté le 15 novembre 2026
- codecs/libgav1, dépôt de libgav1, Git at Google, consulté le 15 novembre 2026
- Advancing science and engineering with Antigravity’s /teamwork, discussion Hacker News avec des commentaires de Vahab Mirrokni, 14 novembre 2026
Image d’en-tête : graphique MACCUS, données de Google Research, 13 novembre 2026
