Lanyon AI: formal verification for scientific computing

Lanyon AI may interest people here. Their approach uses an LLM to propose a formal specification in a domain-specific language, then generates code and proofs together through symbolic methods.

Their research notes include PDE solvers and benchmarks.

Has anyone explored this approach, or how it could fit with Julia/SciML workflows?

This is a relevant paper: [2602.14853] BEACONS: Bounded-Error, Algebraically-Composable Neural Solvers for Partial Differential Equations

The Lanyon team has been developing the Gkeyll code, used for numerical simulations of plasmas.

I know they’re working on a DSL for LLMs that would allow them to do verifiable scientific research, in particular physics in the same way Lean allows this for pure math. So I was wondering if Julia community could learn something from this.

Definitely interesting!
Gorard was heavily involved in Wolfram’s (paraphrasing) “Physics as a hypergraph” project.