formal verification of artefacts: famously very approachable, pretty reasonable to set verifying something like a C compiler for a graduate class.

Oh, wait. it't not that easy. oh. oh well I'm sure the LLMs will be fine and won't cheat the test