Skip to content
@formal-land

Formal Land

Formal Verification for everyday-life applications
README.md

Formal Land

Welcome to the GitHub organization of Formal Land. Read about what we are doing on our Blog!

logo

Overview

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.

Projects

L1 of Tezos

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.

Rust Language

Developed coq-of-rust, a tool for verifying large Rust programs, funded by Aleph Zero.

EVM Verification

We're verifying the equivalence of Python EVM and Rust EVM implementations, leveraging coq-of-rust and coq-of-python.

Upcoming Projects

Stay tuned for announcements on our next formal verification project aimed at improving dApp security.

Get Involved

We welcome collaboration and inquiries. Contact us by email or on X to discuss how we can help verify your projects.

Popular repositories Loading

  1. rocq-of-rust rocq-of-rust Public

    Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.

    Rocq Prover 1.2k 43

  2. rocq-of-ocaml rocq-of-ocaml Public

    Formal verification for OCaml, with Rocq

    OCaml 275 22

  3. rocq-of-solidity rocq-of-solidity Public

    Forked from argotorg/solidity

    Formal verification for Solidity smart contracts with the theorem prover Rocq. Providing higher security in a time of smarter AIs.

    Rocq Prover 53 3

  4. rocq-of-python rocq-of-python Public

    Translate Python code to Rocq code for formal verification. Applied to the reference implementation of the Ethereum VM in Python (WIP, in pause)

    Rocq Prover 47 3

  5. garden garden Public

    Make your zero-knowledge circuits safe with formal verification. 🍀

    Rocq Prover 35 7

  6. coq-bonsai coq-bonsai Public

    🌳 Generate a fresh bonsai in your terminal

    Coq 34 1

Repositories

Showing 10 of 41 repositories
  • rocq-of-rust Public

    Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.

    formal-land/rocq-of-rust's past year of commit activity
    Rocq Prover 1,165 43 26 35 Updated Sep 23, 2026
  • ArkLib Public Forked from Verified-zkEVM/ArkLib

    Formally Verified Arguments of Knowledge in Lean

    formal-land/ArkLib's past year of commit activity
    Lean 0 Apache-2.0 113 0 1 Updated Sep 22, 2026
  • garden Public

    Make your zero-knowledge circuits safe with formal verification. 🍀

    formal-land/garden's past year of commit activity
    Rocq Prover 35 MIT 7 17 9 Updated Aug 24, 2026
  • ironwood Public Forked from zcash/ironwood

    Formal Verification of the Zcash Protocol and Documentation for the Ironwood Pool

    formal-land/ironwood's past year of commit activity
    Lean 1 19 0 1 Updated Jul 31, 2026
  • orchard Public Forked from zcash/orchard

    Implementation of the Zcash Orchard Protocol

    formal-land/orchard's past year of commit activity
    Rust 1 86 0 0 Updated Jul 28, 2026
  • halo2 Public Forked from zcash/halo2

    The Halo2 zero-knowledge proving system

    formal-land/halo2's past year of commit activity
    Rust 2 624 0 0 Updated Jul 28, 2026
  • formal.land Public

    Formal Land website

    formal-land/formal.land's past year of commit activity
    JavaScript 1 3 0 5 Updated Jul 14, 2026
  • CompPoly Public Forked from Verified-zkEVM/CompPoly

    A computable model of Polynomials in Lean.

    formal-land/CompPoly's past year of commit activity
    Lean 0 Apache-2.0 43 1 3 Updated Jun 20, 2026
  • lambdaworks Public Forked from lambdaclass/lambdaworks

    lambdaworks offers implementations for both SNARKs and STARKs provers, along with the flexibility to leverage their individual components for constructing customized SNARKs.

    formal-land/lambdaworks's past year of commit activity
    Rust 0 Apache-2.0 196 0 1 Updated May 26, 2026
  • rocq-of-solidity Public Forked from argotorg/solidity

    Formal verification for Solidity smart contracts with the theorem prover Rocq. Providing higher security in a time of smarter AIs.

    formal-land/rocq-of-solidity's past year of commit activity
    Rocq Prover 53 GPL-3.0 6,766 2 0 Updated May 24, 2026
View all repositories

People

This organization has no public members. You must be a member to see who’s a part of this organization.