Alessandro Bruni

About

I am Associate Professor in Computer Security at the IT-University of Copenhagen. My research focuses on formal methods, logics, protocol verification, and model checking — including formal verification of security protocols and machine learning systems.

Previously, I worked as a Postdoc in Carsten Schürmann’s group at ITU, on the Meta-CLF project. I obtained my Ph.D. at the Technical University of Denmark under supervision of Flemming Nielson and Hanne Riis Nielson, and did my B.Sc. and M.Sc. at the University of Padova, Italy under supervision of Paolo Baldan.

Current Research

My current work spans three main areas — see the Research section for details on each project.

Neurosymbolic AI. Formally verifying neural networks and differentiable logics using Rocq, with applications to network intrusion detection and autonomous driving controllers. One tool I use is the Vehicle language.

Verified Mathematical Foundations in Rocq. I am an active contributor to MathComp-Analysis, a Rocq formalization of mathematical analysis, where I develop the theory of probability including concentration inequalities and Lebesgue integration.

NLP for Interactive Theorem Proving. I am exploring the integration of large language models with the Rocq prover, including automated proof generation, proof translation, and learning environments.

Teaching

• Ethical Hacking, Spring 2021–2025
• Discrete Mathematics, Fall 2017–2025
• Advanced Security, Fall 2020–2022
• Security 2, Fall 2018, Spring 2019
• Security, Spring 2018
• Critical Systems, Fall 2016–2017
• Supervising Theses and Projects

Software

MathComp-Analysis — a Rocq/Coq formalization of mathematical analysis; I contribute a formalization of probability theory.

AIF-Omega — an abstraction-based verification tool for stateful security protocols.

CPNunf — an unfolder for contextual Petri nets.

Publications

Conference papers

1. Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa: Formalizing concentration inequalities in Rocq: infrastructure and automation. ITP 2025 PDF slides
2. Jairo Miguel Marulanda-Giraldo, Ekaterina Komendantskaya, Alessandro Bruni, Reynald Affeldt, Matteo Capucci, Enrico Marchioni: Our Ongoing Work: Quantifiers for Differentiable Logics in Rocq SAIV 2025 PDF
3. Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark: Taming Differentiable Logics with Coq Formalisation. ITP 2024 arXiv PDF
4. Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann: Robust Mean Estimation by All Means (Short Paper). ITP 2024 PDF
5. Alessandro Bruni, Eike Ritter, Carsten Scürmann: Skolemization for Intuitionistic Linear Logic. IJCAR 2024 arXiv
6. Karl Norrman, Vaishnavi Sundararajan, Alessandro Bruni: Extended Formal Analysis of the EDHOC Protocol in Tamarin. ICETE (Selected Papers) 2021 (published 2023)
7. Alessandro Bruni, Marco Carbone, Rosario Giustolisi, Sebastian Moedersheim, Carsten Schürmann: Security Protocols as Choreographies. Protocols, Strands, and Logic - Essays Dedicated to Joshua Guttman on the Occasion of his 66.66th Birthday
8. Ieva Daukantas, Alessandro Bruni, Carsten Schürmann: Trimming Data Sets: a Verified Algorithm for Robust Mean Estimation. PPDP 2021
9. Karl Norrman, Vaishnavi Sundararajan, Alessandro Bruni: Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices. SECRYPT 2021
10. Rosario Giustolisi, Alessandro Bruni: Privacy-Preserving Dispute Resolution in the Improved Bingo Voting. E-VOTE-ID 2020
11. Karl Norrman, Vaishnavi Sundararajan, Alessandro Bruni: Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices. CoRR abs/2007.11427 (2020)
12. Carsten Schürmann, Alessandro Bruni; Technical and Socio-Technical Attacks on the Danish Party Endorsement System. E-VOTE-ID 2019
13. Theis Grønbech Petersen, Thorvald Sahl Jørgensen, Alessandro Bruni and Carsten Schürmann; “Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC)”. Security Standardisation Research, Third International Conference, 2018 [Preprint]
14. Alessandro Bruni, Rosario Giustolisi, Carsten Schürmann; Automated Analysis of Accountability. 20th Information Security Conference (ISC), 2017 [Slides]
15. Eva Drewsen, Alessandro Bruni, Carsten Schürmann; Towards a Mechanized Proof of Selene Receipt-Freeness and Vote-Privacy. Second International Joint Conference on Electronic Voting, 2017 [Slides]
16. Peter Brottveit Bock, Alessandro Bruni, Agata Murawska and Carsten Schürmann: Representing Session Types. Dale Miller’s Festschrift, 2016
17. Michael Denzel, Alessandro Bruni and Mark Ryan. Smart-Guard: Defending User Input from Malware. The 13th IEEE International Conference on Advanced and Trusted Computing, 2016
18. Sebastian Mödersheim and Alessandro Bruni. AIF-ω: Set-Based Protocol Abstraction with Countable Families. Principles of Security and Trust, 2016 [Preprint]
19. Alessandro Bruni, Sebastian Mödersheim, Flemming Nielson and Hanne Riis Nielson. Set-pi: Set Membership Pi-calculus. Computer Security Foundations, 2015 [Extended version with corrections]
20. Alessandro Bruni, Michal Sojka, Flemming Nielson and Hanne Riis Nielson. Formal Security Analysis of the MaCAN Protocol. Integrated Formal Methods, 2014
21. Vigo, Roberto, Alessandro Bruni, and Ender Yüksel. Security Games for Cyber-Physical Systems. Secure IT Systems. Springer Berlin Heidelberg, 2013. 17-32.
22. Baldan, P., Bruni, A., Corradini, A., König, B., & Schwoon, S. On the computation of McMillan’s prefix for contextual nets and graph grammars. Graph Transformations, 2010. 91-106.

