NEAR Targets AI-Assisted Formal Verification

NEAR Protocol has announced plans to apply AI-assisted formal verification to its network protocol and core smart contracts. According to an announcement from the company on Oct. 16, the research initiative seeks to reduce the specialist work and computing costs required to mathematically prove software follows defined rules.

The initiative follows a benchmark run where an AI agent solved 672 Lean problems from PutnamBench at a submission-time model cost of $111.85, according to the report. The mean cost was approximately $0.17 per problem using model prices at the time of submission.

Implementation Stages and Methodology

According to NEAR, applying automated proof generation to running software involves three distinct stages: representing a program mathematically, defining the properties it must satisfy, and constructing proofs to show those properties hold. NEAR AI's recent results demonstrate progress on the proof-construction stage.

The approach utilizes Lean, an open-source programming language and proof assistant. An AI agent proposes a proof, runs Lean, inspects feedback, and revises the attempt until the kernel checks whether the logic follows defined rules. NEAR co-founder Illia Polosukhin noted that achieving verifiable and mathematical guarantees of software behavior is necessary to address risks from AI-generated code and potential attacker tools.

Ecosystem Applications

Formal verification has prior documented applications within the NEAR ecosystem. Certora conducted a manual review of Rust contracts and formal specification and verification of a market contract for Templar, a lending protocol deployed on NEAR.

Other blockchain networks have similarly explored automated verification tooling. Aptos Labs described support for AI-assisted formal verification involving dynamic dispatch in Move contracts, while Ethereum co-founder Vitalik Buterin has discussed combining AI tools with machine-checked proofs across consensus and zero-knowledge systems.

Key facts

• NEAR Protocol announced plans on Oct. 16 to apply AI-assisted formal verification to its protocol and core smart contracts.
• NEAR AI reported solving 672 PutnamBench mathematics problems at a submission-time model cost of $111.85.
• The methodology utilizes Lean, an open-source programming language and proof assistant.
• NEAR stated that formal verification is intended to complement traditional testing, code reviews, and operational security practices.