We've spent several years understanding what makes linear temporal logic (which is used in verification, planning, and much more) tricky for humans. Now expanded to finite-trace LTL (LTLf) as well. Lots of material usable off-the-shelf for educators! See:
https://blog.brownplt.org/2024/07/07/little-tricky-logics-2.html