Journal papers

1. Baldan, P., Bruni, A., Corradini, A., König, B., Rodríguez, C., & Schwoon, S. Efficient unfolding of contextual Petri nets. Theoretical Computer Science, 2012.

Posters and Workshop Papers

1. Reynald Affeldt, Alessandro Bruni, Pierre Roux, Takafumi Saikawa: Yet another formal theory of probabilities in Coq. TYPES 2024 slides abstract
2. Alessandro Bruni, Sebastian Mödersheim, Flemming Nielson, Hanne Riis Nielson. Verification of Stateful Protocols, Set-based Abstractions in the Applied π-Calculus. Secure IT Systems, 2014.
3. Alessandro Bruni, Markulf Kohlweiss, Myrto Arapinis, Mark D. Ryan, Eike Ritter, Flemming Nielson, and Hanne Riis Nielson. “Proving Stateful Injective Agreement with Refinement Types”. Cryptoforma Workshop, 2015. [Paper]

Thesis

1. Alessandro Bruni. Analysis of Security Protocols in Embedded Systems. PhD thesis, DTU, 2016. [Link]

Popular media appearances (in Danish)

• Nyt EU-direktiv er godt nyt for vores cyberforsvar og for etiske hackere, 5. maj 2025
• Børnehave-hackeren endte i retten: Nu kræver eksperter klare rammer for “venlige hackere”, 12. november 2024
• Lektor: Hardwarebegrænsninger er ingen undskyldning for dårlig IoT-sikkerhed, 16. februar 2022
• IoT’s store udfordring: »Det er svært at sælge sikkerhed på bagkant«, 16. februar 2022
• Dark web er ikke kun for aktivister og kriminelle – DR Nyheder, 13. dec 2020
• Rodcertifikater udløber i år: Hardware i perfekt stand kan holde op med at virke – Version2, 28. februar 2020
• It-forsker skal styrke cybersikkerhed i Danmark – Altinget, 4. april 2019
• ITU-forsker bliver leder af OWASP i København – Version2, 27. marts 2019
• Slut med kringlede kodeord: Ny login-teknik kommer til Android – DR Nyheder, 4. mar 2019

