Hello seL4-devs,
I'm currently working on a CS MSc thesis at ETH Zurich supervised by David Cock, working on verified low-level system components using seL4 and CAmkES, which I'll be doing until August.
I haven't worked with seL4 or CAmkES before, but I have some rudimentary Isabelle/ITP experience from my BSc thesis (mainly typing sledgehammer ;) ).
During the course of my thesis I will probably have some questions which I'll post here, and hopefully I can contribute to improving the tooling around seL4+CAmkES verification.
Nice to meet you all!
Cheers,
Ben