Welcome to the COSTA website

The COSTA research group develops formal techniques and models for program optimization and verification, along with related implementation technologies.Our current application domain is the blockchain ecosystem, where we develop new formal methods for the verification and optimization of Solidity smart contracts, and advance zero‑knowledge proof technologies through the generation, analysis and optimization of arithmetic circuits.

Our research focuses on three main lines of work:

• Development of the circom compiler and analysis of arithmetic circuits

  We are the development team behind the circom compiler for building arithmetic circuits, a language widely adopted by thousands of users in the context of Zero-Knowledge Protocols. We have also developed CIVER, a tool that verifies whether these circuits are underconstrained. We currently work on ZK-ARCKIT, a project funded by the Ethereum Foundation that aims to provide tools to analyze, transform, and optimize the polynomial constraint systems generated for building zero-knowledge proofs.

  News!: CIVER has helped the ZisK development team find two soundness bugs in the recursion circuits! See the details here.

• Analysis and Optimization of Smart Contracts

  We investigate new techniques to analyze and optimize smart contracts (decentralized applications that run on blockchain platforms). In this area, we have developed several tools: EthIR, a decompiler for EVM bytecode, GASTAP, a gas-consumption analyzer for smart contracts; and GASOL and SuperStack, two superoptimizers of EVM bytecode that rely on an SMT-solver and a SAT-solver, respectively. These tools have been partially funded by the GASOL, GREEN, and SOPA projects, granted by the Ethereum Foundation. Currently, we are working on the GREY project, a new approach to EVM code generation.

• Formally Verified Compilers

  In this research line, our goal is to formally verify the correctness of optimization and static analysis tools using proof assistants like Rocq (formerly known as Coq). We have carried out several projects in this area, supported by the Ethereum Foundation: in the FORVES and FORVES 2.0 projects, we developed a formally verified checker to certify the correctness of EVM (Ethereum Virtual Machine) block optimizations; currently, in the FORYU project, we are developing a formal semantics for Yul, the intermediate language of the Solidity compiler.

Contact

Elvira Albert
Departamento de Sistemas Informáticos y Programación
Facultad de Informática,
C/ Profesor José García Santesmases, s/n
Complutense University of Madrid
E-28040 - Madrid (Spain)