It's very exciting to see the work on combining AI models with static analysis, test generation, formal proof, and refactoring. All of these suggests we might see high assurance (EAL6+) developed rapidly in the future. At least for combinations of well-understood concepts.
You don't mention generating code from scratch; is that on purpose? Perhaps a developer could add many constraints that would have been too expensive previously - e.g., code in Spark, use only these ___ system calls, never use this riskier capability, use only these ___ libraries, etc.
The LLM might take longer than otherwise, but still be fast enough. The new technology, like every useful one, changes the tradeoff equation.