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.