🏁 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 projects written in the OCaml programming language. We focus on easy-to-catch bugs or safety critical properties. We configure our tools to make the translation to Coq works. We communicate with your teams to formally verify important properties. We maintain the Coq proofs to make sure there are no regressions. We can train the developers so that they can interact with the proofs.

The higher your requirements are, the more you need us.

Get started

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