Former researchers from Axiom Math and Kimi have teamed up to launch a startup leveraging AI to solve the challenging problem of chip verification.

Insight Beating AI Express: One of the biggest fears in chip design is discovering logic errors only after manufacturing. Such issues often require full re-design and re-fabrication, leading to exorbitant costs. Chip verification’s core goal is to uncover these hidden errors as early as possible before production. Traditional verification relies heavily on simulation testing, but the number of possible internal operating state combinations in a chip is astronomical, making exhaustive testing impossible. Formal verification, by contrast, uses mathematical methods to prove a chip consistently complies with specified rules under defined conditions. For instance, two circuits that should never activate simultaneously must not turn on together under any special operation. While formal verification has existed for some time, mathematical proofs for complex chips are extremely challenging. Many problems require manual work from experts, and existing tools often fail to deliver results due to excessive computational scale. According to Leiphone, Zhang Jujian, former head of formal verification at Axiom Math, and Liu Junqi, who previously researched AI mathematics at Moonshot AI, have co-founded Beijing Rational Number Technology, which leverages AI to automate more formal verification tasks for chips. The startup has completed a seed round of financing. Both founders boast strong backgrounds in mathematical proof: Zhang contributed to the development of Mathlib and AxiomProver; Liu is the core author of Numina-Lean-Agent, a system that successfully solved all 12 problems in the 2025 Putnam Mathematical Competition, with its proofs verified via the Lean tool. Currently, Rational Number has a working technical prototype. In a chip project involving over 100,000 lines of RTL code, the team verified assertions that some existing EDA tools cannot determine. The company is collaborating with chip clients to commercialize this capability into a verification service.