Write tests for your C code. Run c2rust (mechanical translation), including the tests. Let a LLM/MCTS/verifier loop go to town. Verifier here means it passes compiler checks, tests, santiziers and miri.

Additional training data can be generated by running mrustc or by inlining unsafe code (from std/core/leaf crates) into safe code and running semantics-preserving mechanical refactorings on the code.

This can be closer to AlphaProof than ChatGPT