Fully verifiable programming is much “better” with LLMs. This recent one, for example:
huggingface.co/mistralai/Leanstral-2603
Leanstral is the first open-source code agent designed for Lean 4, a proof assistant capable of expressing complex mathematical objects such as perfectoid spaces and software specifications like properties of Rust fragments.