Forgetting variables in d4v2 model counter circuits
Expanding the d4v2 BC-S1.2 circuit format to specify projected variables
I'm a Formal Verification Researcher interested in automated reasoning, formal verification and distributed applications.

Freelance, then full time since February 2024
Contributed to BlockInvest, a SaaS platform for tokenizing financial assets on the Polygon blockchain. Played a key role in launching the first fully tokenized bond with Cassa Depositi e Prestiti Spa, integrating ECB's TIPS HashLink for instant payments. Enabled the automatic transfer and management of โฌ25 million. Managed and optimized AWS infrastructure, cutting costs by ~50% without affecting performance. Maintained internal platforms and coordinated with technical teams across European financial institutions.

Full time
Led the design, development of blockchain products for the holoride ecosystem, with a focus on the RIDE utility token. Set up the RIDE bridge from MultiversX to Ethereum and integrated it into the RIDE Dapp. Developed and deployed smart contracts for staking and farming.
Expanding the d4v2 BC-S1.2 circuit format to specify projected variables
Implementation of the Schnorr identification protocol over Curve25519 in Rust.
Comparing gas efficiency of the most common Solidity libraries