Former Axiom Math and Kimi researchers team up to start a business, using AI to tackle chip verification challenges.

Beating AI News Flash: One of the biggest fears in chip design is discovering logic errors only after manufacturing. Once a problem arises, it may require redesign and new tape-out, incurring high costs. Chip verification is about finding these hidden errors as much as possible before manufacturing.

Traditional chip verification mainly relies on simulation testing, but the combinations of internal operating states in a chip can reach astronomical numbers, making it impossible to test them one by one. Formal verification uses mathematical methods to prove that a chip always obeys a certain rule under specified conditions. For example, two circuits that should never be turned on at the same time must never be turned on together due to some special operation.

This method has long existed, but mathematical proof for complex chips is very difficult. Many problems require experts to handle manually, and existing tools may fail to reach a conclusion because the computational scale is too large.

According to Leiphone, Zhang Jujian, former head of formal verification at Axiom Math, and Liu Junqi, who previously researched AI mathematics at Moonshot AI, founded Beijing Youlishu Technology to use AI to automatically complete more chip formal proof work. The company has completed a seed funding round.

Both have strong backgrounds in mathematical proof. Zhang Jujian participated in the development of Mathlib and AxiomProver. Liu Junqi is a core author of Numina-Lean-Agent, a system that successfully proved all 12 problems in the 2025 Putnam Mathematical Competition and verified the proof process through the Lean tool.

At present, Youlishu has completed a technical prototype and, in a chip project involving more than 100,000 lines of RTL code, verified some assertions that existing EDA tools could not determine. The team is working with chip customers to try to turn this capability into a commercial verification service.