Formal tooling for Algorand’s smart contract architecture
Building formal semantics of both L1 and L2 languages for Algorand’s smart contract architecture in the K framework
Recent Projects
Modeling and Verification of Gasper
Modeling Gasper and verifying its properties using the Coq proof assistant
An executable model of the Beacon Chain protocol
An executable K model of Ethereum 2.0 Beacon Chain Phase 0 specification
Verification of Algorand’s Safety Property
Modeling of the Algorand Consensus Protocol in the Coq proof assistant and verifying its safety guarantees
Statistical Model Checking of RANDAO Against Attacks
Statistical model checking of RANDAO’s resilience against pre-computed reveal sstrategies
Resource-bounded Intruders in Denial of Service Attacks
A formal resource-bounded-intruders model for a wide range of denial of service attacks
Modeling and Verification Distance Fraud Attacks
Statistical model checking of distance fraud attacks on the Hancke-Kuhn family of protocols