Comment by joomy
5 hours ago
> 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.
Are LLMs part of your development workflow for something like this? If they are, is it through something like Claude Code or something else?
Very cool. Can't wait to see what's next with this project! Congrats on the huge scale of tests/examples as well.