Zoltan, a non-standard analyst by training, working on the correctness proof seL4-based OS code.
More contact information is available at the Contact page.