I have looked into the Isabelle tutorial which presents an example of it's use in verifying security protocol. However, it is a bit out of my understanding as I only know the basics. I'm looking for some examples which are not just simple theorems but practical applications using Isabelle/HOL. For example proving some algorithms or may be verifying properties system or some non-trivial mathematical theorem. Are such examples available anywhere ?
I have looked into the list of all applications provided in the isabelle official page but most of them are proofs of theorems.
I am also looking at an example of a file system verification using Alloy. It provides a proof where the properties of file/directories can be verified. I'm looking for something similar to it.
A few highly non-trivial examples I can think of right now are:
seL4, an entire operating system kernel written in C that was verified with Isabelle.
The AFP entry Jinja_Threads contains, as far as I know, a fully formalised bytecode compiler for a Java-like language with arrays and threads.
Jeremy Avigad's proof of the Prime Number Theorem.
The proof of Kepler's conjecture. A part of this was done in Isabelle; most of it, however, was done in the more ‘basic’ theorem prover HOL Light, whose logic is similar to Isabelle.
As Joachim mentioned, I am sure you can find more interesting applications in the AFP