A selfie I took in the desert

I work in the Trustworthy Systems Research Group of CSIRO, Australia's national science research agency. I use techniques from mathematical logic to help create trustworthy software and hardware that comes with strong security, safety and reliability guarantees.

I obtained my PhD in Mathematics at the University of Manchester in October 2019, under the supervision of Prof. Alexandre Borovik. My PhD thesis explored algebraic applications of Internal Set Theory, an axiomatic set theory developed by Edward Nelson as a foundation for Nonstandard Analysis. Highlights from my thesis include a powerful extension theorem for actions of LEF groups on compact manifolds, along with a "Robinsonian" characterization theorem for sheaves on topological spaces. Introducing a non-standard extension of Martin-Löf Type Theory allowed me to formally verify the main results of my thesis using the Agda interactive theorem prover. I also made some contributions to the theory of degrees of satisfiability in probabilistic group theory, and to the theory and practice of stochastic optimization in computer science. I have 16 refereed publications in international journals and conferences (listed in my CV). Click the buttons below to find out more about my research interests!

Mathematical Curiosities

Geometry of pseudo-random sequences

Pseudo-Randomness and Homology

Which one of these three point clouds can we get by sampling the unit cube using a pseudo-random sequence? Surprisingly, the answer is any one of them, depending on the sequence we use. We used three sequences to sample the same manifold: the unit cube, which has one connected component and no holes. However, the first two sequences fail to yield a uniform sample. In the first case (RANDU), the resulting point cloud seemingly consists of 15 separate connected components. In the second case (XorShift64, scaled), there is only one component, but it has many holes. Using persistent homology, one can rigorously define the Betti numbers of point samples, and investigate their relationship to the Betti numbers of the sampled manifold. In my honors thesis I classified some pseudorandom sequences based on their ability to reflect the topological properties of the manifolds they sample, and developed an algorithm that can test for failures of uniformity by calculating persistent homology groups of the samples..

Degree of Primality diagram for the number 45

Degree of Satisfiability

Which non-Abelian group is closest to being Abelian? Which composite number is farthest from being prime? Such questions can be formulated and answered using the theory of Degree of Satisfiability (and result in striking visual arrangements that feature heavily on this web page). The degree of satisfiability of a logical formula φ(x,y) is the probability that φ(a,b) holds for uniformly randomly chosen a,b. A famous theorem of Gustafson states that the degree of satisfiability of the equality xy=yx is at most 5/8 in a non-Abelian group, with equality obtained in the Quaternion Group. Hence, one can say that the Quaternion Group is closest to being Abelian among all the non-Abelian groups. The degree of satisfiability of equations in infinite groups gives significant information about algebraic structure, e.g. about virtual properties. I proved results about the degree of satisfiability of some special equations, and introduced criteria to identify which equations hold in a finite index subgroup precisely if they have positive degree of satisfiability.

PhD Thesis

My PhD thesis (available here) explores two novel algebraic applications of Internal Set Theory. I prove that every profinite group admits a finite approximation in the sense of Zilber, and my main result shows that well-behaved actions of the approximating group on a compact manifold give rise to similarly well-behaved actions of periodic subgroups of the approximated group on the same manifold. This generalizes earlier results of Manevitz and Weinberger on circle actions to a large class of groups. Motivated by the extraction of computational bounds from proofs in a pure fragment of IST, I devised a pure presentation of sheaves over topological spaces in the style of Robinson and proved it equivalent to the usual definition over standard objects. By introducing a non-standard extension of Martin-Löf Type Theory I formally verified my results using the Agda proof assistant.

News and Media

Diagram in a spined category

25 Oct 2021

My paper, Degree of satisfiability in Heyting algebras has hit the arXiv! (joint work w/ Ben Bumpus).

20 Oct 2021

A bunch of SMT-based tools I developed for a model-based security engineering project have been open-sourced, available from the CSIRO Data Access Portal (joint work w/ Ihor Kuz).

27 Aug 2021

Upcoming talk on combinatorics and spined categories at Category Theory 2021, 3 Sep 2021, Genoa, Italy. (Joint work, presented by Ben Bumpus).

28 Jul 2021

The recording of my Applied Category Theory 2021 talk is now available on YouTube.

20 Jun 2021

I will be giving a talk on Spined Categories at the Australian Category Seminar (Macquarie University) on 23 Jun 2021.

08 Jun 2021

I will be presenting Treewidth via Spined Categories, joint work with Ben Bumpus, at Applied Category Theory 2021 (Cambridge, UK, 12-16 July 2021).

21 May 2021

I received the CSIRO SCS Engineering and Technology Award, awarded for our high-impact work on binary verification for the 64-bit RISC-V architecture (along with my teammates Matthew Brecknell and Dr Mitchell Buckley).

06 May 2021

Click here to read the RISC-V International coverage of my work, bringing Translation Validation to RISC-V!

05 May 2021

Prof. Gernot Heiser's blog post on our seL4 verification work hit the front page of news aggregator news.ycombinator.com today!

05 May 2021

My work on Translation Validation of the seL4 kernel was featured on the HENSOLDT Cyber GmbH website. Read the full article, including my comments, in English🇦🇺 and German🇩🇪!

26 Apr 2021

I gave a talk about degree of satisfiability at the CSIRO Trustworthy Systems seminar, including announcing some results on degree of satisfiability in Heyting Algebras.

05 Apr 2021

Spined Categories: generalizing tree-width beyond graphs, joint work with Ben Bumpus, submitted to Combinatorica.

31 Mar 2021

Ben Bumpus presented our joint work on spined categories at the 37th British Colloquium for Theoretical Computer Science.

30 June 2020

I gave a talk about my type-theoretic analogue of Internal Set Theory at the Budapest Type Theory Seminar.

05 Feb 2020

My paper, Degree of satisfiability of some special equations hit the arXiv today!

01 Feb 2020

Conflict-free routing of multi-stop warehouse trucks, joint work with Sandy Brownlee and others, has appeared in the journal Optimization Letters.

23 Oct 2019

I relocated to Australia and joined the Trustworthy Systems Research Group of CSIRO!

14 Oct 2019

I successfully defended my PhD thesis, Development of Group Theory in the Language of Internal Set Theory.

07 Sep 2019

I gave an invited talk at LMS Prospects in Mathematics 2019, on applications of Nelson's proof-theoretic algorithm in topology.


Zoltan and bushcraft crew gathered around a sundial

I find the Big City and the Great Outdoors equally comfortable. On my day off, you're just as likely to meet me in the dense urban area of the Sydney CBD as in the coastal bushlands of New South Wales.

Zoltan and friends going up Kinder Scout

If you live in the UK, you may know me from Manchester Orators, a chartered club for the promotion of public speaking, presentation and leadership skills. I was a member between 2017 and 2019, and I hope to return one day.

Meal ingredients mise en place

At home, you'll find me in the kitchen. Fusion cuisine, simple ingredients, mise en place. Sometimes, something good comes out of it.

Salmon ceviche and other favorite dishes


If you have any questions, or if you wish to hire me as a consultant, use the email address below. You can also find me on the Mathematics Stack Exchange and on Semantic Scholar.

To find out my email address, enter the number ---- below: