Autograding has been widely used in programming courses for decades. It reduces the marking load on teaching staff, providing them with more time to give higher quality feedback. There is relatively little work, however, on autograding in formal methods courses where the emphasis is not on programming, but on writing proofs and specifications. This paper describes a tool which employs the proof capabilities of Dafny to automatically grade students’ weakest precondition proofs and Dafny method specifications. The tool has been designed to (i) be reusable for new versions of assignments, with minimal input from teaching staff, (ii) allow fine-grained marking, in order to give students part marks for partially correct solutions, and (iii) not artificially constrain students’ use of programming techniques where they need to provide code as well as specifications, allowing them to apply best programming practices. The paper evaluates the use of the tool over two assignments of a course with 217 undergraduate and Masters students and highlights lessons learnt.