VALE (Verified Assembly for Everest)

A tool for constructing formally verified high-performance assembly language code, with an emphasis on cryptographic code.

Source

It uses existing verification frameworks, such as Dafny and F*, for formal verification. It supports multiple architectures, such as x86, x64, and ARM, and multiple platforms, such as Windows, Mac, and Linux. Additional architectures and platforms can be supported with no changes to the Vale tool.

Part of the Everest project, which aims to build and deploy a verified HTTPS stack.

Tags: language   native   assembly  

Last modified 06 April 2022