Concrete Spec

This page is the living language overview and design reference for Concrete.

Last checked against the compiler in October 2026.

It exists for a different job than the essays in the series. The series argues for the design. This page records the language shape, constraints, and current implementation status in one place.

If you want the shorter editorial introduction, read Why Concrete Exists.

Status

Concrete is real, but incomplete.

Today the project has:

• a full Lean 4 compiler pipeline from parse through SSA and native code generation
• strict LL(1) parsing
• structured diagnostics across semantic passes
• capability tracking and audit reports
• explicit IR boundaries, including Core and SSA
• source-level contracts (#[requires], #[ensures], loop invariants) compiled into proof obligations with stable ids
• a concrete prove workflow that generates Lean proof workspaces and links registered theorems back to obligations
• proof-status, proof-bundle, VC, traceability, audit, and diff reports that keep evidence classes separate
• a built-in test runner, an interpreter, a formatter, and supporting tools such as snapshot diffing and a test-case reducer
• a growing low-level standard library

What it does not yet have:

• a fully formalized kernel connected end to end to the implementation
• verified elaboration and code generation
• a package manager and an LSP server

Design Principles

Concrete is organized around a few hard constraints:

1. Pure by default.
2. Explicit capabilities for effects.
3. Linear ownership by default.
4. No hidden control flow or hidden cleanup.
5. A grammar small enough to parse with one token of lookahead.
6. A language small enough that reports and proofs stay tractable.

Compilation Pipeline

The current compiler pipeline is:

Source
  -> Parse
  -> Resolve
  -> Desugar
  -> Check
  -> Elab
  -> CoreCanonicalize
  -> CoreCheck
  -> Mono
  -> Lower
  -> SSAVerify
  -> SSACleanup
  -> EmitSSA
  -> clang / linker

EmitSSA produces LLVM IR, which clang compiles and links into a native binary. There is also a built-in interpreter as an alternative execution path, useful for running programs without a native toolchain and for cross-checking the backend.

The architectural point is that Concrete has a real semantic boundary at Core IR and a real backend boundary at SSA. Core IR that passes CoreCheck is a validated artifact: downstream passes may assume its invariants hold, and the proof tooling attaches there. That keeps the compiler easier to reason about.

Types

Concrete includes:

• primitive scalars: Bool, Int and Uint (64-bit, also spelled i64/u64), sized integers i8/i16/i32 and u8/u16/u32, Float32 and Float64, Char, and String. A function with no return type returns unit.
• records via struct
• algebraic data types via enum, with named fields on variants
• generic types and traits with bounds
• raw pointers *const T and *mut T for low-level and FFI work
• references via &T and &mut T
• fixed-size arrays [T; N], built with [a, b, c] or [x; N]
• function pointer types such as fn(Int) with(Console) -> Int, which carry their capabilities

The shape is conventional on purpose:

struct Copy Player { points: Int }

enum MyResult {
    Ok { value: Int },
    Err { error: Int },
}

trait Scorer {
    fn score(&self) -> Int;
}

impl Scorer for Player {
    fn score(&self) -> Int { return self.points * 2; }
}

fn evaluate<T: Scorer>(entity: &T) -> Int {
    return entity.score();
}

Copy appears in the type declaration itself, so whether a type is linear or freely copyable is visible at the definition site. Enum values are taken apart with match, which must be exhaustive:

match r {
    MyResult::Ok { value } => { return value; },
    MyResult::Err { error } => { return error; },
}

A few declarations name things without adding machinery. newtype makes a distinct type with the same representation, type is a plain alias, and const names a compile-time value. Conversions between numeric types are always written out with as; nothing converts implicitly:

newtype UserId = u64;
type Block = [u8; 64];
const MAX_USERS: Int = 1000;

fn first_word(b: Block) -> u32 {
    return (b[0] as u32 << 8) | b[1] as u32;
}

The standard library direction is intentionally ordinary rather than magical. The goal is to shrink compiler-known surface area over time and keep more user-facing behavior in regular library code.

Control Flow and Patterns

Control flow is small and all of it is visible: if/else, while, for, match, break, continue, return, and defer. for is the C-style three-part loop, loops can carry labels, and match and if can produce values.

Patterns cover what you need to take data apart without nesting: OR patterns, guards, integer ranges, if let, while let, and destructuring let. Struct literals support field punning and a ..base update:

enum Shape {
    Circle { r: Int },
    Rect { w: Int, h: Int },
}

fn area(s: Shape) -> Int {
    let a: Int = match s {
        Shape::Circle { r } => 3 * r * r,
        Shape::Rect { w, h } if w == h => w * w,
        Shape::Rect { w, h } => w * h,
    };
    return a;
}

fn bucket(n: Int) -> Int {
    let b: Int = match n {
        0..=9 => 0,
        10 | 20 | 30 => 1,
        _ => 2,
    };
    return b;
}

fn or_zero(o: Option<Int>) -> Int {
    if let Option::Some { value } = o { return value; }
    return 0;
}

fn first_negative(xs: [Int; 8]) -> Int {
    let mut found: Int = -1;
    'scan: for (let mut i: Int = 0; i < 8; i = i + 1) {
        if xs[i] < 0 {
            found = i;
            break 'scan;
        }
    }
    return found;
}

