MicSE is a tool for verifying and testing Tezos smart contracts written in Michelson. Michelson is a native smart contract language of the Tezos Blockchain. MicSE verifies and refutes michelson code with initial storage of smart contract by cooperating prover and refuter. MicSE can verify the absence of runtime failures of Michelson programs, e.g., no arithmetic overflow. Also, MicSE supports verification of user-provided assertions.
- OCaml (v.4.10.0): We use OCaml language to programming.
- Opam (v2.0.5): We use Opam to manage package of OCaml.
- Batteries
- Core (v0.14.0)
- Dune (v2.4.0): We use Dune to manage build system of OCaml project.
- Logs
- Menhir
- Mtime
- Ptime
- Ocamlgraph
- Yojson
- Z3 (v4.8.13)
- Zarith
We are following Angular's commitizen rules for formatting git commit message. This allows you to read messages that are easy to understand when looking for project history. It also uses the git commit message to generate our CHANGELOG file.
This project is funded by Tezos Foundation: Verification and Testing Infrastructure for Tezos Contracts.
Authored and maintained by Jisuk Byun, Heewoong Jang
Github @cushionbadak Github @JormalHeewoongJang