Engineering & verification
Selected work
A closer look at the problems I've worked on, my contributions, and the context behind them.
Certora · Formal Verification Researcher
Proving protocol correctness
- The problem
- Financial protocols need precise statements of how assets, accounting, and liquidations should behave. Those properties must hold across more than the examples covered by individual tests.
- My contribution
- At Certora, I analyse protocols and write formal verification specifications using the Certora Prover. My work includes expressing properties on solvency, liquidation, rounding and others as specifications that can be checked against the implementation.
- Outcome & context
- This work guarantees protocol behaviour against explicit and checkable properties.
BlockInvest · Web3 Software Engineer
Engineering tokenised financial assets
- The problem
- Issuing financial assets on a blockchain requires token infrastructure and payment settlement to work together, alongside the systems used by participating institutions.
- My contribution
- At BlockInvest, I contributed to the platform for tokenising financial assets on Polygon and to the launch of CDP’s digital bond. My work included integrating TIPS Hash-Link for payment settlement, maintaining internal platforms, and coordinating with technical teams at European financial institutions.
- Outcome & context
- The project connected tokenised asset infrastructure with payment settlement, leading to the creation of the first fully tokenized bond in Italy.
Independent · Open source
GasBad: measuring Solidity gas costs
- The problem
- Choosing a Solidity library involves tradeoffs. Gas costs vary by operation and implementation, so comparisons need a shared benchmark setup.
- My contribution
- I created GasBad to compare common Solidity libraries using Forge. The published methodology specifies compiler and optimisation settings and reports results by contract and operation.
- Outcome & context
- The source code and benchmark tables are public, so developers can inspect and reproduce the comparisons.