> Have you considered combinatorial testing?

Our plan was to do random Rocq program generation and differential testing of Crane extracted code versus other extraction methods and even CertiCoq. But fixing a program and trying different mappings would certainly be a useful tool for any dev who would like to use our tool, and we should put it on our roadmap.

Very cool. Can't wait to see what's next with this project! Congrats on the huge scale of tests/examples as well.