NEAR AI, 핵심 계약의 정형 검증을 발전시키다

NEAR AI는 형식 검증을 더 쉽게 활용할 수 있도록 노력하고 있으며, 우선 NEAR Protocol과 핵심 스마트 컨트랙트를 대상으로 하고 있습니다. 형식 검증은 수학적 증명을 사용해 소프트웨어가 정해진 규칙을 준수하는지 확인합니다. 이는 테스트와 코드 리뷰를 보완하지만 완전한 보안을 보장할 수는 없습니다. 이번 노력은 Lean Eval v1 리더보드에서 총 해결 문제 수 기준 1위를 차지했다는 NEAR AI의 발표를 토대로 합니다. PutnamBench에서 이 시스템은 Lean 문제 672개를 해결했습니다. 문제당 비용은 약 0.17달러로 보고됐지만, 저장소에는 제출물의 모델 비용으로 111.85달러가 기재돼 있습니다. NEAR는 벤치마크 결과가 프로덕션 소프트웨어 검증에 드는 전체 비용이나 노력을 나타내는 것은 아니라고 강조합니다. 이미 배포된 컨트랙트에 형식 검증을 적용하려면 여전히 정확한 모델, 명확하게 정의된 속성, 그리고 구현과 일치하는 증명이 필요합니다. 보장은 검증한 속성과 가정에만 적용됩니다. 따라서 형식 검증은 테스트, 코드 리뷰, 운영 보안과 함께 이뤄져야 합니다. 이번 구상은 Aptos Labs와 Ethereum 공동 창립자 Vitalik Buterin이 논의한 작업을 비롯해 AI 보조 증명에 대한 폭넓은 관심을 반영합니다. NEAR 트레이더에게 이는 장기적인 보안 개선 가능성이지, 배포 발표나 토큰의 즉각적인 촉매는 아닙니다.