Selected Work
Things I've built
Explored Pulse, a verification framework built on F*, to formally verify a Raft heartbeat handler with memory and permission specs over byte arrays. Including also an extraction pipeline from F* to Rust via pulse2rust setup.
Implemented the full cryptographic stack from scratch during Erasmus at University of Tartu. OTP, ASN.1 DER, AES-CBC, RSA, ECDSA over P-256, X.509 certificate issuance, OCSP, and a minimal TLS 1.2 client. Pure Python without cryptographic libraries.
Built an abstract interpreter for a While+ language in TypeScript. Interval domain with threshold-based widening, narrowing, and backward boolean filtering via the HC4-revise propagation algorithm. Some edge cases are still open.
Implemented Raft consensus in Ada for a simulated seismic sensor network. The challenge was translating the paper's RPC model into actual network packets between independent server processes.
Desktop app to create charts uisng data sheet, with session save and restore using JSON files.
Mobile app for informed consent in private medical clinics. Flutter with clean architecture and BLoC. The interesting part was integrating graphometric digital signatures compliant with Italian advanced electronic signature regulations using Flutter channel and native code integration.
About
Who am I
Finishing an MSc in Computer Science at University of Padova, specializing in programming languages and formal methods. Before that, an Erasmus semester at the University of Tartu.
I work on things that are genuinely difficult to get right — verification, type systems, distributed consensus, cryptography. Not because it is required, but because the problems are interesting.
Looking for internship or thesis opportunities in software engineering or research engineering across Europe. Ideally somewhere the work is hard.