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?