Maybe. I honestly don’t know enough about theorum proving.
One nice thing about fuzz testing is that it tests both the concepts and the specific implementation. Probably 70% of bugs my fuzzers have found over the years are edge cases my code is handling incorrectly. If I made a “pure” model of my sync engine, wouldn’t I also, still, need to prove my actual implementation matches that model?
Ideally (part of) your model would already be executable, so that there is no separate implementation. Why have a separate implementation in C, JS, Java, Go, Dart, Swift, Rust, ..., if you have already something much cleaner which you have proven to be correct?
One nice thing about fuzz testing is that it tests both the concepts and the specific implementation. Probably 70% of bugs my fuzzers have found over the years are edge cases my code is handling incorrectly. If I made a “pure” model of my sync engine, wouldn’t I also, still, need to prove my actual implementation matches that model?