Skip to content

@formal-land Formal Land

Change the repository type filter

All

    Repositories list

    21 repositories

    • coq-of-rust

      Public
      Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
      rustcoqproofformal-verification
      Coq
      •
      GNU Affero General Public License v3.0
      •14•404•14•17•Updated Oct 8, 2024Oct 8, 2024

    • formal.land

      Public
      Formal Land website
      JavaScript
      •1•0•0•4•Updated Oct 7, 2024Oct 7, 2024

    • coq-of-solidity

      Public
      Formal verification for Solidity smart contracts with Coq 🐓 Verify arbitrary properties on your smart contracts and make no bugs!
      coqsolidityformal-verification
      Coq
      •
      GNU General Public License v3.0
      •5.7k•11•2•1•Updated Oct 5, 2024Oct 5, 2024

    • coq-of-python

      Public
      Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.
      Coq
      •
      MIT License
      •0•30•12•2•Updated Sep 10, 2024Sep 10, 2024

    • move-sui

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

    • coq-of-ocaml

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

    • coq-evm

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

    • .github

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

    • zkWasm

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

    • coq-of-go

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

    • move

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

    • shared-documentation

      Public
      Shared documentation for the developments
      MIT License
      •0•0•0•0•Updated Apr 2, 2024Apr 2, 2024

    • coq-of-hs-experiment

      Public
      Experiment on translation of Haskell Core to Coq
      Haskell
      •
      GNU Affero General Public License v3.0
      •0•1•0•0•Updated Feb 14, 2024Feb 14, 2024

    • liquid-staking-program

      Public
      Marinde Anchor-Based, first on mainnet, liquid-staking-program and mSOL->SOL swap pool
      Rust
      •
      Other
      •30•0•0•0•Updated Jan 13, 2024Jan 13, 2024

    • ink

      Public
      Parity's ink! to write smart contracts.
      Rust
      •
      Apache License 2.0
      •425•0•0•0•Updated Nov 1, 2023Nov 1, 2023

    • coq-of-js

      Public
      🌍 🐓 Formal verification for JavaScript
      javascriptcoqverification
      JavaScript
      •
      MIT License
      •0•10•1•25•Updated Jul 10, 2023Jul 10, 2023

    • coq-of-LLBC

      Public
      Translate Rust 🦀 LLBC code (generated by https://github.com/AeneasVerif/charon) to Coq 🐓
      rustcoq
      OCaml
      •0•4•0•0•Updated Feb 9, 2023Feb 9, 2023

    • coq-of-ts

      Public
      Formal verification for TypeScript
      typescriptcoqverification
      TypeScript
      •
      MIT License
      •0•11•0•0•Updated Jan 27, 2023Jan 27, 2023

    • candy-for-charon

      Public
      Interface with the rustc compiler for the purpose of program verification
      Rust
      •
      Apache License 2.0
      •15•0•0•0•Updated Jan 25, 2023Jan 25, 2023

    • opam-coq-archive

      Public
      Archive for all Coq related OPAM packages organized in various repositories
      OCaml
      •
      GNU Lesser General Public License v2.1
      •135•0•0•0•Updated Feb 14, 2022Feb 14, 2022

    • coq-bonsai

      Public
      🌳 Generate a fresh bonsai in your terminal
      Coq
      •
      GNU General Public License v3.0
      •0•24•0•0•Updated Oct 4, 2021Oct 4, 2021