Martin Kleppmann from the University of Cambridge has given very nice introductory lectures about formal verification with Isabelle: the title is Correctness proofs of distributed systems with Isabelle, see these slides. Further information and video recordings are available from here:
- Strange Loop, St. Louis, USA, 14-Sep-2019
- Code Mesh LDN 19, London, UK, 08-Nov-2019
The lecture motivates the use of Isabelle by the very fitting characterization by Dominic Mulligan: Isabelle is the world’s most complicated video game.
Later in the talk there is a hands-on demo of the Isabelle Prover IDE, using the standard Isabelle/jEdit front-end: this is not a classic “REPL”, but a semantic document editor with immediate feedback by the prover.
Update (19-Dec-2019): An extended version of both talks is now available.