Ongoing Research Projects

• Projects funded by Ethereum Foundation

  • GREY (A Greedy algorithm for Yul to EVM)
    • Elvira Albert
  • FORYU (FORmal semantics for YUL in Coq)
    • Elvira Albert
  • ZK‑ARCKIT
    • Albert Rubio

• Spanish Projects

  • LIAISON (LogIc-based technologies boosted by AI for Security and OptimizatioN) [Spanish Ministry of Science, Innovation and Universities, PID2024-157044OB-C31] (January 1, 2025 - December 31, 2027)
    • Elvira Albert
    • Albert Rubio
  • DESAFIO-CM (DESArrollo Formal de sistemas y servicios beneficiosos para la sOciedad) [funded by the Community of Madrid, TEC-2024/COM-235] (January 1, 2025 - December 31, 2028)
    • Elvira Albert
    • Manuel Nuñez (COORDINATOR, Complutense University of Madrid)

Past Projects

• Projects funded by Ethereum Foundation

  • Circom 2.0 Language and Compiler. (Oct 2019 - Dec 2020), funded by iden3 and Ethereum Foundation
    • Albert Rubio
  • GASOL
    • Elvira Albert
  • GREEN (GREEdy optimizatioN of EVM bytecode)
    • Elvira Albert
  • SOPA (SOund and yet Precise Gas Analysis of EVM Bytecode)
    • Elvira Albert
  • FORVES (FORmally VErified block optimizationS)
    • Elvira Albert
  • FORVES 2.0 (FORmally VErified EVM optimizationS -- leveraging FORVES to inter-block optimizations)
    • Elvira Albert

• Projects funded by other private companies

  • Circom 2.0 Compiler Development and Deployments (Feb 2021 - Aug 2021), funded by iden3
    • Albert Rubio
  • Extending and Improving the Circom Language and its Compiler (Nov 2021 - May 2024), funded by iden3
    • Albert Rubio
  • Enhancing Security within the Circom Compiler (Feb 2023 - Jun 2023), funded by 0xPARC
    • Albert Rubio
  • Security, Expressiveness and Standardization in the Circom Compiler (Jun 2024 - Jun 2025), funded by Polygon
    • Albert Rubio

• European Projects

  • ENVISAGE (Oct 1, 2013 - Sept 31, 2016) [FP7 610582]
    • Elvira Albert (Complutense University of Madrid)
    • Einar Broch Johnsen (COORDINATOR, University of Oslo)
  • SUPRA (Jan 1, 2012 - Dec 31, 2013) [Deutsch & Spanish Sc Research Councils, Acciones Integradas Hispano-Alemanas]
    • Elvira Albert (Complutense University of Madrid)
    • Andrey Rybalchenko (Technical Univesity of Munich)
  • HATS (March 1, 2009 - February 28, 2013) [EU IST FET Program. Integrated Project #231620] "Highly Adaptable and Trustworthy Software using Formal Methods"
    • German Puebla (Technical University of Madrid)
    • Reiner Hähnle (Technische Universität Darmstadt)
  • MOBIUS (Mobility Usability Security), code IST-15905.
  • ASAP (November 1, 2002 - January 31, 2006) [EU IST FET Program Project Number IST-2001-38059] "Advanced Specialization and Analysis for Pervasive Systems" In collaboration with the Universities of Bristol (UK), Roskilde (Denmark), and Southampton (UK).
  • CoLogNet (1 Jan 2002 - 31 June 2005) [EU IST FET Network of Excellence IST-2001-33123] "The EU Network of Excellence in Computational Logic"
  • AMOS (1 March 2002 - 31 May 2004) [EU IST Program Project Number IST-2001-34717] "Automated Matching of Open Source code" (Localización automática de código abierto) In collaboration with CONECTA (Italy).

• Spanish Projects

  • VIVAC (Jan 1, 2013 - Dec 31, 2015) [Spanish Ministry of Science and Innovation TIN2012-38137-C02]
    • Elvira Albert (Complutense University of Madrid)
    • German Puebla (Technical University of Madrid)
  • DOVES (Development Of Verifiable and Efficient Software)(January 1, 2009 - December 31, 2013), project code TIN-2008-05624.
  • PROMETIDOS-CM (PROgrama en MÉtodos para el Desarrollo de Software Fiable, de Alta Calidad y Seguro)(Jan. 2010 - Dec. 2013) , project code S-0505/TIC/0407.
  • MERIT (MÉtodos RIgurosos para sistemas software heTerogéneos y móviles), project code TIN-2005-09207.