# Automatically Strengthening Formal DeFi Specifications using Program Mutations with Chandra  Nandi

- Channel: [Ethereum Denver](https://streameth.org/ethereum-denver)
- Date: 2023-10-07
- Duration: 12:56
- Watch: https://streameth.org/watch/yt-d6WXU3p5Nbs
- YouTube: https://www.youtube.com/watch?v=d6WXU3p5Nbs

## Description

Formal verification is an effective technique for ensuring DeFi security. It assists humans in finding bugs before the code is deployed and can formally prove many program invariants. Formal verification is particularly relevant in the domain of smart contracts where vulnerabilities in the code can lead to severe financial losses. In this talk, we will show how a formal verification tool we have built, called the Certora Prover, can be used to prove high-level properties of Solidity smart contracts. The Certora Prover has already secured billions of dollars by verifying millions of lines of Solidity code.
 
One of the most important steps in formal verification is writing a good specification against which the program is verified. Writing good specifications can be challenging and may cause the results of formal verification to lead to false beliefs about software correctness. This talk will also present a new mutation-based tool, dubbed Gambit, for strengthening the quality of formal specifications and therefore gaining trust in the result of formal verification. We show cases where mutations can find missing parts of the specifications.

Chandra Nandi
Senior Researcher
Certora
Chandrakana recently graduated with a Ph.D. in Programming Languages and Software Engineering from the University of Washington. During her Ph.D., she focused on developing DSLs, compilers, and program synthesizers for computational geometry. She developed new, general-purpose term-rewriting-based techniques for synthesis and optimization that have found a variety of applications. Her work has won several awards including an Adobe Fellowship, a POPL Best Paper Award, and an OOPSLA Best Paper Award.
https://twitter.com/ChandrakanaNaN

Infrastructure + Scalability Stage