Topics

#compiler #formal-specification #formal-verification #programming-language #security #smart-contracts #web3

Language breakdown

Rust 93.2%

WebAssembly 3.9%

TypeScript 2.8%

Zig 0.1%

JavaScript 0.0%

Dockerfile 0.0%

▸ Files click to expand

README

🌀 Inference Programming Language

Inference is a programming language designed for building verifiable software. It is featured with static typing, explicit semantics, and formal verification capabilities available out of the box.

Inference allows for mathematically verifying code correctness without learning provers. Keep the implementation correct, even with vibecode.

[!IMPORTANT]

The project is in early development. Internal design and implementation are subject to change. So please be patient with us as we build out the language and tools.

Editor Support

Install the official VS Code extension for syntax highlighting:

Learn

Inference homepage
Access our Inference book for a guide on how to get started
Inference Programming Language specification

Inference Suite CLI (`infs`)

infs is the unified toolchain CLI for Inference. It provides subcommands for building, managing, and working with Inference projects.

Build Command

The infs build command compiles Inference source through three phases:

Parse (--parse) – Build the typed AST with the inference-parser
Analyze (--analyze) – Perform type checking, static analysis, and semantic validation
Codegen (--codegen) – Emit WebAssembly binary with optional Rocq translation

Phases run in canonical order (parse → analyze → codegen). When no phase flag is given, infs build defaults to full compilation and writes the WASM binary to disk.

infs build operates in two modes. Given a path, it compiles that single file. With no path, it runs in project mode: it discovers the project's Inference.toml by walking up from the current directory and compiles src/main.inf together with every file it reaches through use imports — the project's module hierarchy — with output rooted at the project directory. infs run mirrors the same two modes.

Basic Usage

# Full compilation (default — no flags needed)
./target/debug/infs build path/to/file.inf
Parse only (syntax check)
cargo run -p infs -- build path/to/file.inf --parse

Compilation Modes

The compiler supports two modes that control optimization and verification behavior:

compile produces optimized production binaries. Non-deterministic spec nodes are stripped since they have no runtime meaning.
proof produces WASM for formal verification. Spec functions (containing non-deterministic operations) are compiled unoptimized to preserve structural correspondence with the source code for Rocq formalization. Execution functions use the target's release optimization so that proofs cover the actual deployed code.

Read more about compilation modes in the book.

Output Flags

-o – Generate WASM binary file in out/ directory
-v – Generate Rocq (.v) translation file in out/ directory

Show Version

infs version
infs --version

Exit Codes

| Code | Meaning | | ---- | -------------------------- | | 0 | Success | | 1 | Usage / IO / Parse failure |

Future Commands (Planned)

infs install – Download and install toolchain versions
infs new – Scaffold new projects
infs doctor – Verify installation health
infs (no args) – Launch TUI interface

Distribution

Prebuilt binaries are available for each release. Two CLI tools are distributed:

infs - Full-featured toolchain CLI (recommended for all users)
infc - Standalone compiler CLI

Release Artifacts

| Platform | infs | infc | | ----------- | --------------------------------- | --------------------------------- | | Linux x64 | infs-linux-x64.tar.gz | infc-linux-x64.tar.gz | | Windows x64 | infs-windows-x64.zip | infc-windows-x64.zip | | macOS ARM64 | infs-macos-apple-silicon.tar.gz | infc-macos-apple-silicon.tar.gz |

Directory Structure

<distribution-folder>/
└── infs (or infc)          # The CLI binary

The CLI binaries are self-contained and require no external dependencies.

Building from Source

To build Inference from source:

For detailed platform-specific setup instructions, see:

Dependencies

No external binaries are required. The compiler generates WebAssembly directly via wasm-encoder.

Build Steps

Clone the repository:

git clone https://github.com/Inferara/inference.git
   cd inference

Build the project:

cargo build --release

The compiled binaries will be in target/release/ (infs and infc).

Build Commands

The workspace is configured for efficient development:

cargo build - Builds only the core/ crates (faster for core development)
cargo build-full - Builds the entire workspace, including tools and tests
cargo test - Runs tests for core/ crates and the tests/ integration suite
cargo test-full - Runs tests for all workspace members, including tools