There is some really promising-looking work on using a mixture of LLMs and formal proof techniques and/or unit testing to perform reliable and idiomatic transla

There is some really promising-looking work on using a mixture of LLMs and formal proof techniques and/or unit testing to perform reliable and idiomatic translation from unsafe to safe languages. See, for example, https://arxiv.org/abs/2503.12511v2 https://arxiv.org/abs/2503.12511v2 and https://arxiv.org/abs/2409.10506 https://arxiv.org/abs/2409.10506, and https://arxiv.org/abs/2503.17741v1 https://arxiv.org/abs/2503.17741v1 The nice thing about this approach is that the LLMs don't need to be flawless for it to work, as the formal analysis / unit testing will keep their errors at bay - they just need to be good enough to eventually output something that passes the tests.