General

[0xGeorgii]

This is a general discussion, and everyone is welcome to join.

[tinc-x]

Inferara is using deductive verification.
What are the benefits of using deductive verification in ensuring the correctness of smart contracts?

[0xGeorgii]

Hey @tinc-x, thanks for raising this question. I list 3 points:

Exhaustive correctness guarantees

Usual test cases check particular function input-output scenarios, while fuzzers cover a large number of such scenarios. In contrast, deductive verification generates proof obligations that cover all possible execution paths and states, so you know formally that your contract meets (or behaves as it is defined in) its spec without blind spots. To make this process easier and more native to developers, we are developing Inference programming language.

Inspectable proof artifacts

Inductive proof is based on a formal model of the execution environment (VM). So, accessible:

1. Formal model
2. Formal properties (specification)
3. Formal proof

Meaning, that it is possible to see these artifacts and understand the proof and ensure the logic inside is correct and really sound. Some other tools can give you a result, but they are not fully human-traceable. In our case, the key is that the proof is open and anyone at any moment can check it.

Specs as standalone documentation

The specification itself is a super valuable artifact. A well‐written formal spec doubles as unambiguous design documentation, clarifying intent for developers and stakeholders before any code is written. Thus, a spec is like a blueprint for the smart contract, but formal and written in a formal language.

[tinc-x]

Thank you for the detailed response! I appreciate the clarity on the benefits of deductive verification for smart contracts.
The transparency of the proof artifacts is indeed a strong point. It’s reassuring to know that the proofs can be inspected and verified by anyone. This could greatly enhance trust in the smart contracts. How do you envision the community engaging with these proofs? Will there be a platform for sharing insights or improvements based on the proofs?

[0xGeorgii]

The correctness certification is the process of creating a tuple (specification + source code + proof). This set is immutable, meaning these 3 artifacts must have the same version, each smart contract release must be equipped with the spec and proof.

Because a community creates and uses smart contracts, our goal is to make the community self-driven in the process of creating specifications, and our team will lead compiler and tooling development. We will create as many educational materials as possible to make people learn and become familiar with the concepts we offer. Inference itself is designed to be very similar to Rust (or C-like) syntax. It is relatively low level, but its semantics is quite straightforward, there are only a few new concepts:

• Uzumaki keyword
• Forall block
• Assume block
• Exists block
• Unique block

Since the proof itself is a self-sufficient and self-contained Rocq source code, it can be executed anywhere with a minimal proof assistant environment ready (various environments are available). In addition, we want to have a platform with a database of correctness certificates so users can check the validity of a proof. As you mentioned, it will be a good idea to have an associated discussion platform (like a forum) so every correctness certificate can be discussed separately by the community.