ForSmart

ForSmart: Effective Formal Methods for Smart-Contract Certification

Project funded by the Vienna Science and Technology Fund

Duration: 2023-09-01 ‒ 2027-08-31 (ongoing)

Funding: € 799.850

Members

Project

Correctness and security of smart contracts is critical as digital assets may be at stake. To detect or evenis critical as digital assets may be at stake. To detect or even avoid such vulnerabilities in smart contracts, there have emerged bug-finding techniques, which lackin smart contracts, there have emerged bug-finding techniques, which lack soundness, and verification techniques, which lack precision.

In ForSmart, we aim to develop a hybrid, automated certification framework for smart contracts thatIn ForSmart, we aim to develop a hybrid, automated certification framework for smart contracts that symbiotically combines bug-finding in the form of test generation and verification in the form of sound staticin the form of test generation and verification in the form of sound static analysis, thereby achieving soundness and precision. Advanced automated-reasoning mechanisms, which we plan to develop and tailor to this domain, will support both testing and static analysis.to this domain, will support both testing and static analysis.

We will maximize the impact of ForSmart by applying our framework to concrete applications of academic,of academic, industrial, and public relevance, such as DeFi apps, with a focus on certifying functional and securitya focus on certifying functional and security properties, as well as by making our infrastructure available to contract developers, auditors, and users. Weas by making our infrastructure available to contract developers, auditors, and users. We additionally plan to leverage our ongoing collaborations with Certora, the Ethereum Foundation, ConsenSys, and Microsoft Research.

We request funding for 3 PhD students. The duration of each PhD will be 4 years – the funding will cover3 PhD students. The duration of each PhD will be 4 years the funding will cover 3.5 years, and the remaining time will be spent on internships at the aforementioned companies tothe aforementioned companies to encourage industrial adoption of our framework.our framework.

The core team of ForSmart (PIs) has a 2/3 female participation. We aim to maintain such a balance when(Pls) has a 2/3 female participation. We aim to maintain such a balance when expanding

Keywords: test generation, static analysis, automated reasoning, hybrid, certification, smart contracts

