Introduction

Here we present our project.

Technology

We formally verify programs by automatically translating the source code to the Rocq proof system. We then prove arbitrarily complex properties, either automatically or manually. We plug into continuous integration systems to make sure proofs are kept up-to-date with the code.

Our public references today are strongest in blockchain and financial infrastructure, including work around Tezos. The underlying approach is more general: translate source code, prove selected properties in Rocq, and keep those proofs aligned with the implementation as it evolves.

Besides the layers of type-checking and testing, we propose to add formal verification as a final layer of security for software development:

Our proposal

Our proposal is to formally verify critical parts of existing projects. We support code written in Rust, Python, or OCaml languages. This is especially relevant for infrastructure software, critical libraries, and embedded or systems components where testing alone leaves too much uncertainty.

Get started

Contact us at contact@formal.land for an evaluation of your code and discuss what is possible to do.