NEAR Protocol pivots to AI-driven formal verification for smart contracts

The initiative follows NEAR AI’s recent performance on the PutnamBench, where automated agents resolved undergraduate-level mathematics challenges at an average cost of $0.17 per problem. While these results demonstrate technical progress, the transition to production-grade security requires a deeper integration of accurate software modeling. Developers must define specific properties of the software and construct proofs that verify these properties remain intact across all possible states.

NEAR co-founder Illia Polosukhin emphasizes that while AI-generated code presents significant opportunities, it necessitates rigorous mathematical verification to mitigate vulnerabilities. The protocol intends to use the Lean programming language and proof assistant, allowing AI agents to propose proofs that the Lean kernel then validates. This process complements traditional testing and code reviews by identifying logical inconsistencies that standard unit tests might overlook.

Applying these methods to live software remains a complex task. A formal proof can confirm that a contract preserves token balances during a transfer, but it does not automatically secure the entire application against every potential attack vector. Consequently, the team views this research as a layer of defense that sits alongside existing security practices. Other industry players, including Aptos Labs and Ethereum contributors like Vitalik Buterin, are similarly exploring AI to automate the verification of consensus mechanisms and cryptographic systems, marking a broader shift toward machine-checked security in decentralized networks.