NEAR Protocol outlined plans in an Oct. 16 announcement, reiterated on Oct. 19 via X, to apply AI-assisted formal verification to its network protocol and core smart contracts after reporting that NEAR AI solved 672 PutnamBench mathematics problems at a submission-time model cost of $111.85.
The research aims to reduce the specialist work and computing costs involved in proving that software follows defined rules. The $111.85 figure reflects a mathematics benchmark based on the Putnam undergraduate competition, with a mean of roughly $0.17 per problem, and excludes the full cost of developing the system or estimating the price of verifying production contracts. The project's public repository describes the result as 670 upstream problems plus corrected versions of two problems with defective formalizations, while replaying the same usage at later DeepSeek off-peak prices would cost $331. The team also reported that its methodology included unsuccessful attempts and that the longest run lasted more than three days.
NEAR said applying the research to production software involves three stages: representing a program mathematically, defining the properties it should satisfy, and constructing proofs that those properties hold. The benchmark results demonstrate progress on the third stage, but production verification still requires accurate models of software behavior and a clear connection between proofs and the implementation users rely on. The approach uses Lean, an open-source proof assistant, where an AI agent can propose a proof, run Lean, inspect feedback, and revise the attempt while Lean's kernel checks whether the proof follows logical rules. NEAR cautioned that an unsuccessful attempt does not necessarily identify a software flaw: the requirement may be wrong, the implementation may violate it, or the agent may fail to find a valid proof.
NEAR co-founder Illia Polosukhin linked the research to risks from AI-generated code. "The future of AI, and AI-generated code, is exciting - but only once we achieve verifiable and mathematical guarantees of its behavior," he said. NEAR stressed that formal verification should complement testing, code review and operational security practices, and that a proof covering one accounting rule is not a guarantee that an entire application is secure.
Formal verification already has documented uses in the NEAR ecosystem. Certora's March 30 assessment of Templar, a lending protocol deployed on NEAR, described manual review of its Rust contracts and formal specification and verification of its market contract. Other blockchain teams have pursued similar work: Aptos Labs in May described support for AI-assisted formal verification involving dynamic dispatch in Move contracts, and Ethereum co-founder Vitalik Buterin has discussed AI tools combined with machine-checked proofs across Ethereum's roadmap while cautioning that proving one layer does not establish that an entire system behaves as intended.
NEAR's security research also includes quantum-resistant signing. Near One's May proposal selected FIPS-204 signature support using the ML-DSA standard approved by the U.S. National Institute of Standards and Technology, with a testnet target for the end of the second quarter of 2026.
