Domains where fuzzing is useful are generally good candidates for formal verification, which I'm pretty bullish about in concert with LLMs. This is in part because you can just formal verify by exhaustiveness for many problems, but the enhancement is being able to prove that you don't need to test certain combinations through inductive reasoning and such.
That's an interesting idea. I hadn't thought about it, but it would be interesting to consider doing something similar for the porting task. I don't know enough about the space, could you have an LLM write a formal spec for a C function and the validate the translated function has the same properties?
I guess I worry it would be hard to separate out the "noise", e.g. the C code touches some memory on each call so now the Rust version has to as well.
