Zoltan, a non-standard analyst by training, works on the correctness proof for the seL4 kernel.
More contact information is available at the Contact page.
