/safepkt_smart-contract-example

Smart Contract Verification Example project for SafePKT verifier

Primary LanguageRustApache License 2.0Apache-2.0

SafePKT Buggy Smart Contract

This is a an example smart contract with a BUG, do not use it in production! It is here for demonstrating how to do SafePKT symbolic execution based static analysis.

This project is implemented in the context of the European NGI LEDGER program.

This project is based on a Plain Multisig smart contract example from ink! eDSL,
which depends on the substrate platform.

Opening this project in a VS Code workspace enables developers and researchers to verify the library-oriented program written in Rust with SafePKT tooking from a text editor.

See SafePKT description

Acknowledgment

We're very grateful towards the following organizations, projects and people:

  • the Project Oak maintainers for making Rust Verifications Tools, a dual-licensed open-source project (MIT / Apache).
    The RVT tools allowed us to integrate with industrial-grade verification tools in a very effective way.
  • the KLEE Symbolic Execution Engine maintainers
  • the Parity Technologies organization,
    for substrate platform and ink! eDSL allowing us to write smart contract in Rust
  • the Rust community at large
  • All members of the NGI-Ledger Consortium for accompanying us
    Blumorpho Dyne FundingBox NGI LEDGER

License

This project is distributed under either the MIT license or the Apache License.