Skip to content

@formal-land Formal Land

Change the repository type filter

All

    Repositories list

    36 repositories

    • CompPoly

      Public
      A computable model of Polynomials in Lean.
      Lean
      •
      Apache License 2.0
      •20•0•1•0•Updated May 14, 2026May 14, 2026

    • formal.land

      Public
      Formal Land website
      JavaScript
      •3•1•0•4•Updated May 6, 2026May 6, 2026

    • Yellowstone

      Public
      A free-monad library compatible with any programming language 🦬
      Go
      •
      MIT License
      •0•0•0•0•Updated Apr 21, 2026Apr 21, 2026

    • rocq-of-rust

      Public
      Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.
      rustproofformal-verification
      rustproofformal-verificationrocq
      Rocq Prover
      •44•1.1k•28•30•Updated Apr 10, 2026Apr 10, 2026

    • rocq-of-solidity

      Public
      Formal verification for Solidity smart contracts with the theorem prover Rocq. Ensure no vulnerabilities for your smart contracts.
      solidityformal-verificationrocq
      solidityformal-verificationrocqrocq-prover
      Rocq Prover
      •
      GNU General Public License v3.0
      •6.1k•49•0•1•Updated Apr 6, 2026Apr 6, 2026

    • 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
      •
      MIT License
      •4•44•12•2•Updated Mar 29, 2026Mar 29, 2026

    • 100-specification-smart-contracts

      Public
      💯 Full Specification Project for Smart Contracts
      Rocq Prover
      •
      MIT License
      •2•8•0•0•Updated Feb 8, 2026Feb 8, 2026

    • garden

      Public
      Make your zero-knowledge circuits safe with formal verification! 🍀
      Rocq Prover
      •
      MIT License
      •6•34•17•6•Updated Nov 27, 2025Nov 27, 2025

    • oxidefier

      Public
      Port your Soldity smart contracts to Rust, with ease and 💯 equivalence
      Rust
      •0•4•3•1•Updated Nov 20, 2025Nov 20, 2025

    • pico

      Public
      Rust
      •
      Apache License 2.0
      •51•0•0•1•Updated Oct 26, 2025Oct 26, 2025

    • Plonky3

      Public
      A toolkit for polynomial IOPs (PIOPs)
      Rust
      •
      Apache License 2.0
      •431•0•0•1•Updated Oct 16, 2025Oct 16, 2025

    • openvm

      Public
      A performant and modular zkVM framework built for customization and extensibility.
      Rust
      •
      Apache License 2.0
      •103•2•0•1•Updated Aug 27, 2025Aug 27, 2025

    • llzk-lib

      Public
      Library for parsing, generating, and analyzing LLZK code.
      C++
      •
      Apache License 2.0
      •12•0•0•1•Updated Aug 20, 2025Aug 20, 2025

    • go-corset

      Public
      A port of the Corset tool into Go.
      Go
      •
      Apache License 2.0
      •13•1•0•1•Updated Jul 2, 2025Jul 2, 2025

    • rocq-of-noir

      Public
      Formal verification tool for Noir programs using the Rocq system
      Rust
      •
      Apache License 2.0
      •392•10•1•2•Updated May 28, 2025May 28, 2025

    • rocq-code-assistant

      Public
      Visual Studio Code extension for AI-assisted coding
      TypeScript
      •1•6•2•0•Updated May 2, 2025May 2, 2025

    • revm

      Public
      Rust implementation of the Ethereum Virtual Machine.
      Rust
      •
      MIT License
      •1k•0•0•1•Updated Feb 25, 2025Feb 25, 2025

    • zirgen

      Public
      Zirgen compiler and RISC Zero circuits
      C++
      •
      Apache License 2.0
      •31•0•0•0•Updated Feb 10, 2025Feb 10, 2025

    • execution-specs

      Public
      Specification for the Execution Layer. Tracking network upgrades.
      Python
      •
      Creative Commons Zero v1.0 Universal
      •456•0•0•1•Updated Dec 30, 2024Dec 30, 2024

    • circom

      Public
      zkSnark circuit compiler
      WebAssembly
      •
      GNU General Public License v3.0
      •364•1•0•1•Updated Dec 22, 2024Dec 22, 2024

    • coq-evm

      Public
      Hash functions used in EVM implemented in Coq.
      Coq
      •
      Apache License 2.0
      •1•0•0•1•Updated Dec 11, 2024Dec 11, 2024

    • sp1

      Public
      The fastest, most feature-complete zkVM for developers.
      Rust
      •
      Apache License 2.0
      •655•0•0•0•Updated Nov 18, 2024Nov 18, 2024

    • shared-documentation

      Public
      Shared documentation for the developments
      MIT License
      •1•1•0•0•Updated Oct 23, 2024Oct 23, 2024

    • move-sui

      Public
      Rust
      •23•0•0•0•Updated Sep 6, 2024Sep 6, 2024

    • coq-of-ocaml

      Public
      Formal verification for OCaml
      compilerocamlcoq
      compilerocamlcoq
      OCaml
      •
      MIT License
      •20•275•5•13•Updated Aug 5, 2024Aug 5, 2024

    • .github

      Public
      1•1•0•0•Updated Jun 2, 2024Jun 2, 2024

    • zkWasm

      Public
      Rust
      •
      Apache License 2.0
      •132•0•0•0•Updated May 14, 2024May 14, 2024

    • coq-of-go

      Public
      Translation from Go to Coq - Experiment
      Coq
      •
      MIT License
      •2•10•0•1•Updated May 1, 2024May 1, 2024

    • move

      Public
      Rust
      •
      Apache License 2.0
      •698•1•0•1•Updated Apr 4, 2024Apr 4, 2024

    • coq-of-hs-experiment

      Public
      Experiment on translation of Haskell Core to Coq
      Haskell
      •
      GNU Affero General Public License v3.0
      •1•3•0•0•Updated Feb 14, 2024Feb 14, 2024
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.