Skip to content
Change the repository type filter

All

    Repositories list

    • Formal Land website
      JavaScript
      3104Updated Feb 23, 2026Feb 23, 2026
    • Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.
      Rocq Prover
      401.1k2829Updated Feb 16, 2026Feb 16, 2026
    • 💯 Full Specification Project for Smart Contracts
      Rocq Prover
      2700Updated Feb 8, 2026Feb 8, 2026
    • Formal verification for Solidity smart contracts with the theorem prover Rocq. Ensure no vulnerabilities for your smart contracts.
      Rocq Prover
      6.1k4800Updated Jan 5, 2026Jan 5, 2026
    • garden

      Public
      Make your zero-knowledge circuits safe with formal verification! 🍀
      Rocq Prover
      532176Updated Nov 27, 2025Nov 27, 2025
    • oxidefier

      Public
      Port your Soldity smart contracts to Rust, with ease and 💯 equivalence
      Rust
      0431Updated Nov 20, 2025Nov 20, 2025
    • pico

      Public
      Rust
      48001Updated Oct 26, 2025Oct 26, 2025
    • Plonky3

      Public
      A toolkit for polynomial IOPs (PIOPs)
      Rust
      388001Updated Oct 16, 2025Oct 16, 2025
    • openvm

      Public
      A performant and modular zkVM framework built for customization and extensibility.
      Rust
      94201Updated Aug 27, 2025Aug 27, 2025
    • llzk-lib

      Public
      Library for parsing, generating, and analyzing LLZK code.
      C++
      9001Updated Aug 20, 2025Aug 20, 2025
    • go-corset

      Public
      A port of the Corset tool into Go.
      Go
      10101Updated Jul 2, 2025Jul 2, 2025
    • Formal verification tool for Noir programs using the Rocq system
      Rust
      3731012Updated May 28, 2025May 28, 2025
    • Visual Studio Code extension for AI-assisted coding
      TypeScript
      1620Updated May 2, 2025May 2, 2025
    • revm

      Public
      Rust implementation of the Ethereum Virtual Machine.
      Rust
      971001Updated Feb 25, 2025Feb 25, 2025
    • zirgen

      Public
      Zirgen compiler and RISC Zero circuits
      C++
      27000Updated Feb 10, 2025Feb 10, 2025
    • Specification for the Execution Layer. Tracking network upgrades.
      Python
      424001Updated Dec 30, 2024Dec 30, 2024
    • circom

      Public
      zkSnark circuit compiler
      WebAssembly
      356101Updated Dec 22, 2024Dec 22, 2024
    • coq-evm

      Public
      Hash functions used in EVM implemented in Coq.
      Coq
      1001Updated Dec 11, 2024Dec 11, 2024
    • sp1

      Public
      The fastest, most feature-complete zkVM for developers.
      Rust
      615000Updated Nov 18, 2024Nov 18, 2024
    • Shared documentation for the developments
      1100Updated Oct 23, 2024Oct 23, 2024
    • Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.
      Coq
      542122Updated Sep 10, 2024Sep 10, 2024
    • move-sui

      Public
      Rust
      23000Updated Sep 6, 2024Sep 6, 2024
    • Formal verification for OCaml
      OCaml
      20272513Updated Aug 5, 2024Aug 5, 2024
    • .github

      Public
      1100Updated Jun 2, 2024Jun 2, 2024
    • zkWasm

      Public
      Rust
      130000Updated May 14, 2024May 14, 2024
    • coq-of-go

      Public
      Translation from Go to Coq - Experiment
      Coq
      2901Updated May 1, 2024May 1, 2024
    • move

      Public
      Rust
      704101Updated Apr 4, 2024Apr 4, 2024
    • Experiment on translation of Haskell Core to Coq
      Haskell
      1300Updated Feb 14, 2024Feb 14, 2024
    • Marinde Anchor-Based, first on mainnet, liquid-staking-program and mSOL->SOL swap pool
      Rust
      39000Updated Jan 13, 2024Jan 13, 2024
    • ink

      Public
      Parity's ink! to write smart contracts.
      Rust
      479100Updated Nov 1, 2023Nov 1, 2023