struct Copy Point { x: Int, y: Int }

fn move_x(p: Point, x: Int) -> Point {
    return Point { x, ..p };
}

Patterns do not nest, and there are no tuples. Both are deliberate: a flat pattern is easy to read and easy to turn into proof terms.

Linearity

Owned values are linear by default. A linear value must be consumed exactly once.

That means:

• forgetting a value is a compile error
• using a value after move is a compile error
• destroying a value twice is a compile error

Cleanup is explicit:

let f: Handle = acquire();
defer destroy(f);

Here Handle implements the Destroy trait, which is what makes destroy(f) the way to consume it.

This is stricter than Rust’s affine ownership. The goal is visibility: resource lifetime becomes part of the program rather than hidden behind implicit Drop behavior.

Copy is explicit and opt-in. A type can only be Copy if all of its fields are Copy and it has no destructor obligations.

Borrowing

Borrowing lets code use a value without consuming it, while preserving linear ownership of the underlying resource.

Instead of Rust-style lifetime inference, Concrete uses scoped borrow blocks. A borrow block names the reference and names the region it lives in:

borrow owner as r in Region {
    // r: &T is available here; owner is frozen
}
// owner is usable again; r no longer exists

borrow mut owner as r in Region {
    // r: &mut T; exclusive access
}

While the block is active, the owner is frozen: it cannot be read, moved, or borrowed again. On block exit the owner thaws and the reference ceases to exist.

The broad rules are:

• immutable borrows can coexist
• mutable borrows are exclusive
• references cannot escape their region: escape analysis rejects a reference that outlives its block
• safe-callable functions cannot return references, directly, nested inside aggregates, or through generic instantiation

Concrete keeps this model intentionally lexical and explicit. It avoids signature-level lifetime machinery entirely, with no lifetime parameters and no elision rules, but it does so by accepting a smaller language surface.

Capabilities

Capabilities are static permissions declared on functions.

Examples:

// signatures only
fn read_file(path: String) with(File) -> String
fn serve() with(Network, Alloc, Console) -> Int
fn hash(data: &Bytes) -> Digest

A function with no capability annotation is pure. A function that allocates must declare with(Alloc). A function that touches files must declare with(File).

The current concrete capability set is: File, Network, Time, Env, Random, Process, Console, Alloc, and Unsafe. Std is a macro for the standard safe capabilities, and user-defined capability aliases expand before the rest of the compiler sees them.

Capabilities propagate transitively through the call graph. If f calls g, and g requires File, then f must also require File.

This makes capabilities a real public contract rather than a documentation convention.

You can name a group of capabilities with cap, and a generic function can be polymorphic over capabilities with <cap C>. That is how higher-order code stays honest: the function pointer type says what the callee needs, and the caller inherits it.

cap Logging = Console + Alloc;

fn log_line(n: Int) with(Logging) {
    println(n);
}

fn apply<cap C>(f: fn(Int) with(C) -> Int, x: Int) with(C) -> Int {
    return f(x);
}

