이더리움 공동 창립자인 비탈릭 부테린은 새로운 프로그래밍 언어를 제안했습니다. 이 언어는 렌 또는 HOL과 같은 형식적 증명 보조 시스템으로 직접 컴파일됩니다.
이 아이디어는 사람들이 AI 결과를 읽는 방식에서의 특정한 격차를 겨냥합니다. 인공지능은 점점 더 빠르게 방대한 양의 자동화된 증명을 만들어내고 있습니다. 이는 어느 인간 팀보다 훨씬 빠른 속도입니다. 대부분의 독자는 이 증명이 실제로 무엇을 입증하는지 신속히 확인하지 못합니다.
AI 증명 검토만을 위한 언어
렌은 증명 보조 도구이며, 수학자와 엔지니어는 이를 사용해 컴퓨터가 한 줄씩 검사할 수 있는 증명을 작성합니다. 이더리움 연구진은 암호화 코드와 합의 논리 검증을 위해 이미 렌을 사용하고 있습니다. 증명 보조 도구는 거의 60년 동안 존재해왔지만, 이 분야는 여전히 소수의 사람들에 의해 주로 연구되고 있습니다.
비탈릭 부테린은 자신의 게시글에서 증명의 내부 단계는 오직 하나의 요건만 충족하면 된다고 주장했습니다. 그 요건은 수학적 정확성뿐입니다. 독자는 그 과정을 직접 검토하지 않습니다. 정의와 정리는 다르게 작동합니다. 사람들은 소프트웨어가 실제로 어떤 것을 보장하는지 배우기 위해 그 부분을 읽습니다.
부테린은 5월 블로그 게시글에서도 관련된 구분을 다루었습니다. 여기서는 수학적 증명을 통해 효율적인 저수준 코드가 별도의 읽기 쉬운 명세와 일치함을 보여줍니다. 따라서 한 번의 감사로 두 가지 버전을 동시에 검토할 수 있습니다.
그의 제안 시점은 이더리움 자체의 재구축 프로젝트와도 일치합니다. 이 노력은 별칭으로 렌 이더리움 로드맵이라 불립니다. 연구진은 한편, 형식적으로 검증된 ZK-EVM도 개발 중입니다. 이는 이더리움 가상머신(EVM)의 영지식 증명 버전으로, 유사한 방법을 활용합니다.
AI가 증명을 작성하고, 사람이 주장만 점검합니다
대형 언어 모델은 이미 실제로 활용 가능한 렌 증명을 작성할 수 있습니다. 부테린은 클로드와 딥시크 4 프로, 그리고 렌에 특화된 소규모 모델인 린스트랄을 유용한 도구로 꼽았습니다. 예시 프로젝트로는 EVM 구현체인 evm-asm이 있습니다. 이 구현체는 읽기 쉬운 참고 자료와 검증이 이루어졌습니다. 이 능력은 최근 부테린 AI 챌린지에서 개발자들이 보였던 논리적 사고와 일맥상통합니다. 테스트 참가자들은 몇 시간 만에 그 챌린지를 해결했습니다.
중요성은 단순한 편리함을 넘어서고 있습니다. 보안 연구원들은 올해 AI가 도운 악용 시도의 급증을 추적했습니다. 형식적으로 검증된 코드는 이런 추세에 대한 방어책이 될 수 있습니다. 더 친근한 명세 언어가 도입된다면, 개발자는 복잡한 증명 절차를 모두 살피지 않고도 주장을 점검할 수 있습니다.
이더리움 연구 집단을 넘어서
비탈릭 부테린은 이 아이디어들을 최근 공개적으로 계속 실험하고 있습니다. 그는 영지식 증명을 적용해 익명 빌보드 데모를 선보였습니다. 이 시연은 검증 가능한 주장이 연구 저장소에서 실제 제품으로 옮겨질 수 있음을 보여주었습니다. 연구진은 또한 렌으로 합의 클라이언트를 공식적으로 검증해 초기 버그를 발견하기 시작했습니다.
이 방향은 여전히 익숙한 패턴과 닮았습니다. 빠른 코드는 읽기 쉬운 주장과 구분하고, 두 가지가 일치함을 입증합니다.
아직 새로운 언어의 프로토타입은 존재하지 않습니다. 부테린은 정확한 문법 역시 확정하지 않았습니다. 개발자들이 하나의 공통 표준에 합의할 수도 있고, 여러 개의 호환되지 않는 방언을 선택할 수도 있습니다. 이 선택은 AI로 검증된 코드가 실제 시스템에 적용되는 속도를 좌우할 수 있습니다.
