This has worked very well in mathematics at Imperial College, London, having undergraduates provide machine-verifiable proofs in the Xena project. They use a no

This has worked very well in mathematics at Imperial College, London, having undergraduates provide machine-verifiable proofs in the Xena project. They use a nonconstructive axiomatic framework (so not really "software", I suppose) in the Lean logical framework. https://xenaproject.wordpress.com/2018/10/07/what-is-the-xena-project/ https://xenaproject.wordpress.com/2018/10/07/what-is-the-xen...