# Lanyon AI: formal verification for scientific computing

**URL:** <https://discourse.julialang.org/t/lanyon-ai-formal-verification-for-scientific-computing/139848>\
**Category:** Numerics\
**Created:** [October 5, 2026, 8:57pm UTC](https://discourse.julialang.org/t/lanyon-ai-formal-verification-for-scientific-computing/139848 "2026-10-05T20:57:10Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![berceanu](https://sea2.discourse-cdn.com/julialang/user_avatar/discourse.julialang.org/berceanu/32/11490_2.png) [@berceanu](https://discourse.julialang.org/u/berceanu)\
**Post date:** [October 5, 2026, 8:57pm UTC](https://discourse.julialang.org/t/lanyon-ai-formal-verification-for-scientific-computing/139848/1 "2026-10-05T20:57:11Z")

</div>

[Lanyon AI](https://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](https://lanyon.ai/research/) include PDE solvers and benchmarks.

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