I’m a software engineer and computer scientist, with a PhD in Computer Science from Imperial College London, and a background spanning audio systems, programming languages, and blockchain technologies.
I currently work in web3 security and formal methods, focusing on the development of static analysis tools for Solidity smart contracts.
Earlier in my career, I also specialized in audio programming and music technology (C++/JUCE, Matlab, Max/MSP) and remain active as an electronic music artist. I also enjoy functional programming and have hands-on experience in Haskell and Clojure among others.
- 🧑💻 stuff I'm working on
- 📚 stuff I'm learning
- 🎧 past projects (audio / music technology)
- 🖥️ past projects (formal methods etc.)
- 🧪 research & publications
For more details, please also see my LinkedIn profile.
I'm currently employed as a Senior R&D Engineer at Veridise where I help develop static analysis tools for discovering vulnerabilities in Solidity smart contracts.
Co-author & Lead developer
2024-Present
An audio FX plugin designed in collaboration with an acclaimed trance producer. It should be the first of a series of releases.
More info soon 🔥
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.
Developer
2016-2017
I had the privilege of working at SSL headquarters in Oxford.
During my employment there I helped develop and maintain the software powering Solid State Logic’s high-end digital consoles in both the Broadcast (System T) and Live (L200, L350 etc.) product families (C#).
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!
Author
2018
A bunch of free audio plugins I wrote while learning JUCE.
- a nice drum synth
- a simple waveshaper
- stereo width utility
- a [bitcrusher][https://github.com/dfilaretti/bitcrusher-demo-2]
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.
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.
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.
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.
- 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.
