My version of dafny flags a compilation error if the program contains "assume" statements, but does not complain if it contains ghost methods with no bodies (which amounts to the same thing).
Similarly, /noCheating:1 does not complain about miraculous ghost methods.
I wonder whether it would be consistent to organise things so that
(1) Dafny -will- compile programs with assume statements (simply ignoring them, as it does miraculous ghost methods). Maybe someone wants to test their program before it's fully proved?
(2) Dafny /noCheating:1 -won't- allow miraculous ghost methods. A good use of noCheating would be to make sure that there remain absolutely no holes (unproved lemmas) of any kind, ie that you really are finished.