Si Vitalik Buterin, co-founder ng Ethereum, nag-suggest ng bagong programming language na automatic mag-compile papunta mismo sa Lean o HOL, mga proof assistant na gamit sa formal verification.
Naitarget ng idea na ‘to ang isang specific na problema: Kapag nagkaroon ng AI-generated na mga proof—karaniwan mas mabilis at madami kesa kaya tapusin ng kahit sinong tao—konti lang talaga ang madaling makaka-confirm kung ano bang napapatunayan ng output na ‘yun.
Programming Language para sa Mga Nagche-check ng AI Proofs
Ang Lean ay isang proof assistant o software na ginagamit ng mga mathematician at engineer para magsulat ng proof na kayang i-check ng computer, step by step. Ginagamit na rin ‘to ng Ethereum researchers para i-verify ang cryptographic code at consensus logic ng network. Nasa 60 years na rin mula nang nag-start ang mga proof assistant, pero hanggang ngayon medyo niche pa rin ang field na ‘to.
Sa kanyang post, sinabi ni Buterin na isang requirement lang talaga ang mahalaga para sa internal steps ng isang proof: mathematically correct dapat, wala nang iba. Hindi rin naman tinitingnan ng reader yung mismong detalye ng steps. Yung definitions at theorems ‘yung madalas binabasa ng tao para maintindihan kung ano talaga shinashow ng software na ‘yon.
Sa isang blog post din ni Buterin noong May, pinag-usapan niya ang ganitong division. Dito, pinapakita ng isang mathematical proof na tugma ang mabilis na low-level code sa hiwalay at mas madaling maintindihang spec, kaya kapag na-audit mo yung isa, covered na rin yung kabila.
Pantay din ang timing nito sa sariling rebuild effort ng Ethereum na tinatawag na Lean Ethereum roadmap. Gamitin din ng mga researchers ang katulad na method sa pag-create ng formally verified ZK-EVM o zero-knowledge na EVM (Ethereum Virtual Machine).
AI ang Gumagawa ng Proofs, Mga Tao ang Nagche-check ng Claims
Marunong nang gumawa ng gamit na Lean proofs ang mga sikat na large language models ngayon. Tinukoy ni Buterin yung Claude at Deepseek 4 Pro bilang malalakas na tools, kasama pa si Leanstral na mas maliit pero specific para sa Lean. May project din na tinatawag na evm-asm kung saan na-verify ang EVM implementation kontra sa mas madaling basahin na reference. Ganitong kakayahan yung pinakita rin ng developers sa mga sumali dati sa AI challenge ni Buterin, na nasagot ng mga testers after only a few hours.
Hindi lang tungkol sa convenience ang issue. Napansin din ng mga security researchers na dumami ang AI-assisted exploit attempts ngayong taon. Yung formally verified na code ay isa sa mga panlaban dito. Kung mas friendly para sa devs ang specification language, mas madali na nilang i-check yung claims nang hindi na kailangan basahin bawat detalye ng proof.
Ano Pa sa Labas ng Ethereum Research Scene?
Tuloy-tuloy parin sa pag-experiment si Buterin at kamakailan lang niyang na-demo ang isang anonymous billboard gamit zero-knowledge proofs. Pinakita dito paano napupunta mula research papuntang working product ang mga tech na ‘to. Sinimulan narin ng mga researchers na i-verify ang consensus clients ng Ethereum sa Lean para mas mabilis mahuli ang bugs.
Sobrang ramdam pa rin ‘yung pattern: hihiwalayin ang mabilis na code mula sa claim na madaling intindihin, tapos ipapakita na magka-match sila.
Wala pang working prototype ng bagong language na ‘to at open pa ang magiging syntax. Baka magkaisa ang mga devs sa isang standard, o baka madaming iba’t ibang versions ang mangyari. Kung alin ang mangyari, malaki’ng epekto nito kung gaano kabilis makarating sa production ang AI-verified na code.
