Skip to content
@formal-land

Formal Land

Formal Verification for Web3
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. coq-of-rust coq-of-rust Public

    Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

    Coq 439 17

  2. coq-of-ocaml coq-of-ocaml Public

    Formal verification for OCaml

    OCaml 255 20

  3. coq-of-python coq-of-python Public

    Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.

    Coq 30

  4. coq-of-solidity coq-of-solidity Public

    Forked from ethereum/solidity

    Formal verification for Solidity smart contracts with Coq 🐓 Verify arbitrary properties on your smart contracts and make no bugs!

    Coq 25 1

  5. coq-bonsai coq-bonsai Public

    🌳 Generate a fresh bonsai in your terminal

    Coq 24

  6. coq-of-ts coq-of-ts Public

    Formal verification for TypeScript

    TypeScript 14

Repositories

Showing 10 of 25 repositories
  • circom Public Forked from iden3/circom

    zkSnark circuit compiler

    formal-land/circom’s past year of commit activity
    WebAssembly 1 GPL-3.0 279 0 1 Updated Dec 22, 2024
  • formal.land Public

    Formal Land website

    formal-land/formal.land’s past year of commit activity
    JavaScript 0 2 0 3 Updated Dec 20, 2024
  • coq-of-rust Public

    Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

    formal-land/coq-of-rust’s past year of commit activity
    Coq 439 AGPL-3.0 17 15 20 Updated Dec 20, 2024
  • coq-of-solidity Public Forked from ethereum/solidity

    Formal verification for Solidity smart contracts with Coq 🐓 Verify arbitrary properties on your smart contracts and make no bugs!

    formal-land/coq-of-solidity’s past year of commit activity
    Coq 25 GPL-3.0 6,374 0 0 Updated Dec 12, 2024
  • coq-evm Public Forked from formalize/coq-evm

    Hash functions used in EVM implemented in Coq.

    formal-land/coq-evm’s past year of commit activity
    Coq 0 Apache-2.0 1 0 1 Updated Dec 11, 2024
  • coq-of-noir Public Forked from noir-lang/noir

    A formal verification tool for Noir programs

    formal-land/coq-of-noir’s past year of commit activity
    Rust 4 Apache-2.0 225 0 2 Updated Dec 10, 2024
  • execution-specs Public Forked from ethereum/execution-specs

    Specification for the Execution Layer. Tracking network upgrades.

    formal-land/execution-specs’s past year of commit activity
    Python 0 CC0-1.0 285 0 1 Updated Dec 10, 2024
  • sp1 Public Forked from succinctlabs/sp1

    The fastest, most feature-complete zkVM for developers.

    formal-land/sp1’s past year of commit activity
    Rust 0 Apache-2.0 380 0 0 Updated Nov 18, 2024
  • shared-documentation Public

    Shared documentation for the developments

    formal-land/shared-documentation’s past year of commit activity
    0 MIT 0 0 0 Updated Oct 23, 2024
  • coq-of-python Public

    Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.

    formal-land/coq-of-python’s past year of commit activity
    Coq 30 MIT 0 12 2 Updated Sep 10, 2024
View all repositories

People

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

Top languages

Loading…

Most used topics

Loading…