Pinned Repositories
coq-bonsai
🌳 Generate a fresh bonsai in your terminal
coq-of-go
Translation from Go to Coq - Experiment
coq-of-hs-experiment
Experiment on translation of Haskell Core to Coq
coq-of-js
🌍 🐓 Formal verification for JavaScript
coq-of-LLBC
Translate Rust 🦀 LLBC code (generated by https://github.com/AeneasVerif/charon) to Coq 🐓
coq-of-ocaml
Formal verification for OCaml
coq-of-python
Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.
coq-of-rust
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
coq-of-solidity
Formal verification for Solidity smart contracts with Coq 🐓 Verify arbitrary properties on your smart contracts and make no bugs!
coq-of-ts
Formal verification for TypeScript
Formal Land's Repositories
formal-land/coq-of-rust
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
formal-land/coq-of-ocaml
Formal verification for OCaml
formal-land/coq-of-python
Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.
formal-land/coq-bonsai
🌳 Generate a fresh bonsai in your terminal
formal-land/coq-of-ts
Formal verification for TypeScript
formal-land/coq-of-js
🌍 🐓 Formal verification for JavaScript
formal-land/coq-of-solidity
Formal verification for Solidity smart contracts with Coq 🐓 Verify arbitrary properties on your smart contracts and make no bugs!
formal-land/coq-of-go
Translation from Go to Coq - Experiment
formal-land/coq-of-LLBC
Translate Rust 🦀 LLBC code (generated by https://github.com/AeneasVerif/charon) to Coq 🐓
formal-land/coq-of-hs-experiment
Experiment on translation of Haskell Core to Coq
formal-land/move
formal-land/candy-for-charon
Interface with the rustc compiler for the purpose of program verification
formal-land/formal.land
Formal Land website
formal-land/ink
Parity's ink! to write smart contracts.
formal-land/liquid-staking-program
Marinde Anchor-Based, first on mainnet, liquid-staking-program and mSOL->SOL swap pool
formal-land/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
formal-land/shared-documentation
Shared documentation for the developments
formal-land/.github
formal-land/coq-evm
Hash functions used in EVM implemented in Coq.
formal-land/move-sui
formal-land/zkWasm