I’d like to see one of these systems designed around generating test suites for the specification. So, you’d prove your algorithm correct using some inefficient

I’d like to see one of these systems designed around generating test suites for the specification. So, you’d prove your algorithm correct using some inefficient representation (nats for integers or whatever) and then the verifier would detect edge cases and generate a junit test suite for the real implementation.