We report our experience in enhancing automated grading in an undergraduate programming course using formal verification. In our experiments, we deploy a program verifier to check the equivalence between student submissions and our reference solutions, alongside the existing testing-based grading infrastructure. We collect and analyse over 1,700 student submissions to 11 programming exercises and show how our grader can prove submission correctness and report counterexamples. Beyond functional correctness, we were able to use the outcome of equivalence checks to differentiate student submissions according to their high-level program structure, in particular their recursion pattern, even when their input–output behaviour is identical. Consequently, we achieve (1) higher confidence in correctness of idiomatic solutions but also (2) more thorough assessment of solution landscape that reveals solutions beyond those envisioned by instructors.

@article{paperbot3944,
  title = {Formal Autograding in a Classroom (Extended Version)},
  author = {Dragana Milovančević and Samuel Chassot and Mario Bucev and Marcin Wojnarowski and Viktor Kunčak},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {48},
  number = {3},
  year = {2026},
  doi = {10.1145/3828727}
}