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 super safe applications! ✈️ 🚀 ⚕️ 🏦

    Coq 897 31

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

    Formal verification for OCaml

    OCaml 257 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 34 3

  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 32 2

  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 18

Repositories

Showing 10 of 30 repositories
  • garden Public

    Make your zero-knowledge applications safe with formal verification! 🍀

    Coq 9 MIT 0 4 1 Updated Apr 23, 2025
  • coq-of-rust Public

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

    Coq 897 AGPL-3.0 31 24 25 Updated Apr 23, 2025
  • rocq-code-assistant Public

    Visual Studio Code extension for AI-assisted coding

    TypeScript 4 0 2 0 Updated Apr 23, 2025
  • 100-specification-smart-contracts Public

    💯 Full Specification Project for Smart Contracts

    Coq 5 MIT 1 0 0 Updated Apr 18, 2025
  • 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 32 GPL-3.0 6,595 0 0 Updated Apr 15, 2025
  • formal.land Public

    Formal Land website

    JavaScript 0 2 0 4 Updated Apr 14, 2025
  • revm Public Forked from bluealloy/revm

    Rust implementation of the Ethereum Virtual Machine.

    Rust 0 MIT 695 0 1 Updated Feb 25, 2025
  • zirgen Public Forked from risc0/zirgen

    Zirgen compiler and RISC Zero circuits

    C++ 0 Apache-2.0 20 0 0 Updated Feb 10, 2025
  • rocq-of-noir Public Forked from noir-lang/noir

    Formal verification tool for Noir programs using the Rocq system

    Rust 7 Apache-2.0 274 0 2 Updated Jan 18, 2025
  • execution-specs Public Forked from ethereum/execution-specs

    Specification for the Execution Layer. Tracking network upgrades.

    Python 0 CC0-1.0 323 0 1 Updated Dec 30, 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…