Description
Formal Land specializes in code audits using formal verification to ensure code is free of vulnerabilities, with a primary focus on the Web3 space. Their services include smart contract audits for Solidity, Rust code verification for critical applications like blockchains, and zero-knowledge system audits. They have worked with prominent organizations such as the Ethereum Foundation, Tezos Foundation, Aleph Zero Foundation, and Sui Foundation. The company develops and utilizes its own automated translation tools (like coq-of-rust and coq-of-solidity) to convert various programming languages into the Rocq proof system, enabling source-level verification. They are committed to open source, making their tools and code publicly available on GitHub.