Over the last decade I've worked across compiler engineering, audio/music software, functional programming and blockchain; today I work on building static analysis tools for Solidity smart contracts using C++ and MLIR.
I have a PhD in Computer Science from Imperial College London, where I focused on programming languages and formal methods (mostly static analysis and abstract interpretation).
I've worked remotely for most of my career and am comfortable collaborating in distributed, async-first teams across time zones.
Outside of software, I'm an electronic music producer and artist.
For more details, please also see my LinkedIn profile or download my CV.
I'm currently employed as a Senior R&D Engineer at Veridise where I develop static analysis tools for Solidity smart contracts using C++ & MLIR.
Lately I've been working a lot with LLM tools and trying to understand their effectiveness and limitations in the context of the specific projects I'm involved.
Here's a selection of cool project I did work on in the past. For a more complete list plese see my LinkedIn and repos on GitHub.
🎧 Music technology
Developer
2020-2024
Since 2020, I contributed to the development of the Loopcloud desktop app and its companion audio plugin (which syncs the app to the user's DAW for a more integrated experience).
I delivered several new major features (such as collections, MIDI support and an onboarding interactive tutorial), and an extensive UI rework, in addition to countless bug fixes and workflow improvements.
Lead developer
2021-2022
TATAT is a MIDI plugin designed for 3 main purposes: to create always-changing sequences, to quickly sketch and store music ideas, to add unexpected events to fixed patterns.
Author
2020-Present
A Max4Live device I built for helping me quickly come up with lead patterns when writing trance. It started as a 2020 lockdown project but it's still receiving updates!
Available here!
Field recording, sound analysis/design/editing
2009-2010
Since 2020, I contributed to the development of the Loopcloud desktop app and its companion audio plugin (which syncs the app to the user's DAW for a more integrated experience).
I delivered several new major features (such as collections, MIDI support and an onboarding interactive tutorial), and an extensive UI rework, in addition to countless bug fixes and workflow improvements.
💻 Compilers & formal methods
Developer
2018
According to its official docs,
"K is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations and rules"
I loved using K as the foundational framework for my research work as a PhD student,
and I was privileged, a couple of years later, to be able to contribute
back to its community (as well as practicing some Haskell!)
Developer
2018
IELE is an improvement on the Ethereum blockchain virtual machine. It was created after the KEVM project demonstrated that a K formal specification of EVM could automatically generate a VM comparable in performance to hand-crafted implementations.
I helped developing the Solidity to IELE compiler.
😎 Misc
Clojure Developer (full-stack)
2019 - 2020
Helped developing Yapster - a messaging app for the workplace; contributing new features across both frontend and backend as well as bug-fixes (Clojure/ClojureScript).
I really enjoyed learning and working with the Clojure programming language!
Lead Developer
2016 - 2017
Lead the development of DIMMAND, a cross-platform digital solution for detecting literacy difficulties & strengths in children.
Internship
2009 - 2008
Implemented syntax highlighting in the ne text editor.
🧸 Toy projects
Author
2025-Present
As I've been learning Rust during the last couple of months, I decided to get some practice by building this fun little project that converts image files to ASCII art.
One of the goals was also to familiarize with functional programming techniques in Rust
(e.g. I didn't use any for loop to iterate through the image pixels, but relied on iterators facilities; also tried not to use mutable variables)
Check out the README!
I hold a PhD in Computing from Imperial College London, where I worked in the field of programming language theory and formal methods.
My thesis was about the formalisation of the PHP programming language and the development of a static analysis tool derived from the formal semamtics (see below).
Here are the main research projects and publications I worked on during the years.
🔬 Research Projects
Lead Developer / PhD Student
2018
KPHP is a formal specification of the PHP programming language written in the K-Framework, together with a prototype bug finding tool based on the theory of abstract interpretation and derived directly from the formal semantics.
Developer / PhD Student
2018
JSCert is a mechanised specification of JavaScript, written in the Coq proof assistant. JSRef is a reference interpreter for JavaScript in OCaml, which has been proved correct with respect to JSCert and tested with the Test 262 test suite.
📄 Publications
- IELE: A Rigorously Designed Language and Tool Ecosystem for the Blockchain with T. Kasampalis, D. Guth, B. Moore, T. Serbanuta, V. Serbanuta, G. Rosu and Ralph Johnson - International Symposium on Formal Methods 2019.
- A Digital App to Aid Detection, Monitoring, and Management of Dyslexia in Young Children (DIMMAND): Protocol for a Digital Health and Education Solution with MR Sood, A. Toornstra, M. Sereno, M. Boland, A. Sood - 2018
- An Executable Formal Semantics of PHP with Applications to Program Analysis. PhD Thesis, Imperial College London, 2016.
-
An Executable Formal Semantics for PHP - with S. Maffeis - ECOOP 2014.
-
A Trusted Mechanised JavaScript Specification - with M. Bodin, A. Chargueraud, P. Gardner, S.Maffeis, D. Naudziuniene, A. Schmitt, G. Smith - POPL 2014.
- Building bricks with bricks, with Mathematica - with P. Codara, O. D'Antona - Mathematica Italian User Group Meeting 2011.
