Expecting to see more like this, but good to really think about it: “Aver is a programming language for auditable AI-written code: verify in source, deploy with Rust, prove with Lean/Dafny”

It's not clear to me that the workflow of moving between spec, proof, deploy is really setup for iterative refinement the way I'd want here, but it's got a lot of good pieces!

https://github.com/jasisz/aver