In this presentation, I will give a very brief introduction to interactive formal verification of programming languages.
I will then proceed with an overview of three projects that we are working on or contributing to in our CoBRA institute.
- ConCert, a framework for smart contract verification. As part of this we have developed a general backend to the Coq proof assistant which allows us to generate provably correct functional rust programs.
- hacspec, a subset of rust for the specification of high assurance cryptography.
- fiat-crypto, a verified compiler which allows one to generate efficient, provably correct, constant time and platform independent implementations of cryptographic primitives.
Finally, I will shortly reflect on the status of formal verification in these subsets of rust.
YOU MAY ALSO LIKE:
- Introduction to Rust (Online Course on 8th - 15th December 2021)
- Embedded Rust: Beginners Workshop (Online Course on 9th December 2021)
- Functional Programming in 40 Minutes (SkillsCast recorded in November 2021)
- How to end-to-end encrypt all application layer communication - with Ockam (SkillsCast recorded in October 2021)
Formal Verification of Subsets of the Rust Language
Associate professor Computer Science at Aarhus University. He leads the formal verification and smart contract parts of the CoBRA research center. His research focuses on type theory and formal verification, especially in the context of blockchains. This includes programming languages and high assurance cryptography.