Lanyon AI discloses $10.6M round for formally verified scientific code

Why it matters

Formal verification can make AI-generated scientific software auditable, but its value depends on whether the certified specification captures the engineer's real intent.

Jonathan Gorard, Ammar Hakim, and James "Jimmy" Juno disclosed a $10.6 million initial fundraising round for Lanyon AI on Aug. 17, backing their attempt to make AI-generated scientific software prove that it does what its specification requires.

Dimension led the financing, with Industrious Ventures participating, according to Lanyon AI's announcement. The Princeton, New Jersey, research lab is targeting aerospace, propulsion, nuclear energy, physics simulations, GPU optimization, and AI inference, where a plausible answer can still be a dangerous one.

The round puts capital behind a founding team assembled from formal mathematics and computational plasma physics. Gorard, Lanyon AI's CEO, previously worked on automated theorem proving and quantum computing at Wolfram Research and co-founded the Wolfram Physics Project with Stephen Wolfram. Hakim, Lanyon AI's CTO, is a Princeton lecturer and principal research physicist whose work includes fusion, space plasmas, tokamak turbulence, and machine learning for partial differential equations. Juno, the chief scientist, is a Princeton Plasma Physics Laboratory researcher and core developer of the Gkeyll plasma simulation framework.

Their wager is that general-purpose coding agents start from the wrong language. "Why are agents still reasoning and coding in imperfect human languages?" Gorard asked in the Aug. 17 announcement. Lanyon AI instead wants its agent to reason through a condensed formal language built for mathematics, physics, and scientific computing.

One source for the code and the proof

Lanyon AI's architecture assigns creative work to an underlying language model, which proposes a formal specification in Lanyon AI's domain-specific language. A symbolic compiler then expands that specification into implementation code and a machine-checkable proof at the same time. If the specification cannot be proven, Lanyon AI says the system withholds the code and tries again.

That design targets a specific weakness in autoformalization systems. A conventional agent can write code and then produce a Lean proof that type-checks while describing a different implementation. Lanyon AI calls that failure "misformalization." Deriving both artifacts from one source is intended to prevent the proof from drifting away from the code it supposedly certifies.

The strongest evidence available so far comes from Lanyon AI itself. In company-run benchmarks published in July, Juno tested frontier models on linear advection and Maxwell equation solvers, using three trials for each model and detailed and terse prompts. Lanyon AI reported that its reference linear-advection solver took about seven seconds and roughly 800 output tokens to generate, while its Maxwell solver took about 23 seconds and roughly 600 tokens.

Those figures support a narrower claim than the August announcement's sweeping comparison with frontier models. The tests were designed, executed, and graded by Lanyon AI around scientific problems that fit its architecture. Independent replication has yet to establish how the approach performs across a wider set of engineering work.

Lanyon AI has also published six solver repositories on GitHub, covering advection-diffusion, Maxwell equations, general relativistic Maxwell equations, Burgers' equation, compressible Euler equations, and the electrostatic Vlasov equation. The repositories use C and Lean, giving researchers inspectable examples of the formal-verification work behind Lanyon AI's claims.

The specification remains the boundary

Formal verification establishes that an implementation conforms to a formal specification. It cannot automatically establish that the specification captures the user's actual scientific intent, physical assumptions, or deployment conditions.

Gorard acknowledged that boundary in Lanyon AI's July introduction. He distinguished the syntactic guarantee that code, proofs, and specifications match from the semantic problem of translating a user's natural-language request into the correct specification. Lanyon AI described semantic correctness as an open research area.

That distinction matters in the industries Lanyon AI is pursuing. A proof can certify a solver while leaving unanswered whether an engineer selected the correct governing equations, boundary conditions, material properties, or failure thresholds. Lanyon AI's product challenge is therefore concentrated at the interface between the engineer and the formal language. The symbolic compiler can police everything downstream only after that interface produces the right specification.

The market is already attracting technically ambitious teams. Axiomatic AI disclosed an $18 million seed round in March 2026 for verification-focused engineering AI, while Harmonic has concentrated its Aristotle system on formal mathematical reasoning and verified software. Lanyon AI is carving out a position closer to executable simulations and numerical methods, drawing directly on Hakim's and Juno's experience building software for plasma physics.

The investor lineup follows that industrial direction. Dimension describes its mandate as investing across science and compute. Industrious Ventures focuses on aerospace, energy, manufacturing, and other physical industries where software errors collide with hardware costs and safety requirements.

Lanyon AI is still presenting a research program rather than a fully documented commercial business. Its public materials do not establish pricing, customer adoption, or a general product release. The company page is recruiting research scientists and engineers in formal verification, computational physics, applied mathematics, and AI infrastructure.

The founders have produced a coherent technical thesis and exposed enough code to make parts of it inspectable. Their next test is turning that architecture into a system engineers can use without shifting the hardest error from generated code into the specification that controls it.