Lelio Brun's homepage

Lelio Brun

Postdoctoral research scientist in Computer Science

National Institute of Informatics

Biography

I am a software developer at Braid Technologies in Tokyo.

Before that, I was a postdoctoral research scientist in the ZT-IoT project at NII in Tokyo.
I worked with Ichiro Hasuo and Taro Sekiyama on applying formal methods to ensure security of IoT (Internet of Things) systems.

I defended my PhD thesis in 2020, Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset, written under the supervision of Marc Pouzet and Timothy Bourke.

Interests

Functional programming
Synchronous languages
Proof assistants
Security protocols analysis

Education

PhD in Computer Science, 2020

École normale supérieure - PSL Research University
MSc in Computer Science (MPRI), 2016

Université Paris Cité
MSc in Aerospace Engineering, 2013

ISAE-ENSMA

Publications

Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation

2025 · Christophe Garion, Lélio Brun, Pierre-Loïc Garoche, Xavier Thirioux

Commun. ACM

Abstract

Model-based design tools are often used to design safety-critical embedded software. Consequently, generating correct code from such models is crucial. We tackle this challenge on Lustre, a dataflow synchronous language that embodies the concepts that base such tools. Instead of proving correct a whole code generator, we turn an existing compiler into a certifying compiler from Lustre to C, following a translation validation approach.
We propose a solution that generates both C code and an attached specification expressing a correctness result for the generated and optionally optimized code. The specification yields proof obligations that are discharged by external solvers through the Frama-C platform.

