Skip to main content

🏁 Introduction

Here we present our project.


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:

programming flow

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 for an evaluation of your code and discuss what is possible to do.