Sure, this is simple! You provide them with a definition written in Coq and make them implement a proof that their implementation satisfies that definition. Use probabilistic couplings to make sure the output of the biased coin function adheres to specified distribution.

You can easily implement a grader that checks the the proof.