Aymeric Fromherz, an architect of software trust

Like an architect, Aymeric Fromherz, an ISFP (Inria Starting Faculty Position) researcher since 2022 in the PROSECCO project team, examines the mathematical foundations of the digital world, ensuring that every line of code is based on unshakeable foundations. What is his chosen field? Formal verification, a rigorous approach that he applies to various types of programmes. From securing cryptographic exchanges to improving the reliability of operating systems and even unravelling the mysteries of tax law, Aymeric strives to build ever more robust and trustworthy systems.

His career path, punctuated by successes, was not written in stone. After spending his high school years in Lyon, he turned to mathematics, entering ENS-PSL in Paris after two years of scientific preparatory classes. However, after completing a joint honours degree, he was then enticed by the potential and creative capacity offered by computer science.

Aymeric’s initial experiences led him to signal processing over graphs during an internship in Lyon, but it was a period of immersion in the business world at Prove&Run, a company specialising in formally verified operating systems with an industrial focus, which led to the emergence of his vocation for formal verification. The idea of mathematically modelling programs to prove their accuracy and reliability became a guiding principle.

Eager to explore beyond French horizons, Aymeric flew to the United States, where he completed his thesis at Carnegie Mellon University. For Aymeric, research is a constant source of stimulation, a unique opportunity to interact with like-minded people, where nothing is taken for granted.

In research, new things are always happening. You can never cover absolutely everything. It's a form of permanent stimulation. It's also a unique opportunity to interact with like-minded people.

During his time at Microsoft Research, he discovered just how crucial it is to establish links between fundamental research and concrete industrial applications: 

I was impressed by this team, which brought together people with brilliant but accessible minds. We were encouraged to exchange ideas with researchers from Microsoft Research, who are true experts in their field (...) I also appreciated the balance between research and practical applications. Keeping one foot in the real world, solving application problems and sometimes industrial problems, while doing research, is hugely important to me.

On his return to France, he joined the PROSECCO project team as a post-doc in October 2021, becoming an ISFP researcher in 2022, where he continues to look for ways to improve software security and reliability. Aymeric ensures that his work does not remain confined to laboratories, but also resonates outside their walls. His aim is to extend the application of formal verification techniques to a wide range of domains and systems.

In a world in which software governs our lives, from banking systems to secure communications, the reliability of computer code is a crucial issue. This is where formal verification comes into play, a field at the intersection of mathematics and computer science, which sets out to ensure that programs function as expected with no flaws or ambiguities. This is an extremely important property for embedded systems, aeronautical systems and nuclear power stations, for example.

Creating mathematical models of a program's behaviour to demonstrate that it is free from critical errors is Aymeric's field of study. One of the key challenges of this discipline is “functional correctness”, which in addition to ensuring that a programme does not crash, also ensures that it “does what it is supposed to do”. In cryptography, for example, this involves checking that the implementation of an algorithm, which is often complex, corresponds perfectly to its mathematical specification. 

Formal verification does not stop there, however. Aymeric and his colleagues apply these techniques to operating systems and especially to memory management mechanisms (storage allocation). Recently, they have also applied them to a more surprising field: tax law implementations. 

Their activities have highlighted ambiguities in the interpretation of date calculations in legal texts, with significant implications for administrative and judicial decisions. This earned them recognition at the ESOP conference in April 2024, where they received a Best Tool Paper Award for their paper entitled “Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law”. This is a concrete example of the impact that these methods can have on society, going far beyond the small world of software development.

Date-based calculations are frequently used in the implementation of legal systems, to determine the eligibility of citizens for social benefits, for example. However, these calculations are not always clearly defined: if we add one month to 31 March, will the result give a date of 30^th April or 1^st May? Existing implementations of date calculations rarely have a clearly defined and specified behaviour for this type of case. To solve this problem, we have defined semantics for date arithmetic that enable the formalisation of the expected behaviour.

Behind the scenes in the PROSECCO project team, research is progressing at the pace required for in-depth reflection, where the rigour of formal verification is combined with concrete technological challenges. The focus here is on securing IT systems and languages well before their roll-out. These activities include the Rust programming language. The team is seeking to understand its fundamental principles and intrinsic behaviour before examining the implications in terms of software reasoning. “This language has many positive aspects in terms of software security, but it also requires a new understanding of programs written in Rust compared with those written in C,” explains Aymeric.

But PROSECCO's involvement does not stop there. Cryptography is also a fundamental pillar of the team's research, particularly with the advent of post-quantum cryptography. “If a quantum computer exists one day, certain aspects of modern cryptography will no longer be secure and will become obsolete. So, it's important to protect against these things upstream,” adds Aymeric, “hence the development of new ‘post-quantum’ cryptographic constructions”. The aim is therefore to anticipate these upheavals by developing solutions capable of withstanding the threats posed by these new machines.

And then comes the challenge of tax law verification, as explained above. Through this project, the team is applying its methods of formalisation and mathematical proof to legislation, in order to support public decision-makers. “The idea is to provide lawyers and legislators with tools to prevent ambiguities and inconsistencies in the interpretation of laws,” explains Aymeric. 

This research is part of AVoCat, an exploratory action of which Aymeric is scientific co-leader with Raphael Monat (SYCOMORES project-team from the University of Lille Inria Centre). AVoCat focuses on the automatic verification of programs written in Catala, a new programming language designed to be understandable for legal experts and to conform to the structure of legislative texts in order to transform the law into code. 

If he had to recommend a book to students interested in his field of research, Aymeric would choose Mechanizing Proof: Computing, Risk, and Trust by Donald MacKenzie (MIT Press, 2001). This essay in the sociology of science traces the history of the formal verification of programmes and highlights an interesting fact: the major questions driving the field today were already being asked 40 or 50 years ago. “I consider this to be a pretty important book, if only to obtain an overview of the field and understand how it has evolved, and in particular how AI was envisaged as a mathematical reasoning tool from the 1960s onwards. It provides an insight into the contributions, limitations and areas of application of formal verification,” concludes Aymeric.