apply(double, 4) with a pure double stays pure. apply(shout, 4) with a shout that needs Console needs Console too, and a caller that does not declare it gets a compile error.

Allocation

Allocation is treated as a first-class effect.

If code allocates on the heap, it requires with(Alloc). Today that is libc malloc; passing an allocator explicitly is planned.

That gives you two properties that most languages do not expose cleanly:

• allocation can be audited semantically
• which functions can allocate is part of the program structure

Stack allocation does not require Alloc.

Arithmetic

Integer arithmetic is checked. Overflow on +, -, and *, division or remainder by zero, a shift by the bit width or more, and negating the minimum value all trap at runtime, in every build. Array indexing out of bounds traps the same way, and an index that is out of bounds as a constant is a compile error.

When you want modular or clamped arithmetic you say so with a named operation. #[overflow_checked] asks for something else: it does not change what the code does, it makes the compiler generate a no-overflow obligation for each operation so you can prove the trap never fires.

fn mix(a: u32, b: u32) -> u32 {
    return wrapping_add(a, b) ^ (a >> 3);
}

fn brighten(pixel: u8, boost: u8) -> u8 {
    return saturating_add(pixel, boost);
}

#[overflow_checked]
fn add_capacity(len: i32, extra: i32) -> i32 {
    return len + extra;
}

Trust Model

Concrete separates low-level trust boundaries instead of collapsing them into one broad keyword.

• Capabilities express semantically visible effects.
• trusted fn and trusted impl mark pointer-level internal unsafety behind a safe API.
• trusted extern fn is a narrow carve-out for audited foreign bindings.
• with(Unsafe) marks foreign or semantically dangerous boundaries.

This separation matters because “does pointer tricks internally” and “can call arbitrary foreign code” are not the same kind of risk.

Errors

Errors are values. Concrete uses Result<T, E>, and you propagate an error by matching it and returning the Err arm yourself. There is no ?:

fn read_config(path: &String, mode: &String) with(File, Alloc) -> Result<Config, FsError> {
    let f: File = match File::open(path, mode) {
        Result::Ok { value } => value,
        Result::Err { error } => { return Result::<Config, FsError>::Err { error: error }; },
    };
    defer close_file(f);
    return parse(&f);
}

close_file and parse are ordinary functions defined elsewhere.

There are no exceptions and no hidden unwinding paths.

defer runs on every scope exit, including early returns.

Abort is separate and immediate. It is outside normal cleanup semantics.

Contracts and Proofs

Functions can carry source-level contracts:

#[requires(0 < n && n < 32)]
fn rotr(x: u32, n: u32) -> u32 {
    return (x >> n) | (x << (32 - n));
}

A contract is a claim, not a guarantee. The compiler turns each claim into proof obligations with stable ids, then attaches evidence. Preconditions are assumed at function entry and pushed to every caller; postconditions become exit obligations. Loops take explicit invariants and variants.

Evidence is tiered rather than binary. An obligation can be:

• discharged by a registered Lean theorem, kernel-checked
• closed by a Lean-owned decision procedure such as omega or bv_decide, with no external SMT solver in the trusted base for that obligation; bv_decide still carries the native-code trust documented in the axiom inventory
• constant-folded true at a call site
• assumed, planned, or still missing

The audit report shows the evidence class for every obligation. There is never a single green badge.

The full vocabulary is wider than that list. Besides proved_by_lean and proved_by_kernel_decision, a report can say solver_trusted (an external SMT solver closed it, and that solver is now in the trusted base; this is opt-in with --smt), tested_by_oracle, runtime_checked, enforced, assumed, trusted, partial, stale, vacuous (the claim only holds because its premise is impossible), counterexample, or unproven.

Postconditions name the return value result and can refer to a spec fn, a specification with no body and no code generated for it. Inside a function, assert(e); creates an obligation, assume(e); is a trapdoor that marks the function as assumed in the audit, and ghost let binds a value that exists only for proofs and is erased before code generation:

spec fn rotr_spec(x: u32, n: u32) -> u32;

#[requires(0 < n && n < 32)]
#[ensures(result == rotr_spec(x, n))]
fn rotr(x: u32, n: u32) -> u32 {
    return (x >> n) | (x << (32 - n));
}