Past events

• Sep 2025: Program Committee of PPDP 2025, University of Calabria, Rende, Italy
• Sep 2025: Presented “Formalizing concentration inequalities in Rocq: infrastructure and automation” at ITP 2025 PDF slides
• Attended PPL 2025 and presented our poster on “Developing Probability Theory Using the Lebesgue Integral in Rocq”
• Presented “Yet another formal theory of probabilities in Coq” at TYPES 2024
• Attended EuroProofNet workshop on “Alignment of Proof Systems and Machine Learning” in Vienna and presented our Types abstract
• Presenting “Responsible disclosure programmes” at the Cyber security summer school 2022
• Presenting “Security protocols as choreographies” at GuttmanFest 2022
• 5 May 2022: presenting at V2 security “There are no excuses for insecure IoT - Here’s why”
• 26-27 Nov 2018: Paper accepted at Standardization Security Research “Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC)”, with Theis Grønbech Petersen, Thorvald Sahl Jørgensen, and Carsten Schürmann
• 24-27 Oct 2017: Paper accepted at E-Vote-ID 2017 Towards a Mechanized Proof of Selene Receipt-Freeness and Vote-Privacy, with Eva Drewsen and Carsten Schürmann
• 3 Sep 2017: First International Workshop on Trends in Mechanized Security Proofs
• 7-8 Aug 2017: EASSS Summer school Presenting the analysis of security protocols in AIF-omega, with case studies in automotive
• 30 May 2017: Oresund Security Day ‘17, Resolution in linear logic, joint work with Eike Ritter and Carsten Schürmann
• 07 Sep. 2016: “Selene in Celf: Formalising Voting Protocols in Linear Logic”, Invited talk at the University of Luxembourg [Slides]
• 16 Sep. 2016: Presenting AIF-ω at Lamas Sing 2016, [Slides].
• 26 Apr. 2016: Giving a talk at MF#K, on F* and the verification of security protocols [Slides]
• Jan 2016: “AIF-ω: Set-Based Protocol Abstraction with Countable Families” accepted at POST-2016

Neurosymbolic AI

Overview

Neurosymbolic AI combines the pattern-recognition power of neural networks with the rigour of symbolic reasoning. My work in this area focuses on formally verifying correctness and robustness properties of neural networks and other machine learning systems using the Rocq proof assistant.

A central goal is to give machine learning systems the same level of trustworthiness that we expect from safety-critical software, by providing machine-checked proofs of their behaviour.

Differentiable Logics in Rocq

Differentiable logics are a family of logical frameworks that allow neural networks to be trained to satisfy logical specifications by differentiating through the logic. I am working on:

NLP for Interactive Theorem Proving

Overview

Large language models (LLMs) have shown surprising ability at natural language reasoning. Interactive theorem provers (ITPs) such as Rocq provide a rigorous setting where every reasoning step can be machine-checked. Combining the two opens a new frontier in automated mathematical reasoning.

I explore the integration of LLMs with ITPs, aiming to make proof development faster, more accessible, and eventually capable of tackling frontier mathematical problems.

Research Directions

Automated proof generation. Given a theorem statement in Rocq, can an LLM propose a valid proof? I study how to prompt, fine-tune, and evaluate models for this task, with a focus on proofs that are verified end-to-end by the Rocq kernel.

Verified Mathematical Foundations in Rocq

Overview

Rigorous mathematics requires that theorems be provably correct. Proof assistants such as Rocq make this literal: every step of a proof is mechanically verified by a computer. I contribute to MathComp-Analysis, a large-scale formalization of mathematical analysis built on the Mathematical Components library.

My focus is on probability theory — building machine-checked foundations for the mathematics that underpins statistics, machine learning, and information theory.

Probability Theory and Lebesgue Integration

Classical probability theory rests on measure theory and the Lebesgue integral. I formalize this infrastructure in Rocq, including: