> I believe this is called model-code gap and there are ways to address it but I haven't found an easy-to-follow approach.

I would say Ada SPARK solves this problem.

Not just that, I've been seeing a huge effort in the Ada community to leverage LLMs to convert a lot of libraries into formally verified SPARK code. One of the biggest issues I see with vibe coded stuff is that it's difficult to review and difficult to prove that it's doing what you think it's doing, but with a strongly type language like Ada and formal verification with SPARK, LLM output is easy to read and easy to prove.