The hard stuff aseipp alludes to supposedly can be learned with these books: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.ed

The hard stuff aseipp alludes to supposedly can be learned with these books: https://www.cis.upenn.edu/~bcpierce/sf/current/index.html https://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ A book on refinement calculus that connects high-level specs to low-level implementations: http://lara.epfl.ch/w/_media/sav08:backwright98refinementcalculus.pdf http://lara.epfl.ch/w/_media/sav08:backwright98refinementcal... My favorite illustration using Event-B of how requirements and specs can explode into many verification conditions for even something simple. You're explicitly handling both the stuff that's usually unstated and the needs of the tool. http://eb2all.loria.fr/html_files/files/landingsystem.pdf http://eb2all.loria.fr/html_files/files/landingsystem.pdf