I think this is a nice idea. But to-be-filled-in postconditions of functions give this vulnerability to inconsistencies. Instead, you could ask them to fill in the body of a predicate. E.g., ask them to express formally what 'even' is provide the file

ghost predicate even(n: int)
   // TODO
   // write here what even means 

method EvenTest() {
  assert even(4);
  assert ! even(3);
}

Then this program will not verify unless a body is provided that satisfies the assertions in the test. (Note that with more complex definitions, the verification may fail although the body is correct. For example, if a student defines even as exists k :: 2 * k == n, the case even(4) will not verify without an additional assertion.)

Similarly, you could ask to give a body to the function max.

Is this what you are aiming for?