quote: NEAR AI is now #1 on Lean Eval v1, Lean FRO's active benchmark of extremely hard formalization problems. The system runs almost entirely on open-weight DeepSeek V4.1 Flash, so it's low cost and has no third-party model dependency. This work lays the groundwork for formally verifying NEAR Protocol and core contracts, and for a tool any team can use to verify its own. | NEAR AI has claimed first place on the Lean Eval v1 leaderboard. Lean Eval v1 is an active benchmark maintained by Lean FRO that contains extremely hard formalization problems. We reached first place despite joining the competition just four weeks ago, a full month later than other top participants. NEAR is very heavily investing in formal verification efforts. Our ultimate goal is to formally prove the protocol and all the core contracts, and to provide a practical tool for others to formally verify their contracts in a fast and affordable way. The system that enabled us to claim first place is almost entirely powered by DeepSeek V4.1 Flash, and thus is (a) extremely cheap, and (b) has no dependencies on third parties because the model is open weight. When it comes to formally verifying software, the approach boils down to three pillars: 1. Representing the program in a way that can be reasoned about; 2. Expressing the properties that we desire to prove; 3. Coming up with a proof and formalizing it in Lean. Until recently, step (3) was prohibitively expensive for practical use at scale. With the system that we used for Lean Eval, we now have it solved. Stay tuned for updates on how we apply it in practice to formally verify NEAR contracts.