Haven't seen much about SPARK and why3 recently, combined with frontier LLMs. It would seem easier to progressively prove properties from an actual implementation (going from absence of runtime errors to partial functional proof to full functional proof if you can beau the cost) and only focus the Lean effort on places where why3 (and its menagerie) of SMT provers give up ?

It would also seem highly agent-able since verification is very modular in SPARK.