Vitalik Buterin wil AI-bewijzen begrijpelijk maken voor ontwikkelaars

AI-bewijzen worden steeds belangrijker binnen Ethereum

Volgens Buterin is dat een belangrijke uitdaging nu AI steeds vaker wordt ingezet bij de ontwikkeling van software en blockchaintechnologie. Een duidelijkere programmeertaal moet ontwikkelaars helpen om sneller te begrijpen welke garanties een programma daadwerkelijk biedt.

Nieuwe programmeertaal richt zich op leesbaarheid

Het voorstel draait om een programmeertaal die direct kan worden omgezet naar bestaande systemen zoals Lean of HOL. Dat zijn zogenoemde proof assistants: programma’s waarmee ontwikkelaars wiskundige bewijzen schrijven die een computer stap voor stap kan controleren.

Binnen Ethereum wordt Lean al gebruikt om onderdelen van de blockchain te verifiëren, zoals cryptografische functies en de logica achter het consensusmechanisme. Dankzij deze methode kunnen fouten vroeg worden opgespoord voordat software in productie gaat.

Buterin stelt dat de technische tussenstappen van zo’n bewijs alleen mathematisch correct hoeven te zijn. Ontwikkelaars willen vooral de definities en conclusies kunnen lezen, omdat juist die uitleggen wat software precies garandeert.

AI schrijft sneller, mensen moeten sneller kunnen controleren

Grote AI-modellen kunnen inmiddels zelfstandig formele bewijzen genereren. Buterin noemt onder meer Claude, DeepSeek 4 Pro en Leanstral als systemen die hiervoor geschikt zijn.

Dat betekent echter niet dat ontwikkelaars automatisch begrijpen wat de AI precies heeft bewezen. Juist daar ziet Buterin ruimte voor verbetering. Zijn voorgestelde taal moet de beschrijving van software overzichtelijk houden, terwijl de onderliggende bewijzen volledig automatisch gecontroleerd blijven.

Een vergelijkbare aanpak gebruikt Ethereum al bij projecten waarbij een leesbare specificatie naast de technische code staat. Vervolgens controleert een formeel bewijs dat beide exact hetzelfde gedrag vertonen.

Onderdeel van de bredere Ethereum-strategie

Het idee sluit aan bij de bredere ontwikkeling van Ethereum. Binnen de zogeheten Lean Ethereum-roadmap werken onderzoekers aan software die steeds vaker formeel wordt gecontroleerd.

Ook de ontwikkeling van een formeel geverifieerde ZK-EVM past binnen die strategie. Een ZK-EVM is een versie van de Ethereum Virtual Machine waarbij gebruik wordt gemaakt van zero-knowledge proofs. Met deze techniek kan een computer aantonen dat een berekening correct is uitgevoerd zonder alle onderliggende gegevens openbaar te maken. Dat verbetert zowel de veiligheid als de schaalbaarheid van het netwerk.

Steeds meer consensussoftware binnen Ethereum wordt daarnaast met Lean gecontroleerd, zodat programmeerfouten al tijdens de ontwikkeling aan het licht komen.

Veiligheid krijgt extra aandacht

De timing van Buterins voorstel is opvallend. AI speelt een steeds grotere rol bij softwareontwikkeling, maar wordt ook gebruikt om kwetsbaarheden sneller op te sporen. Cybersecurity-onderzoekers zien dat AI steeds vaker onderdeel is van geavanceerde cyberaanvallen.

Volgens Buterin kan formeel gecontroleerde software een belangrijk verdedigingsmiddel worden. Wanneer ontwikkelaars eenvoudiger kunnen controleren welke eigenschappen software daadwerkelijk heeft, wordt het lastiger om verborgen fouten over het hoofd te zien.

Nog volop in ontwikkeling

De nieuwe programmeertaal bestaat voorlopig alleen als concept. Buterin heeft nog geen prototype of definitieve syntax gepubliceerd. Ook is nog onduidelijk of de Ethereum-gemeenschap uiteindelijk één standaard zal gebruiken of dat meerdere varianten naast elkaar ontstaan.

Toch laat het voorstel zien welke richting Ethereum op beweegt. AI zal waarschijnlijk steeds meer programmeerwerk uitvoeren, terwijl ontwikkelaars zich richten op het controleren van de resultaten en het bewaken van de veiligheid.

Conclusie

Met zijn nieuwe voorstel wil Vitalik Buterin AI en formele softwareverificatie beter op elkaar laten aansluiten. Door complexe AI-bewijzen leesbaarder te maken, kunnen ontwikkelaars sneller controleren of software doet wat zij verwachten. Dat kan niet alleen de veiligheid van Ethereum vergroten, maar ook bijdragen aan betrouwbaardere softwareontwikkeling binnen de bredere blockchainsector.

FAQ

Wat is een proof assistant?

Een proof assistant is software waarmee wiskundige bewijzen stap voor stap door een computer worden gecontroleerd. Hierdoor kunnen ontwikkelaars aantonen dat software zich exact volgens de specificaties gedraagt.

Waarom wil Vitalik Buterin een nieuwe programmeertaal?

Hij wil AI-gegenereerde formele bewijzen begrijpelijker maken. Ontwikkelaars kunnen daardoor sneller controleren welke garanties software biedt zonder alle technische details handmatig door te nemen.

Wat betekent dit voor Ethereum?

Als het voorstel wordt uitgewerkt, kan Ethereum veiliger worden doordat formeel gecontroleerde software eenvoudiger te ontwikkelen en te controleren is. Dat helpt bij de verdere professionalisering van het netwerk en de toepassingen die erop worden gebouwd.