Software that manages assets needs clear rules: who can move funds, how balances change, and what happens when an action fails. Formal verification gives developers a way to establish mathematically that software follows a precisely defined set of rules. Within the scope of those proofs and their assumptions, it can rule out errors that would otherwise lead to unintended or dangerous outcomes.
NEAR AI is researching how AI can make the formal verification process faster, more affordable, and accessible to more developers. NEAR AI recently reached #1 by total solves on the Lean Eval v1 formalization leaderboard, one of the benchmarks that measures automated proof work. One of the first goals is to formally verify the NEAR protocol and its core smart contracts, while also providing practical tools for ecosystem developers.
In Illia’s writing on software security, he argues that stronger verification is becoming more urgent as AI also helps attackers discover and exploit weaknesses.
“The future of AI, and AI-generated code, is exciting – but only once we achieve verifiable and mathematical guarantees of its behavior.”
— Illia Polosukhin, The Looming Security Armageddon No One Is Talking About
AI is already helping researchers uncover weaknesses in real software. As of August 26, 2026, Anthropic reported sending findings covering 2,300 potential vulnerabilities across 392 open-source projects to their maintainers, although not all had undergone independent validation. Those discoveries can also become targets for attackers. Google documented an AI-discovered flaw in BeyondTrust remote-access software being exploited within four days of public disclosure, with five additional threat clusters exploiting it within seven days.
For NEAR, this reinforces the motivation to make formal verification practical at scale: helping developers establish that critical software properties hold before deployment, alongside the ongoing work of finding and fixing vulnerabilities.
To understand NEAR’s progress, it helps to understand what formal verification actually does, why it has historically required substantial expertise and resources, and what the recent benchmark results measure.
What Is Formal Verification?
Formal Verification uses mathematical methods to establish that a system satisfies specified requirements. In the proof-based approach NEAR is pursuing, those requirements become mathematical statements, and a computer checks the proofs supporting them.
Imagine a simplified token transfer. A test might confirm that sending five tokens from Alice to Bob subtracts five from Alice’s balance and adds five to Bob’s. A formal proof could establish a broader rule: every successful transfer covered by the model preserves their combined balance.
In practice, a developer starts by choosing the rule to verify, for example, “a successful transfer must preserve the combined balance of both accounts.” They then represent the relevant code’s behavior mathematically and express that rule as a precise statement. A person or AI agent constructs a proof, and a proof checker verifies that it establishes the statement under the defined assumptions.
If the proof attempt fails, that does not automatically mean the code has a bug. The requirement might be incorrectly written, the code might violate it, or the agent might simply be unable to find a proof. Developers investigate the result and refine the code, specification, or proof as needed.
Several common terms can be used to describe the steps of this process:
- Specification: A precise description of the required behavior.
- Property: An individual requirement, such as “only an authorized account can withdraw funds.”
- Invariant: A property that must remain true as the system operates, such as an accounting rule preserved after every permitted transaction.
- Model: A mathematical representation of the relevant parts of a system.
- Formal Proof: A logical argument expressed in a form a computer can check.
Testing examines selected cases. A proof can establish a property for every case covered by its definitions and assumptions, without trying each one individually.
Proving that transfers preserve balances does not establish that only authorized users can initiate them. Authorization requires its own property. Developers must also establish that the model accurately represents the relevant behavior of the deployed software.
Formal verification, therefore, complements testing, code review, and other operational security best practices. It provides precise guarantees about specified behavior, rather than a blanket declaration that a system is secure.
Historically, formal verification has demanded deep expertise in mathematical logic, computer science, and specialized proof tools, skills often developed through years of graduate-level study or research. Experts must translate software behavior into mathematics, construct the relevant proofs, and maintain them as code changes. This meant formal verification was very expensive and resource intensive, and thus was mostly used for high-stakes, critical use cases where safety was non-negotiable and failure would be catastrophic and/or un-patchable.
Intel’s experience shows both why formal verification matters and the effort it can require. In 1994, a flaw in its Pentium processors caused certain division calculations to return incorrect results, resulting in a roughly $475 million charge against its earnings to cover the problem. In its later Pentium 4 project, Intel invested approximately 60 person-years of engineering effort in formal verification, checking more than 14,000 properties across key processor components.
Making these guarantees accessible to more developers means reducing the effort needed to produce them. AI can automate parts of the search for proofs, but that search also consumes computing resources. NEAR’s research aims to reduce both the specialist effort and computational cost, making verification practical across a wider range of software.
What Is Lean, and How Do AI Proof Agents Use It?
Lean is an open-source programming language and proof assistant, basically software for expressing mathematical statements and checking proofs. The first version was created in 2013, but the redesigned and stabilized version, Lean 4, was officially released for wider usage in 2023. NEAR AI’s PutnamBench work used Lean 4. Lean’s core proof checker, called the kernel, checks whether the resulting proof follows its logical rules.
An AI agent is software that uses an AI model and tools to work through a task. A proof agent can write a candidate proof, run Lean, read the feedback, and try again. Automated theorem proving means automating the search for proofs of mathematical statements.
The AI proposes the proof; the checker validates it. Developers do not need to accept a model’s explanation simply because it sounds convincing. They still need to review the statement being proved, its assumptions, and its connection to the software.
Illia describes NEAR’s approach in three parts: (1) represent the program in a form that can be reasoned about, (2) express the desired properties, and (3) construct proofs in Lean. NEAR AI’s recent benchmark work demonstrates progress on proof generation, which is part 3. The hope is that streamlining this effort will make verification practical for more applications and easier to maintain as code evolves.
What the Benchmark Results Measure
In general, researchers measure progress using benchmarks, which are defined collections of tasks that different systems attempt in order to measure and evaluate performance or value: they can establish a baseline across systems. A leaderboard, or scoreboard, records results such as accepted solutions and reported costs. It shows performance on those tasks under the stated conditions.
So why use mathematics problems to measure progress toward safer software? Once software behavior is represented mathematically, a requirement such as “a transfer preserves the combined balance” becomes a mathematical statement to prove. Producing proofs for difficult mathematics problems exercises a capability that software verification also needs.
The benchmarks help measure that proof-generation capability. Applying it to production software requires additional work: accurately representing the code, choosing the properties that matter, and ensuring the proof covers the implementation people actually use. Strong benchmark results show progress toward that goal.
NEAR AI’s recent results involve two benchmarks.
PutnamBench contains formalized problems from the Putnam undergraduate mathematics competition. “Formalized” means the problems have been translated into precise mathematical statements that a proof assistant can work with. The official leaderboard records 672 solved Lean problems for NEAR AI, with a mean reported cost of approximately $0.17 per problem.
NEAR AI’s public repository reports $111.85 at the model prices used for the submission. The result includes 670 upstream problems and corrected versions of two problems with defective formalizations. Its verification checks guard against incomplete proofs and changes to the statement being proved. The agent code is publicly available for inspection.
This is evidence of affordable proof generation on that benchmark. It is not the full cost of developing the system or an estimate for verifying a production contract. Low cost also does not necessarily mean instant results. The repository mentions that its longest run took more than three days – in this case, a deliberate choice to prioritize low cost over speed.
Lean Eval v1 evaluates difficult formalization problems. Its formalization leaderboard tracks total accepted solves, first solves, and unique solves. Rankings depend on which measure is selected. NEAR AI reached #1 by total solves on the Lean Eval v1 formalization leaderboard.
From Benchmarks to Production Code
These results build upon years of shared work by Lean developers, benchmark maintainers, researchers, and contributors to Mathlib, the community’s library of formalized mathematics. NEAR AI achieved this result because of that shared foundation.
It feels like we just ran a four-minute mile. We’ve shown that it is possible to have affordable automated proof generation, and now the gates are open to push further together. Every advance from NEAR, another research team, or an ecosystem developer gives all of us more to build on.
Now the goal is to bring that progress to the software people actually use. For NEAR, that means accurately modeling how systems behave, defining the properties that matter, and proving those properties hold in the code running in production.
The ambition is to make formal verification a normal, affordable part of building software, so the code people rely on in production is more secure and reliable. More real systems covered, more proofs anyone can check, and more developers able to catch flaws before they reach users. The benchmark results give us momentum. Now let’s turn that into stronger software.
Proven, not promised.
