Lanyon AI discloses $10.6M round to make physics code prove itself

Lanyon AI, a Princeton, New Jersey-based lab co-founded by applied mathematician Jonathan Gorard and computational physicists Ammar Hakim and James Juno, emerged from stealth on August 17 after closing a $10.6 million financing round in July, led by Dimension with participation from Industrious Ventures and angel investor Siqi Chen. The company is building an AI agent that generates scientific simulation code with machine-checkable mathematical proofs, targeting aerospace, propulsion, and nuclear energy fields where verifiable computation is critical.

Jonathan Gorard @getjonwithit https://x.com/getjonwithit , an applied mathematician who previously worked at Wolfram Research and Princeton, is taking a narrower route into AI-generated code: make the software prove that it does what its formal specification says. Lanyon AI https://lanyon.ai/ , which Gorard co-founded with computational physicists Ammar Hakim @minmodammar https://x.com/minmodammar and James "Jimmy" Juno @JunoRavin https://x.com/JunoRavin , said in an August 17 press release https://www.prnewswire.com/news-releases/lanyon-ai-emerges-from-stealth-to-build-the-future-of-scientific-and-technical-computing-302852383.html that it had emerged from stealth after closing an initial $10.6 million financing in July. Dimension https://www.dimensioncap.com/ led the round, with participation from Industrious Ventures https://industrious.vc/ and angel investor Siqi Chen https://mercury.com/investor-database/siqi-chen , according to Lanyon AI's announcement. The Princeton, New Jersey-based lab is building an AI agent, also called Lanyon, that generates scientific simulation code and accompanying mathematical proofs. Lanyon AI is initially pitching the system at aerospace, propulsion, nuclear energy and other fields where a plausible-looking answer is of little use if engineers cannot verify the underlying computation. Gorard, Hakim and Juno met while working at the Princeton Plasma Physics Laboratory, Industrious Ventures said in its investment announcement https://industrious.vc/resource/announcing-our-investment-in-lanyon-ai/ . Their research covered plasma environments in fusion reactors and around black holes. Princeton records show Gorard joined its research software engineering group in 2024 to work on Gkeyll, a multiphysics simulation framework led by Hakim. Gorard holds an MPhil in scientific computing from the University of Cambridge and previously held roles at Cardiff University, Wolfram Research and the Wolfram Institute. Lanyon AI says he helped co-found the Wolfram Physics Project with Stephen Wolfram. Hakim's work spans fluid mechanics, nuclear fusion and aerospace engineering, while Juno has focused on laboratory, space and astrophysical plasmas. That background predates the fundraising pitch. Gorard and Hakim published a formal verification pipeline for hyperbolic partial differential equation solvers in 2025. The trio followed in February 2026 with BEACONS https://arxiv.org/abs/2602.14853 , a framework for producing neural solvers with machine-checkable guarantees around properties including convergence, stability and conservation. Lanyon splits creativity from verification Lanyon AI's architecture assigns different jobs to language models and symbolic software. An LLM proposes a specification in a domain-specific formal language. Deterministic systems then expand that specification into executable C code and proofs in Lean, a theorem-proving language. If the proof process fails, Lanyon AI says the implementation is not generated. The distinction matters because asking a language model to write code and separately produce a proof creates another failure point: the proof may verify a different specification from the one the code implements. Lanyon AI's system derives the implementation and proof from the same formal source. That design supports a narrower guarantee than Lanyon AI's broadest claims might suggest. In its July launch post https://lanyon.ai/blog/welcome/ , Lanyon AI initially described the agent as mathematically incapable of making a mistake. A footnote qualified that assertion: Lanyon AI guarantees that the implementation matches the formal specification, while determining whether the specification captures the user's natural-language intent remains an open research problem. The practical risk therefore moves upstream. The generated code can faithfully implement a specification that does not express what the engineer actually wanted. Lanyon AI's technical case depends on reducing that semantic gap while preserving the formal guarantees that distinguish the product from conventional coding agents. Lanyon AI has begun publishing examples through its GitHub organization https://github.com/lanyonai/ , including formally verified solvers for Maxwell's equations, compressible Euler equations, advection-diffusion systems and electrostatic Vlasov equations. The repositories provide inspectable code and Lean proofs, though Lanyon AI's wider performance and cost comparisons remain based on benchmarks produced by Lanyon AI. The investors cover research and industrial sales The investor lineup maps closely to the founders' problem. Dimension describes itself as a research-oriented investment firm focused on science and computing. Industrious Ventures invests across aerospace, energy, manufacturing, national security and other industrial sectors that Lanyon AI wants to sell into. Gorard wrote that the founders were "three nerdy theorists fresh out of academia" who needed access to customers in aerospace, nuclear and defense. Industrious Ventures supplies those relationships. Dimension gives Lanyon AI room to operate as a research lab while the founders develop a commercial product around their formal methods work. Chen provided the earliest money. Gorard said Chen's investment paid for Lanyon AI's first office, computers and legal counsel during the rest of the fundraising process. The $10.6 million gives the founders time to convert years of research into production software and find buyers willing to put AI-generated simulation code near expensive physical systems. Lanyon AI has shown that proofs can be generated alongside code. Its commercial test is whether engineers trust the specification process enough to use the output.