I am a researcher in the formal verification team of the Argot Collective. My main research interests lie in automated theorem proving and type theory, and its applications to blockchain protocols.
| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Wed, 15 Oct 2025 10:10:31 GMT
access-control-allow-origin: *
etag: W/"68ef7317-8aeb"
expires: Mon, 29 Dec 2025 20:44:31 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 16FE:2BC55:948BC6:A6A7C8:6952E5D7
accept-ranges: bytes
age: 0
date: Mon, 29 Dec 2025 20:34:31 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210025-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767040472.726351,VS0,VE212
vary: Accept-Encoding
x-fastly-request-id: e1d88a84d44bed31c2408c7ff3ef7263698870ff
content-length: 9069
Anja Petković Komel
Anja Petković Komel
anja@argot.org
anjapetkovic
AnjaPetkovic
0000-0001-7203-6641
About me
Publications and talks
Peer-reviewed conferences and journals
Game Modeling of Blockchain Protocols
with Laura Kovács, Sophie Rain, and Michael Rawson
The 20th International Conference on Integrated Formal Methods (iFM 2025)
Divide and Conquer: a Compositional Approach to Game-Theoretic Security
with Ivana Bocevska, Laura Kovács, Sophie Rain, and Michael Rawson
ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2025)
Ground Truth: Checking Vampire Proofs via Satisfiability Modulo Theories
Andrei Voronkov, Michael Rawson, Anja Petković Komel and Johannes Schoisswohl.
The 30th International Conference on Automated Deduction (CADE-30)
Scaling CheckMate for Game-Theoretic Security
with Lea Brugger, Laura Kovács, Sophie Rain, and Michael Rawson
25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2024)
CheckMate: Automated Game-Theoretic Security Reasoning
with Lea Brugger, Laura Kovács, Sophie Rain, and Michael Rawson
2023 ACM SIGSAC Conference on Computer and Communications Security (CCS 2023)
Automating Security Analysis of Off-Chain Protocols
with Lea Brugger, Laura Kovács, Sophie Rain, and Michael Rawson
4th International Workshop on Formal Methods for Blockchains
An extensible equality checking algorithm for dependent type theories
with Andrej Bauer
Logical methods in computer science
Equality Checking for General Type Theories in Andromeda 2
with Andrej Bauer and Philipp G. Haselwarter
7th International Conference on Mathematical Software ICMS (2020)
Preprints
Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
Anja Petković Komel, Michael Rawson, Martin Suda,
Arxiv
International seminars (mostly peer-reviewed)
Towards verifying Vampire proofs in λΠ-calculus Modulo Theories
Anja Petković Komel, Michael Rawson, Martin Suda,
The 7th Vampire Workshop, 2023
The essence of elaboration
Anja Petković Komel,
Workshop on Syntax and Semantics of Type Thoery, Stockholm, 2022, invited talk
Equality checking for Finitary type theories
Andrej Bauer, Philipp G. Haselwarter, and Anja Petković
HoTTEST Conference 2020, invited talk
Cancelled On equality checking for general type theories: Implementation in Andromeda 2
Andrej Bauer, Philipp G. Haselwarter, Anja Petković
TYPES 2020
Employment
- July 2025 - ?: Formal Verification Researcher at Argot Collective.
- March 2025 - June 2025: Formal Verification Researcher at Ethereum Foundation.
- January 2022 - February 2025: Postdoctoral Researcher at Informatics department of TU Wien, Austria with Laura Kovács.
- July 2023 - August 2024: Career break: Maternity leave.
- October 2017 - December 2021: Researcher & PhD student & TA at Faculty of mathematics and physics, University of Ljubljana, Slovenia with Andrej Bauer.
Experience and service
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
- Oregon Programing Lanugages Summer School (OPLSS 2025), teaching.
- 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 June 2025 I gave an interview on my research for Slovenian national newspaper Delo: interview.
- In June 2025 I was guest on the special episode of the science show called Ugriznimo znanost (eng. "Bite the Science") on Slovenian national TV, speaking about mathematics, why people are afraid of it, and why they love it.
- In June 2025 I was awarded (together with Matej Petković and Uroš Kuzman) the award "Prometej znanosti za odličnost v komuniciranju znanosti" (eng. Prometheus of Scinece for excellent science commmunication) for the mathematical riddles on the science show called Ugriznimo znanost (eng. "Bite the Science") on Slovenian national TV (see below). Reports on the award: FMF report, MMC RTVSLO article.
- 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).
- 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.
Teaching
During the three years of my postdoc at TU Wien, I had the chance to teach the students. I was honoured to get to design and lecure the course on type theories, teaching students the basics of type theories as mathematical foundation, as well as formalizing mathematics and software correctness in a proof assistant.
During the four years of my PhD I had the chance to teach the students of mathematics and physics at University of Ljubljana. Besides the courses listed below I conducted a workshop on advanced uses of Mathematica. Prior to that I was a tutor and demonstrator for mathematics and analysis courses at Faculty for mathematics and physics, University of Ljubljana.
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.
In a similar fashion I thought the material at Oregon Programming Languages Summer School (OPLSS 2025), the materials and videos available here.
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.
Education
- 2017 - 2021: PhD from Faculty of mathematics and physics,
University of Ljubljana.
Thesis title: Meta-analysis of type theories with an application to the design of formal proofs
Thesis adviser: Andrej Bauer - 2015 - 2017: Master of Mathematics from Faculty of mathematics and physics, University of Ljubljana, graduated with honors.
Thesis title: Computing fixed points of monotone piecewise linear functions
Thesis adviser: Alex Simpson - 2012 - 2015: Bachelor of mathematics from Faculty of mathematics and physics, University of Ljubljana, graduated with honors.
Thesis title: Compactly dominated spaces are homotopy equivalent to compact spaces
Thesis adviser: Jaka Smrekar
My PhD thesis
Meta-analysis of type theories with an application to the design of formal proofs
I was a PhD student of Andrej Bauer at Faculty of mathematics and physics, University of Ljubljana. In my thesis, I analyze the meta-theory of type theory and its applications to proof assistants. I focus on two aspects: interactions of type theories via transformations and a general user-extensible equality checking algorithm.
One way of studying compatibility of type theories is by looking at their transformations. To accommodate for the use in proof assistants, the transformations we consider are syntactic in nature, they preserve derivability and are general enough to be applicable to a large class of type theories. The transformations preserve some syntactic structure (like judgement kinds and syntactic classes) and they interact nicely with substitutions of variables and instantiations of metavariables: with the action on expressions they form a relative monad for syntax.
A major use case for our definition of type-theoretic transformation is an elaboration. When designing a type theory, especially for using it in a proof assistant, one often faces a dilemma of how verbose the syntax should be. Terms annotated with full typing information are easily amenable to algorithmic processing and have good meta-theoretic properties. However, the syntax can quickly become too verbose to handle, so more economic terms that omit typing information are much more usable in practice. One can also omit other evidence, like proof of termination for recursive functions, or explicit universe levels. One common solution to this problem is to design two type theories: a fully annotated type theory S (the elaboration) that resides in the kernel of the proof assistant and an economic one T for the users input. The theories are connected via two maps: the retrogression transformation (r) that forgets the additional information, and the elaboration map (l) which uses a derivation to construct the missing data. We then prove two theorems: that elaboration is universal and that every finitary type theory has an elaboration. We also investigate some algorithmic properties of elaboration.
Proof assistants based on type theories have equality checking algorithms as their essential components. The algorithms free the users from proving mostly trivial judgemental equalities, and povide computation-by-normalization engines. Some systems, like Agda and Dedukti, allow the users to extend the built-in equality checkers. However, in a proof assistant that supports arbitrary user-definable type theories, like Andromeda 2, an equality checking algorithm highly depends on the given rules or may not even be available. Still, the proof assistant should provide support for equality checking that is easy to use and works well in the common, well-behaved cases. For this purpose we have developed a sound and extensible equality checking algorithm for user-definable type theories. We implemented it in the Andromeda 2 proof assistant.
An extensible equality checking algorithm for dependent type theories
with Andrej Bauer
Logical methods in computer science