Results

  • Simon Jeanteur, Laura Kovács, Matteo Maffei, and Michael Rawson. “Automated Reasoning for Indistinguishability in the CCSA.” In Proceedings of the 33rd ACM Conference on Computer and Communications Security (CCS 2026). To appear. https://eprint.iacr.org/2026/1853
  • Arman Ferdowsi and Laura Kovács. “Certificate-Aware Property-Directed Reachability.” In Proceedings of the 26th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2026), pages 414-425, 2026. https://doi.org/10.34727/2026/ ISBN 978-3-85448-093-8_46
  • Amir Kafshdar Goharshady, Thomas Hader, Laura Kovács, and Harshit Jitendra Motwani. “Randomized Satisfiability Checking for Non-Linear Arithmetic over Finite Fields.” In Proceedings of the 26th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2026), pages 84-93, 2026. https://doi.org/10.34727/2026/ ISBN 978-3-85448-093-8_14
  • Robin Coutelier, Thomas Hader, and Laura Kovács. “Generalizing CDCL with Graph Backtracking.” In Proceedings of the 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026), LIPIcs, Volume 377, pages 14:1-14:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.SAT.2026.14
  • Laura Kovács. “SAT in Saturation: A Satisfied Match.” In Proceedings of the 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026), LIPIcs, Volume 377, pages 1:1-1:2. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.SAT.2026.1
  • Laura Kovács. “Saturation-Guided Inductive Synthesis.” In Proceedings of the 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026), LIPIcs, Volume 378, pages 2:1-2:3. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. https://doi.org/10.4230/LIPIcs.FSCD.2026.2
  • Ivana Bocevska, Takeshi Tsukada, Hiroshi Unno, Oded Padon, and Sharon Shoham. “Lagrangian-Based Duality for Quantified SMT Algorithms.” In Proceedings of the 38th International Conference on Computer Aided Verification (CAV 2026), LNCS, Volume 16683, pages 75-96, 2026. https://doi.org/10.1007/978-3-032-32526-6_4
  • Márton Hajdu, Petra Hozzová, Laura Kovács, Andrei Voronkov, Eva Maria Wagner, and Richard Steven Žilinčík. “Synthesis Benchmarks for Automated Reasoning.” In Proceedings of the 18th International Conference on Intelligent Computer Mathematics (CICM 2025), LNCS, Volume 16136, pages 21-28, 2025. https://doi.org/10.1007/978-3-032-07021-0_2
  • Clemens Eisenhofer, Theodor Seiser, Nikolaj Bjørner, and Laura Kovács. “On Solving String Equations via Powers and Parikh Images.” In Proceedings of the 34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2025), LNCS, Volume 15980, pages 120-138, 2025. https://doi.org/10.1007/978-3-032-06085-3_7
  • Clemens Eisenhofer, Michael Rawson, and Laura Kovács. “Finding Connections via Satisfiability Solving.” In Proceedings of the 34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2025), LNCS, Volume 15980, pages 82-102, 2025. https://doi.org/10.1007/978-3-032-06085-3_5
  • Michael Rawson, Clemens Eisenhofer, and Laura Kovács. “Constraint Learning for Non-confluent Proof Search.” In Proceedings of the 34th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2025), LNCS, Volume 15980, pages 103-119, 2025. https://doi.org/10.1007/978-3-032-06085-3_6
  • Christoph Hochrainer, Valentin Wüstholz, and Maria Christakis. “Arguzz: Testing zkVMs for Soundness and Completeness Bugs.” In Proceedings of the 35th USENIX Security Symposium (USENIX Security 2026), pages 1807-1826. USENIX Association, 2026. https://www.usenix.org/conference/usenixsecurity26/presentation/hochrainer
  • Markus Scherer, J. F. Blaabjerg, A. Sjösten, and Matteo Maffei. “Wanilla: Sound Noninterference Analysis for WebAssembly.” In Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security (CCS ’25), pages 126-140, 2025. https://doi.org/10.1145/3719027.3765156
  • Sophie Rain, Anja Petković Komel, Michael Rawson, and Laura Kovács. “Game Modeling of Blockchain Protocols.” In Proceedings of the 20th International Conference on Integrated Formal Methods (iFM 2025), LNCS, Volume 16194, pages 359-377, 2025. https://doi.org/10.1007/978-3-032-10794-7_18
  • Ivana Bocevska, Anja Petković Komel, Laura Kovács, Sophie Rain, and Michael Rawson. “Divide and Conquer: A Compositional Approach to Game-Theoretic Security.” Proceedings of the ACM on Programming Languages, Volume 9, Issue OOPSLA2, Article 342, pages 1949-1973, 2025. https://doi.org/10.1145/3763120
  • Christoph Hochrainer, Anastasia Isychev, Valentin Wüstholz and Maria Christakis. Fuzzing Processing Pipelines for Zero-Knowledge Circuits. In Proceedings of the 31st International Conference on Computer and Communications Security (CCS'25), 2025. ACM. To appear.
  • Márton Hajdú, Laura Kovács, and Andrei Voronkov. Partial Redundancy in Saturation. In 30th International Conference on Automated Deduction (CADE), pages 532-551, 2025
  • Márton Hajdú, Robin Coutelier, Laura Kovács, and Andrei Voronkov. Term Ordering Diagrams. In 30th International Conference on Automated Deduction (CADE), pages 552-569, 2025
  • Filip Bártek, Ahmed Bhayat, Robin Coutelier, Márton Hajdú, Matthias Hetzenberger, Petra Hozzová, Laura Kovács, Jakob Rath, Michael Rawson, Giles Reger, Martin Suda, Johannes Schoisswohl, and Andrei Voronkov. “The Vampire Diary”. In 37th International Conference on Computer Aided Verification (CAV), pages 57-71, 2025
  • Lorenzo Benetollo, Andreas Lackner, Matteo Maffei, Markus Scherer. Let’s Move2EVM. Usenix Security 2025, 1339-1355. https://www.usenix.org/conference/usenixsecurity25/presentation/benetollo
  • Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner and Laura Kovács. PolySat: Word-level Bit-vector Reasoning in Z3. In Proceedings of the 16th International Conference on Verified Software: Theories, Tools and Experiments (VSTTE), pages 47–69, 2024
  • Robin Coutelier, Laura Kovács, Michael Rawson, Jakob Rath, Armin Biere. “SAT Solving for Variants of First-order Subsumption”. Formal Methods in System Design, 2024.
  • Markus Scherer, Jeppe Fredsgaard Blaabjerg, Alexander Sjösten, Magdalena Solitro and Matteo Maffei, “Wappler: Sound Reachability Analysis for WebAssembly,” in 2024 IEEE 37th Computer Security Foundations Symposium (CSF), Enschede, Netherlands, 2024 pp. 249-264. https://www.computer.org/csdl/proceedings-article/csf/2024/620300a377/1W0eVUjUN2g
  • Robin Coutelier, Mathias Fleury, Laura Kovács: “Lazy Reimplication in Chronological Backtracking”. SAT 2024: 9:1-9:19. https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9
  • Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs (Extended). CoRR abs/2407.08455, 2024. https://arxiv.org/abs/2407.08455
  • Jana Chadt, Christoph Hochrainer, Valentin Wüstholz and Maria Christakis. Olympia: Fuzzer Benchmarking for Solidity. In Proceedings of the 39th International Conference on Automated Software Engineering (ASE'24), 2024. ACM. https://mariachris.github.io/publications.html
  • Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs. In Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP'24), 2024. Schloss Dagstuhl. https://mariachris.github.io/Pubs/ECOOP-2024.pdf
  • Johannes Schoisswohl, Laura Kovács, Konstantin Korovin. VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. LPAR 2024: 147-164
  • Pamina Georgiou, Márton Hajdú, Laura Kovács. Saturating Sorting without Sorts. LPAR 2024: 88-105. https://easychair.org/publications/paper/qbDc
  • Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovács, Michael Rawson. Scaling CheckMate for Game-Theoretic Security. LPAR 2024: 222-231. https://easychair.org/publications/paper/6ZDH
  • Márton Hajdú, Laura Kovács, Michael Rawson. Rewriting and Inductive Reasoning. LPAR 2024: 278-294. https://easychair.org/publications/paper/T1mjX
  • Simon Jeanteur, Laura Kovacs, Matteo Maffei and Michael Rawson, “CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model,” in 2024 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, 2024 pp. 3165-3183. https://doi.org/10.1109/SP54263.2024.00246
  • Clemens Eisenhofer, Laura Kovács, Michael Rawson. Embedding the Connection Calculus in Satisfiability Modulo Theories. AReCCa@TABLEAUX 2023: 54-63. https://ceur-ws.org/Vol-3613/AReCCa2023_paper4.pdf
  • Laura Kovács, Petra Hozzová, Marton Hajdu, Andrei Voronkov. Induction in Saturation. IJCAR 2024: 21-29. https://doi.org/10.1007/978-3-031-63498-7_2
  • Márton Hajdu, Laura Kovács, Michael Rawson, Andrei Voronkov. Reducibility Constraints in Superposition. IJCAR 2024: 115-132. https://doi.org/10.1007/978-3-031-63498-7_8
  • Petra Hozzová, Daneshvar Amrollahi, Márton Hajdu, Laura Kovács, Andrei Voronkov, Eva Maria Wagner. Synthesis of Recursive Programs in Saturation. IJCAR 2024: 154-171. https://doi.org/10.1007/978-3-031-63498-7_10
  • Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács. MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). IJCAR 2024: 386–395. https://doi.org/10.1007/978-3-031-63498-7_23