Hello! My name is Fernando Leal, known in the internet as ayhon!

I am a computer scientist interested in programming languages, software verification ant theorem provers. In general, I am likely to enjoy any topic in the intersection of Computer Science and Mathematics.

In 2024 I finished my Computer Science and Mathematics Double Bachelor at UCM in Madrid, Spain. That same year I started my masters in Research in Computer Science at ENS Paris-Saclay.

During my first year of my masters, I had an internship in Inria's Prosecco team under the supervision of Aymeric Fromherz and Son Ho, where I worked with Aeneas to verify a SHA3 implementation in Lean. Some additional autocomes of this internship were the initial step* tactic implementation for Aeneas and an executable Lean SHA3 specification.

During my second year of my masters, I had an interenship in ETH's Programming Language Foundations lab under the supervision of Ralf Jung and Max Vistrup, where I worked on the Iris-Lean project by porting the programming language interface and developing Wander, a Lean native Iris automation tactic.

For the end of 2026, I will collaborate with Jonathan Protzenko's team as part of the Google Student Researcher Program, where I will contribute to existing projects (Kraken, Aeneas) as a Lean metaprogrammer.