Federico Mora

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2025-163

August 15, 2025

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-163.pdf

Distributed systems are pervasive today, from cloud computing to Internet-of-Things (IoT) systems to connected automotive vehicles. However, building dependable distributed systems remains a challenging problem. While major strides have been made in formal methods for verifying distributed systems, successful users of formal methods must be both domain experts and experts in automated reasoning---a rare combination. In this dissertation, we address this challenge through a new automated reasoning stack that integrates artificial intelligence and formal methods at every layer.

The new automated reasoning stack consists of four key tools: Eudoxus, the P Verifier, Algaroba, and MedleySolver. Eudoxus is a neuro-symbolic tool that helps users generate formal models and specifications from informal artifacts. The P Verifier extends P, a formal modelling and specification language that developers are already using to test their distributed system designs, with support for formal verification and specification mining. To do this, the P Verifier generates satisfiability modulo theories (SMT) queries that Algaroba solves. Algaroba is currently one of the fastest SMT solvers in the world for the theory of quantifier-free algebraic data types. MedleySolver coordinates solvers, like Algaroba, to get better performance than any individual solver over realistic workloads, like those generated by the P Verifier.

We used our work to verify existing systems from related work and three new case studies; our industrial collaborators are actively using our work to verify their systems and classic protocols. Beyond these industrial applications, our stack represents the beginning of a broader vision for automated reasoning: one whose fundamental principle is that the full stack should be tailored to users’ needs rather than the other way around.

Advisors: Sanjit A. Seshia

---

BibTeX citation:

@phdthesis{Mora:EECS-2025-163,
    Author= {Mora, Federico},
    Title= {Scalable and Usable Domain-Specific Automated Reasoning},
    School= {EECS Department, University of California, Berkeley},
    Year= {2025},
    Month= {Aug},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-163.html},
    Number= {UCB/EECS-2025-163},
    Abstract= {Distributed systems are pervasive today, from cloud computing to Internet-of-Things (IoT) systems to connected automotive vehicles. However, building dependable distributed systems remains a challenging problem. While major strides have been made in formal methods for verifying distributed systems, successful users of formal methods must be both domain experts and experts in automated reasoning---a rare combination. In this dissertation, we address this challenge through a new automated reasoning stack that integrates artificial intelligence and formal methods at every layer.

The new automated reasoning stack consists of four key tools: Eudoxus, the P Verifier, Algaroba, and MedleySolver. Eudoxus is a neuro-symbolic tool that helps users generate formal models and specifications from informal artifacts. The P Verifier extends P, a formal modelling and specification language that developers are already using to test their distributed system designs, with support for formal verification and specification mining. To do this, the P Verifier generates satisfiability modulo theories (SMT) queries that Algaroba solves. Algaroba is currently one of the fastest SMT solvers in the world for the theory of quantifier-free algebraic data types. MedleySolver coordinates solvers, like Algaroba, to get better performance than any individual solver over realistic workloads, like those generated by the P Verifier.

We used our work to verify existing systems from related work and three new case studies; our industrial collaborators are actively using our work to verify their systems and classic protocols. Beyond these industrial applications, our stack represents the beginning of a broader vision for automated reasoning: one whose fundamental principle is that the full stack should be tailored to users’ needs rather than the other way around.},
}

EndNote citation:

%0 Thesis
%A Mora, Federico 
%T Scalable and Usable Domain-Specific Automated Reasoning
%I EECS Department, University of California, Berkeley
%D 2025
%8 August 15
%@ UCB/EECS-2025-163
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2025/EECS-2025-163.html
%F Mora:EECS-2025-163