Cite

                @article{garion_equation-directed_2025,
	title = {Equation-{Directed} {Axiomatization} of {Lustre} {Semantics} to {Enable} {Optimized} {Code} {Validation}},
	volume = {69},
	issn = {0001-0782},
	url = {https://www.leliobrun.net/publication/cacm26/paper.pdf},
	doi = {10.1145/3747584},
	abstract = {Model-based design tools are often used to design safety-critical embedded software. Consequently, generating correct code from such models is crucial. We tackle this challenge on Lustre, a dataflow synchronous language that embodies the concepts that base such tools. Instead of proving correct a whole code generator, we turn an existing compiler into a certifying compiler from Lustre to C, following a translation validation approach.
We propose a solution that generates both C code and an attached specification expressing a correctness result for the generated and optionally optimized code. The specification yields proof obligations that are discharged by external solvers through the Frama-C platform.},
	number = {1},
	urldate = {2026-02-04},
	journal = {Communications of the ACM},
	author = {Garion, Christophe and Brun, Lélio and Garoche, Pierre-Loïc and Thirioux, Xavier},
	month = dec,
	year = {2025},
	pages = {93--101},
}

DOI

Automated Security Analysis for Real-World IoT Devices

2023 · Lelio Brun, Ichiro Hasuo, Yasushi Ono, Taro Sekiyama

HASP'23

Abstract

Automatic security protocol analysis is a fruitful research topic that demonstrates the application of formal methods to security analysis. Several endeavors in the last decades successfully verified security properties of large-scale network protocols like TLS, sometimes unveiling unknown vulnerabilities.

In this work, we show how to apply these techniques to the domain of IoT, where security is a critical aspect. While most existing security analyses for IoT tackle individually either protocols, firmware or applications, our goal is to treat IoT systems as a whole. We focus our work on a case study, the Armadillo-IoT G4 device, highlighting the specific challenges we must tackle to analyze the security of a typical IoT device. We propose a model using the Tamarin prover, that allows us to state certain key security properties about the device and to prove them automatically.

Cite

                @inproceedings{brun_automated_2023,
	address = {New York, NY, USA},
	series = {{HASP}'23},
	title = {Automated {Security} {Analysis} for {Real}-{World} {IoT} {Devices}},
	copyright = {All rights reserved},
	isbn = {979-8-4007-1623-2},
	url = {https://www.leliobrun.net/publication/hasp23/paper.pdf},
	doi = {10.1145/3623652.3623667},
	abstract = {Automatic security protocol analysis is a fruitful research topic that demonstrates the application of formal methods to security analysis. Several endeavors in the last decades successfully verified security properties of large-scale network protocols like TLS, sometimes unveiling unknown vulnerabilities. 

In this work, we show how to apply these techniques to the domain of IoT, where security is a critical aspect. While most existing security analyses for IoT tackle individually either protocols, firmware or applications, our goal is to treat IoT systems as a whole. We focus our work on a case study, the Armadillo-IoT G4 device, highlighting the specific challenges we must tackle to analyze the security of a typical IoT device. We propose a model using the Tamarin prover, that allows us to state certain key security properties about the device and to prove them automatically.},
	language = {en},
	booktitle = {Proceedings of the 12th {International} {Workshop} on {Hardware} and {Architectural} {Support} for {Security} and {Privacy}},
	publisher = {Association for Computing Machinery},
	author = {Brun, Lelio and Hasuo, Ichiro and Ono, Yasushi and Sekiyama, Taro},
	month = oct,
	year = {2023},
	pages = {29--37},
}

DOI Slides

Equation-Directed Axiomatization of Lustre Semantics to Enable Optimized Code Validation

2023 · Lélio Brun, Christophe Garion, Pierre-Loïc Garoche, Xavier Thirioux

EMSOFT'23 Best paper

Abstract

Model-based design tools like SCADE Suite and Simulink are often used to design safety-critical embedded software. Consequently, generating correct code from such models is crucial. We tackle this challenge on Lustre, a dataflow synchronous language that embodies the concepts that base such tools. Instead of proving correct a whole code generator, we turn an existing compiler into a certifying compiler from Lustre to C, following a translation validation approach.

We propose a solution that generates both C code and an attached specification expressing a correctness result for the generated and optionally optimized code. The specification yields proof obligations that are discharged by external solvers through the Frama-C platform.

Cite

                @article{brun_equation-directed_2023,
	series = {{EMSOFT}'23},
	title = {Equation-{Directed} {Axiomatization} of {Lustre} {Semantics} to {Enable} {Optimized} {Code} {Validation}},
	volume = {22},
	copyright = {All rights reserved},
	issn = {1539-9087},
	url = {https://www.leliobrun.net/publication/emsoft23/paper.pdf},
	doi = {10.1145/3609393},
	abstract = {Model-based design tools like SCADE Suite and Simulink are often used to design safety-critical embedded software. Consequently, generating correct code from such models is crucial. We tackle this challenge on Lustre, a dataflow synchronous language that embodies the concepts that base such tools. Instead of proving correct a whole code generator, we turn an existing compiler into a certifying compiler from Lustre to C, following a translation validation approach.

We propose a solution that generates both C code and an attached specification expressing a correctness result for the generated and optionally optimized code. The specification yields proof obligations that are discharged by external solvers through the Frama-C platform.},
	language = {en},
	number = {5s},
	journal = {ACM Transactions on Embedded Computing Systems},
	author = {Brun, Lélio and Garion, Christophe and Garoche, Pierre-Loïc and Thirioux, Xavier},
	month = sep,
	year = {2023},
	pages = {151:1--151:24},
}

DOI HAL Slides

Faites-vous confiance à votre thermostat ?

2022 · Lélio Brun

Interstices

Abstract

Certains systèmes logiciels qui interagissent avec le monde réel ne doivent échouer sous aucun prétexte, au risque de provoquer des catastrophes. Comment s’assurer que ces systèmes sont sûrs ? En particulier, quel degré de confiance accorder au processus de traduction de ces logiciels vers du code exécutable ?

Cite

                @article{brun_faites-vous_2022,
	title = {Faites-vous confiance à votre thermostat ?},
	copyright = {All rights reserved},
	url = {https://interstices.info/faites-vous-confiance-a-votre-thermostat/},
	abstract = {Certains systèmes logiciels qui interagissent avec le monde réel ne doivent échouer sous aucun prétexte, au risque de provoquer des catastrophes. Comment s’assurer que ces systèmes sont sûrs ? En particulier, quel degré de confiance accorder au processus de traduction de ces logiciels vers du code exécutable ?},
	language = {fr},
	journal = {Interstices},
	author = {Brun, Lélio},
	month = jun,
	year = {2022},
}

HAL

Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset

2020 · Lélio Brun

GDR GPL accessit prize

Abstract

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like Scade and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by dataflow synchronous languages like Lustre.

In this thesis we present Vélus, a Lustre compiler verified in the interactive theorem prover Coq. We develop semantic models for the various languages in the compilation chain, and build on the verified CompCert C compiler to generate executable code and give an end-to-end correctness proof. The main challenge is to show semantic preservation between the dataflow paradigm and the imperative paradigm, and to reason about byte-level representations of program states.

We treat, in particular, the modular reset construct, a primitive for resetting subsystems. This necessitates the design of suitable semantic models, compilation algorithms and corresponding correctness proofs. We introduce a novel intermediate language into the usual clock-directed modular compilation scheme of Lustre. This permits the implementation of compilation passes that generate better sequential code, and facilitates reasoning about the correctness of the successive transformations of the modular reset construct.

Cite

                @phdthesis{brun_mechanized_2020,
	type = {Doctoral {Thesis}},
	title = {Mechanized {Semantics} and {Verified} {Compilation} for a {Dataflow} {Synchronous} {Language} with {Reset}},
	copyright = {All rights reserved},
	url = {https://www.leliobrun.net/files/thesis.pdf},
	abstract = {Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like Scade and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by dataflow synchronous languages like Lustre.

In this thesis we present Vélus, a Lustre compiler verified in the interactive theorem prover Coq. We develop semantic models for the various languages in the compilation chain, and build on the verified CompCert C compiler to generate executable code and give an end-to-end correctness proof. The main challenge is to show semantic preservation between the dataflow paradigm and the imperative paradigm, and to reason about byte-level representations of program states.

We treat, in particular, the modular reset construct, a primitive for resetting subsystems. This necessitates the design of suitable semantic models, compilation algorithms and corresponding correctness proofs. We introduce a novel intermediate language into the usual clock-directed modular compilation scheme of Lustre. This permits the implementation of compilation passes that generate better sequential code, and facilitates reasoning about the correctness of the successive transformations of the modular reset construct.},
	language = {en},
	school = {École normale supérieure - PSL Research University},
	author = {Brun, Lélio},
	collaborator = {Pouzet, Marc and Bourke, Timothy},
	month = jul,
	year = {2020},
}

HAL Slides

Mechanized semantics and verified compilation for a dataflow synchronous language with reset

2020 · Timothy Bourke, Lélio Brun, Marc Pouzet

POPL'20

Abstract

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers to translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.

Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.

Cite

                @inproceedings{bourke_mechanized_2020,
	address = {New Orleans, LA, USA},
	series = {{POPL}'20},
	title = {Mechanized semantics and verified compilation for a dataflow synchronous language with reset},
	volume = {4},
	copyright = {All rights reserved},
	url = {https://www.leliobrun.net/publication/popl20/paper.pdf},
	doi = {10.1145/3371112},
	abstract = {Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers to translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.

Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.},
	language = {en},
	booktitle = {Proceedings of the 47th {ACM} {SIGPLAN} {Symposium} on {Principles} of {Programming} {Languages}},
	publisher = {ACM},
	author = {Bourke, Timothy and Brun, Lélio and Pouzet, Marc},
	month = jan,
	year = {2020},
	pages = {29},
}

DOI HAL Slides Video

Towards a Verified Lustre Compiler with Modular Reset

2018 · Timothy Bourke, Lélio Brun, Marc Pouzet

SCOPES'18

Abstract

This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal specification for the construct and sketch our plans to integrate it into the compiler and its correctness proof.

Cite

                @inproceedings{bourke_towards_2018,
	address = {Sankt Goar, Germany},
	series = {{SCOPES}'18},
	title = {Towards a {Verified} {Lustre} {Compiler} with {Modular} {Reset}},
	copyright = {All rights reserved},
	isbn = {978-1-4503-5780-7},
	url = {https://www.leliobrun.net/publication/scopes18/paper.pdf},
	doi = {10.1145/3207719.3207732},
	abstract = {This paper presents ongoing work to add a modular reset construct to a verified Lustre compiler. We present a novel formal specification for the construct and sketch our plans to integrate it into the compiler and its correctness proof.},
	language = {en},
	booktitle = {Proceedings of the 21st {International} {Workshop} on {Software} and {Compilers} for {Embedded} {Systems}},
	publisher = {ACM},
	author = {Bourke, Timothy and Brun, Lélio and Pouzet, Marc},
	month = may,
	year = {2018},
	pages = {14--17},
}

DOI HAL Slides

A Formally Verified Compiler for Lustre

2017 · Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, Lionel Rieg

PLDI'17

Abstract

The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.

We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimization that eliminates unnecessary conditional statements.

Cite

                @inproceedings{bourke_formally_2017,
	address = {Barcelona, Spain},
	series = {{PLDI}'17},
	title = {A {Formally} {Verified} {Compiler} for {Lustre}},
	copyright = {All rights reserved},
	isbn = {978-1-4503-4988-8},
	url = {https://www.leliobrun.net/publication/pldi17/paper.pdf},
	doi = {10.1145/3062341.3062358},
	abstract = {The correct compilation of block diagram languages like Lustre, Scade, and a discrete subset of Simulink is important since they are used to program critical embedded control software. We describe the specification and verification in an Interactive Theorem Prover of a compilation chain that treats the key aspects of Lustre: sampling, nodes, and delays. Building on CompCert, we show that repeated execution of the generated assembly code faithfully implements the dataflow semantics of source programs.

We resolve two key technical challenges. The first is the change from a synchronous dataflow semantics, where programs manipulate streams of values, to an imperative one, where computations manipulate memory sequentially. The second is the verified compilation of an imperative language with encapsulated state to C code where the state is realized by nested records. We also treat a standard control optimization that eliminates unnecessary conditional statements.},
	language = {en},
	booktitle = {Proceedings of the 38th {ACM} {SIGPLAN} {Conference} on {Programming} {Language} {Design} and {Implementation}},
	publisher = {ACM},
	author = {Bourke, Timothy and Brun, Lélio and Dagand, Pierre-Évariste and Leroy, Xavier and Pouzet, Marc and Rieg, Lionel},
	month = jun,
	year = {2017},
	pages = {586--601},
}

DOI HAL Slides Video

Projects

LustreC
A prototype compiler for Lustre, with verification abilities and certifying compilation in mind.
Vélus
A prototype compiler for Lustre, verified in Coq.
Obelisk
A tool to pretty-print (LaTeX) Menhir grammars.

Experience

Software engineer

Braid Technologies

Sep 2025 – Present
Backend programming in Rust, Python and C++.
Postdoctoral research scientist

NII · ZT-IoT project

Oct 2022 – Present
Formal methods for the security analysis of IoT systems.
Postdoctoral research scientist

ISAE-SUPAERO · IpSC Team (DISC)

Jan 2021 – Aug 2022
Adding translation validation features to the LustreC Lustre to C compiler through the Frama-C platform.
Postdoctoral research engineer

École normale supérieure / Inria · PARKAS Team

Jan 2020 – Dec 2020
Adding enumerations and case analysis support to the Vélus Lustre to Assembly compiler verified with the Coq Proof Assistant.
Software engineer

Astek

May 2014 – Aug 2014
Bug tracking and fixing in a large C++ codebase.

Teaching

Teaching assistant

2021/22

Computer science · ISAE-SUPAERO · 3^rd year undergraduate
Languages translation · ENSEEIHT · 3^rd year undergraduate
Functional programming · ENSEEIHT · 3^rd year undergraduate

2020/21–21/22

Transition systems - TLA+ · ENSEEIHT · 3^rd year undergraduate

2020/21

Automata and lexical analysis · Université Paris Cité · 2^nd year undergraduate
Databases · Université Paris Cité · 3^rd year undergraduate and 1^st graduate
Computer science concepts 2 · Université Paris Cité · 1^st year undergraduate
Programming basics 2 · Université Paris Cité · 1^st year undergraduate

2017/18

Computability, decidability · Sorbonne Université · 2^nd year undergraduate

2016/17–18/19

Programming languages and compilation · École normale supérieure · 3^rd year undergraduate

Academic service

ATVA'24 · artifact reviewer
CAV'24 · artifact reviewer
OOPSLA'23 · reviewer and artifact reviewer
JFLA'23 · Program Committee member
EMSOFT'20 · reviewer
EMSOFT'19 · WiP Committee
ECRTS'19 · artifact reviewer
EMSOFT'18 · reviewer
POPL'17 · student volunteer
PLDI'17 · student volunteer

Contact

lb@leliobrun.net

National Institute of Informatics
2 Chome-1-2 Hitotsubashi
101-8430 Chiyoda City
Tokyo, Japan

Lelio Brun

Postdoctoral research scientist in Computer Science

Biography

Interests

Education

Publications

Projects

Experience

Software engineer

Postdoctoral research scientist

Postdoctoral research scientist

Postdoctoral research engineer

Software engineer

Teaching

Teaching assistant

2021/22

2020/21–21/22

2020/21

2017/18

2016/17–18/19

Academic service

Contact