Inferara

Independent research group specializing in Programming Languages and Formal Methods Our goal is to make formal verification accessible for Web3 developers.

Read Our Papers

We know that automatic theorem provers^1,2 are the most powerful tools to find errors in code. But except inside universities, almost no one uses it.

So we aim to:

Make automatic theorem provers accessible to developers
Make smart contracts more secure
Prevent the next multi-million dollar hack

We keep our work open-sourced, so we need your support 💌.

Support Inferara

The first developer-friendly formal specification language designed for Web3.

Inference lets specify and formally prove smart contracts properties without needing a PhD in math.

How it works

        flowchart LR
            Inference --> WAT
            WAT --> WASM
            WASM --> V;

Inference compilation process consists of the following steps:

Transpile Inference code to WebAssembly Text (WAT)
Compile WAT to WebAssembly (WASM)
Translate WASM to V (proof assistant code)

        graph TD
            A[Program]
            PA[Proof]
            A -->|Inductive program simulation| PA
            PA --> B
            PA --> C
            
            subgraph OC[Operation context]
                B[Final machine state]
            end

            subgraph LC[Logic context]
                C[List of theorems that must be proven]
            end

            C -.-> |Prove the state is reachable: no traps, out of gas, etc.| B
            C --> H[Hummer]
            C --> S[Inferara tactics]
            S -.-> H
            H -.-> S
            S --> D([✅ correctness certificate])
            H --> D;

Inference is a formal specification programming language based on Inferara's research into non-deterministic abstract machine execution. For more details, read our papers.

Inference documentation