fn byte_at(a: [u8; 16], i: i32) -> u8 {
    assume(0 <= i);
    assert(i < 16);
    ghost let last: i32 = 15;
    return a[i];
}

fn count_to_ten() -> i32 {
    let mut acc: i32 = 0;
    #[invariant(0 <= i && i <= 10)]
    #[variant(10 - i)]
    for (let mut i: i32 = 0; i < 10; i = i + 1) {
        acc = acc + 1;
    }
    return acc;
}

Proofs are linked in the source too. #[proof_by(...)] and #[ensures_proof(...)] name the Lean theorems, and #[proof_fingerprint("...")] records the body they were written against, so editing the body turns the proof stale.

concrete prove generates a Lean proof workspace for a function, links registered theorems back to their obligations, and supports replay so proofs stay tied to the source they were written against.

This is the part of the language that connects the essays’ argument to running code: the compiler does not just accept programs, it emits the facts about them that a proof can attach to.

Traits, Modules, and FFI

Traits are static dispatch only. The language avoids trait objects and most of the implicit machinery that tends to make systems languages harder to read and harder to formalize.

Modules use explicit imports and visibility. Imports name every symbol they bring in; everything is private unless marked pub:

import std.fs.{ File, FsError };

FFI exists, but it is deliberately narrow. extern fn declarations require FFI-safe types (integers, floats, Bool, Char, raw pointers, and C-layout structs), and foreign boundaries are tracked explicitly through the trust model:

#[repr(C)]
struct Timespec { sec: i64, nsec: i64 }

extern fn malloc(size: u64) with(Alloc) -> *mut u8;
extern fn clock_gettime(clock: i32, out: *mut Timespec) with(Time) -> i32;

#[repr(C)] gives a struct C layout. #[repr(packed)] and #[repr(align(N))] control padding and alignment. Every extern fn declares the effects the foreign code exercises, with with() for none, and the compiler rejects one that leaves them out. Calling a plain extern fn requires with(Unsafe) in the caller, unless the caller is trusted.

Projects, Tests, and Queries

A project is a Concrete.toml manifest and a src/ directory. concrete build, concrete run, and concrete test work on it, and concrete fmt formats a file. Test functions are marked #[test] and return 0 on success:

#[test]
fn test_bucket() -> i32 {
    if bucket(3) != 0 { return 1; }
    if bucket(20) != 1 { return 1; }
    return 0;
}

Every fact the compiler knows can be read as a report (--report caps, authority, effects, contracts, vcs, audit, proof-status, and more) or asked as a JSON query:

concrete main.con --query why-capability:greet:Console
concrete main.con --query predictable:main

The first answers with the call path that explains why greet needs Console. The second lists every predictable-profile gate main fails, with source locations.

Anti-Features

Concrete intentionally avoids a number of familiar features:

• garbage collection
• hidden allocation
• implicit destruction
• exceptions
• closures (function pointers carry no captured state)
• trait objects
• operator overloading
• reflection and eval
• implicit global state
• variable shadowing (decided; today the compiler rejects only shadowing a live linear value)
• undefined behavior in safe code

These are not omissions born of neglect; they are design constraints chosen to keep the language explicit, auditable, and mechanically tractable.

What You Can Say About Programs

If Concrete’s checker accepts a function, you can often say more than “it type-checks.”

Depending on the function, you may be able to say:

• it is pure
• it cannot allocate
• it cannot reach the network
• its trust boundaries are explicit
• its cleanup sites are visible
• it belongs to the proof-eligible fragment
• its contract obligations are discharged, assumed, or still open, with the evidence class visible in the audit report

That is the main point of the language.

Open Questions

Several important areas are still intentionally unfinished:

• concurrency model
• broadening the proof connection: contracts, obligations, and concrete prove exist today. Runtime-safety obligations are mostly closed automatically by decision procedures, but claims about values still need hand-written Lean proofs, and many of those are still missing
• long-term verified kernel boundary
• a package manager and editor support beyond syntax highlighting

Concrete is not trying to hide that incompleteness. The design and the implementation are meant to converge over time.