Certora · Formal Verification Researcher
Proving protocol correctness
Formal specifications for blockchain protocols, covering properties such as solvency, fair liquidation, and rounding safety.
Formal Verification Researcher at Certora
Emanuele Civini — Formal verification & blockchain engineering.
I work on the correctness of blockchain protocols, from implementation to formal specifications. My research explores automated reasoning, SMT solving, and knowledge compilation.
Selected work
View workBlockInvest · Web3 Software Engineer
Engineering tokenised financial assets
Blockchain infrastructure for financial assets, including work on CDP’s digital bond and the integration of TIPS HashLink for settlement.
Independent · Open source
GasBad: measuring Solidity gas costs
A reproducible comparison of gas consumption across OpenZeppelin, Solady, and Solmate implementations.
From implementation to specification
Problems I work on
- Protocol correctness
- Expressing formal properties of a system that can be checked against code.
- Blockchain engineering
- Building smart contracts and the infrastructure around them.
- Automated reasoning
- Researching SMT solving and knowledge compilation.
Research & publications
Work on automated reasoning and knowledge compilation with collaborators at the University of Trento.
IJCAR 2026 · Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT
The paper introduces scalable, theory-agnostic methods to eagerly enumerate all necessary SMT theory lemmas to better handle complex tasks such as unsat-core extraction and MaxSMT. Authors: Emanuele Civini, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani.
SAT 2026 · d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries
The paper extends knowledge compilation to SMT by combining formulas with precomputed theory lemmas so they can be compiled into d-DNNF and efficiently queried at the propositional level in polytime. Authors: Gabriele Masina, Emanuele Civini, Massimo Michelutti, Giuseppe Spallitta, Roberto Sebastiani.
Latest writing
View all posts →Let's talk
Interested in similar questions?
I enjoy exchanging ideas about formal verification, blockchain systems, and automated reasoning. If any of my work resonates with you, feel free to get in touch.
hi@emanuelecivini.com