IMDEA Software Institute

Syntheos is a tool for checking the realizability of LTL specifications with theories that supports referencing previous variable values.

Hoare Type Theory

Partial Commutative Monoids

Prototype implementation of SwiftPaxos (NSDI 2024)

A Runtime Verification Engine

L2 Optimistic rollups fraud proofs mechanization

Implementation of the paper "Modular Sumcheck Proofs with Applications to Machine Learning and Image Processing"

A Byzantine-fault tolerant distributed grow-only set equipped with synchronization barriers.

A Rust library for the Lunar universal zkSNARK