SafePKT Verifier Extension for Visual Studio Code

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

This prototype aims at bringing more automation to the field of software verification tools targeting rust-based programs.

See SafePKT description

Features

Rust-based smart contract Task-based verification for VS Code editor.

Requirements

The extension should be able to send HTTP requests to SafePKT backend.

Extension Settings

Include if your extension adds any VS Code settings through the contributes.configuration extension point.

For example:

This extension contributes the following settings:

• safePKTSmartContractVerifier.backend: ["http://vinny.cjdns.fr"]

This value is an array, which can possibly contain as a single string value

• an HTTP or HTTPS protocol scheme ("http://")
• a host name ("vinny.cjdns.fr")
• a base path ("" empty by default)

resulting in the default value "http://vinny.cjdns.fr"

Demo

safepkt-smart-contract-verification.mp4

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
• Tree-sitter, a parser generator tool and an incremental parsing library
• the Rust community at large
• All members of the NGI-Ledger Consortium for accompanying us
  
  
  

License

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