EVEREST
A high-level language for replicated state whose constructs are verified automatically.
Website: VUB research portal Funding: FWO Research Project Timeline: 2024–2027 PI: Elisa Gonzalez Boix
Distributed systems commonly replicate data to improve their availability, scalability, and fault tolerance, but keeping replicas consistent makes these systems considerably more complex. EVEREST (nearly full automatic verification for geo-replicated systems) develops a high-level language whose constructs can be verified automatically through transpilation to SMT, reducing the expertise and effort needed to build correct distributed abstractions for replicated state.