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:
blog.brownplt.org/2024/07/07/l