CVL: Separating Formal Specifications from Code

I will describe a simple declarative language CVL for describing the intended behavior of software and its applications to formally specify the intended behavior of Decentralized Financial Applications (DeFI). CVL allows specifying invariants on reachable states of the program, API restrictions, and relational properties comparing two programs. The language is designed to make specifications reusable across different code versions and different DeFi protocols.

Certora provides an SaaS which implements two complementary techniques for detecting bugs before the code is deployed and proving their absence:

1) Formally verify that all behaviors of the code meet the specifications.

2) Iteratively search for paths in the code that violates the specifications.

Both of these techniques are implemented in the Certora prover and check that the low-level bytecode correctly implements the CVL specifications.

Mooly Sagiv is a professor and chair of Computer Sciences at Tel Aviv University and a CEO and co-founder of Certora. He is a leading researcher in the area of large-scale (inter-procedural) program analysis and one of the key contributors to shape analysis. His fields of interest include programming languages, compilers, abstract interpretation, profiling, pointer analysis, shape analysis, inter-procedural dataflow analysis, program slicing, and language-based programming environments. Sagiv is a recipient of a 2013 senior ERC research grant for Verifying and Synthesizing Software Composition and a member of Academia Europa. He is a recipient of the Friedrich Wilhelm Bessel Research Award (2002). He is an ACM fellow and a recipient of the Microsoft Research Outstanding Collaborator Award 2016 for contributions to automatic formal verification.