I am a researcher in the formal verification team of the Ethereum Foundation. My main research interests lie in automated theorem proving, its applications to blockchain protocols, type theory, its applications to proof assistants, and logic.

Preprints

International seminars (mostly peer-reviewed)

Software

CheckMate is a framework designed to automatically check security properties of games that arise from off-chain (blockchain) protocols. The framework yields a strategy (if it exists) for the following properties: weak immunity, collusion resilience and practicality.

Andromeda is an implementation of (standard) finitary type theories, allowing the user to define their own type theory. It is based on an ML style meta-language that supports proof development via runners and bidirectional evaluation. It implements a user-extensible equality checkig algorithm.

Community service

• Women in EuroProofNet 2025, organizing committee.
• WiL 2025, programme committee.
• HoTT/UF 2025, programme committee.
• TACAS 2025, artefact evaluation committee.
• Cost action: CA20111 European Research Network on Formal Proofs, management committee, gender balance coordinator.
• CPP 2023, programme committee, Best Reviewer Award.
• HoTT/UF 2023, organizing committee, programme committee, local organiser.
• Women in EuroProofNet 2023, organizing committee.
• Womencourage 2023, poster evaluation committee.
• ICFP 2022, organizing committee, virtualization chair.
• HoTT/UF 2022, organizing committee.
• Women in EuroProofNet 2022, organizing committee.
• Women in Mathematics on Mediterranean Shores, Bled, Slovenia, September 2019, organizing committee.

Outreach to society and media

I believe the mission of scientists is not only discovering new science, but also communicating science and science-related issues to others, from fellow scientists to the general public. In May 2025 I participated in a podcast about Cryptocurrencies and Financial literacy, organized by Slovenian national radio station Val 202 (audio). In the years 2022 and 2023 I helped organise workshops for school children at TU Wien, to help them learn the concept of algorithm in a playful way. In October 2022 I gave a talk about gender balance in computer science for students at ENS Paris-Scalay (slides). In June 2022 I participated at a round table about the profession of a scientist, organized by Slovenian national radio station Val 202 (audio). From September 2019 to January 2022 I posed mathematical riddles at the science show Ugriznimo znanost on Slovenian national television RTVSLO. In March 2020 I gave an interview for Metina Lista science podcasts (audio) and in November 2019 an interview at the occasion of 100. anniversary of University of Ljubljana on Slovenian national radio station Val 202 (audio). In December 2018 I co-organised a round table called Women in Science and Technology (video.) with the collegues from Jožef Stefan Institute.

Introduction to type theories (Faculty of Informatics, TU Wien)

I had the honour to present type theories to students of informatics and mathematics at TU Wien. The purpose of this course was to familiarize the students with the concept of a type theory, the most commonly used type theories in practice and how we use type theories in proof assistants. The course fosuced on the mathematical foundation, the type theories and it comprised of the following topics:

• Martin-Löf type theory (MLTT) - where we described the most common dependent types and ingredients of type theories.
• Agda (proof assistant based on MLTT) - where we got to know how to use MLTT to formalize proofs.
• Calculus of inductive constructions (CIC) - where we described the differences and nuances between different type theories.
• Coq (proof assistant based on CIC) - where we gdt to know how to use CIC to formalize proofs in the most commonly used proof assistant.
• Meta-theory of type theories - where we formally defined a type theory and related it to first-order and other higher-order theories.

Formal methods in infromatics (Faculty of Informatics, TU Wien)

I was a TA for master students of informatics.

• In autumn 2023, I marked students' exams.
• In spring 2023, I marked students' exams.
• In autumn 2022, I marked students' exams.
• In spring 2012, I marked students' exams.

Logic and sets (Faculty of Mathematics and Physics, University of Ljubljana)

I was a TA for first year undergraduate mathematics students taking a course on foundations of mathematics: first-order logic and set theory.

• In autumn 2020, I was a TA for one group and I marked students' exams.
• In autumn 2019, I was a TA for one group and I marked students' exams.
• In autumn 2018, I was a TA for one group and I marked students' exams.
• In autumn 2017, I was a TA for one group and I marked students' exams.

Introduction to programming (Faculty of Mathematics and Physics, University of Ljubljana)

I was a TA for first year undergraduate mathematics and financial mathematics students, givng them an introducotry course on programming in python.

• In spring 2021, I was a TA for one group and I marked students' exams.
• In spring 2020, I was a TA for one group and I marked students' projects.
• In spring 2019, I was a TA for one group and I marked students' exams.

Teaching mathematics and physics in English (Faculty of Mathematics and Physics, University of Ljubljana)

I was a TA for master students in pedagogical mathematics and pedagogical physics. We discussed different approaches to teaching mathematics in English and covered vocabulary for various highschool level topics.

• In spring 2021, I was a TA for the course I marked students' coursework.