Welcome to the GitHub organization of Formal Land. Read about what we are doing on our Blog!
Formal Land is dedicated to enhancing security and reliability through advanced formal verification techniques. We specialize in verifying blockchain implementations, smart contracts, and systems software to ensure they meet the highest standards of correctness.
We achieved a milestone by formally verifying over 100,000 lines of OCaml code for Tezos' layer 1, including its storage system and smart contracts VM.
Developed coq-of-rust, a tool for verifying large Rust programs, funded by Aleph Zero.
We're verifying the equivalence of Python EVM and Rust EVM implementations, leveraging coq-of-rust and coq-of-python.
Stay tuned for announcements on our next formal verification project aimed at improving dApp security.
We welcome collaboration and inquiries. Contact us by email or on X to discuss how we can help verify your projects.