🏁 Introduction

Here we present our project.

Technology

We formally verify programs by automatically translating the source code to the Coq 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 technology is used by the crypto-currency Tezos to formally verify its implementation. We believe Tezos to be the first crypto-currency with a process of formal verification of its implementation, making it one the safest decentralized platform. See the Coq Tezos of OCaml project for the current status.

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.

Get started

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