👥 Who we are

• team of 5
• formal verification/audit specialists
• leading project: verification of Tezos 💫

🎯 What we propose

Formal verification of Solidity programs.

❓ Why

• a lot of value stored in smart contracts
• millions of $ stolen at a time 💰
• hard to test all the cases 🌌

⚙️ Technology

• Proof engine Coq 🐓
• Specifications and proofs in Coq ✒️
• Translation to Coq with our tool coq-of-solidity

🥇 Positioning

We do theorem proving, the highest level of code certification
(picture from Runtime Verification)

🚀 How we proceed

1. Translation of the Solidity code to Coq
2. Specifications in Coq
3. Proofs that specifications are always valid ✅

We offer ✅ 🛍️

• Detected bugs (even when extensive testing) 🧨
• Detected potential vulnerabilities 🕳️
• A cleaner code 🪒

🏁 To start

• send us an email contact@formal.land ✉️

Thanks!

🌲 Formal Land

Formal verification for everyday-life programs

🏇