Open Source — Now in Development

AI-native.
Secure by construction.

C! is the first programming language designed from the ground up for AI-human collaboration. Linear types eliminate entire vulnerability classes. One codebase deploys everywhere.

Get Started Star on GitHub
10+
Vulnerability classes eliminated
3
Deployment targets
1
Unified codebase
wallet.cb 
// Linear types prevent double-spend
fn transfer(token: own Token, to: Address) -> Receipt {
    ledger.move(token, to)  // token consumed
}

fn bad() {
    let t = mint_token();
    transfer(t, alice);  // t consumed
    transfer(t, bob);    // COMPILE ERROR: t already consumed
}
Security by Construction

Entire vulnerability classes, eliminated at compile time

Not by discipline. Not by linting. Not by auditing. By the type system itself. If it compiles, these bugs are structurally impossible.

✓ Buffer overflows
✓ Use-after-free
✓ Double-spend
✓ Reentrancy attacks
✓ SQL injection
✓ Cross-site scripting
✓ Data races
✓ Integer overflow
✓ Null pointer deref
✓ Resource leaks
Why C!

Built for the future of software

C! brings together ideas that have never existed in a single language before.

🔒

Linear Type System

Every value has exactly one owner. Consumed values cannot be reused. Buffer overflows, use-after-free, double-spend — all impossible by construction.

🤖

AI-Native Design

Structured intent annotations let any AI understand what code should do. The compiler formally verifies it does. AI writes code, the type system proves it correct.

🌐

Universal Deployment

One codebase compiles to native binaries, WebAssembly, and blockchain bytecode. Frontend, backend, and smart contracts share the same types.

⚡

Actor Model Concurrency

No shared mutable state, no locks, no races. Isolated actors communicate via typed messages with supervision trees for fault tolerance.

📜

First-Class Smart Contracts

Reentrancy is impossible by construction thanks to linear state. Write decentralized applications with the same confidence as traditional software.

🛠

Self-Hosting Compiler

The C! compiler is written in C! itself, proving the language is powerful enough for systems-level work. Open source for humans and AI contributors alike.

See It in Action

Code that proves itself correct

Explore real C! examples showing how the type system and intent annotations work together.

transfer.cb 
#[intent("Transfer tokens between accounts,
         ensuring sender has sufficient balance,
         atomic — both sides update or neither does")]
#[invariant(total_supply_unchanged)]
#[pre(balances[from] >= amount)]
#[post(balances[to] == old(balances[to]) + amount)]
fn transfer(
    from: Address,
    to: Address,
    amount: u256
) {
    // Compiler proves this matches
    // the annotations above
}
AI Meets Formal Verification

Intent annotations bridge AI and correctness

Write what your code should do in natural language. The compiler formally verifies it does. Any AI can instantly understand any C! codebase.

  • ✓ Natural-language intent descriptions
  • ✓ Pre- and post-conditions checked at compile time
  • ✓ Invariants enforced across all code paths
  • ✓ AI can generate code; compiler proves it correct
shared/models.cb 
// Same type used in backend, frontend,
// AND smart contract
type User {
    id: UUID,
    name: String{len: 1..100},
    email: Email,
    role: Admin | Editor | Viewer,
}
Full-Stack Unified

One type definition, three deployment targets

Define your types once. Use them in your backend API, your frontend UI, and your smart contracts. No code generation, no schema drift, no bugs.

  • ✓ Shared types across all deployment targets
  • ✓ Refined types with built-in constraints
  • ✓ Sum types for safe exhaustive matching
  • ✓ Zero runtime overhead
wallet_service.cb 
actor WalletService {
    state balances: Map<Address, u256>

    on Transfer(from, to, amount) {
        verify!(balances[from] >= amount);
        balances[from] -= amount;
        balances[to] += amount;
        reply Receipt { tx_id: generate_id() }
    }
}
Concurrency Without Fear

Actor model with isolated state

Each actor owns its state exclusively. No shared memory, no locks, no data races. Communication happens through typed messages with built-in supervision.

  • ✓ Isolated mutable state per actor
  • ✓ Typed message passing
  • ✓ Supervision trees for fault tolerance
  • ✓ Data races impossible by construction
wallet.cb 
fn transfer(
    token: own Token,
    to: Address
) -> Receipt {
    ledger.move(token, to)
}

fn bad() {
    let t = mint_token();
    transfer(t, alice);
    transfer(t, bob);
    // ^ COMPILE ERROR: t already consumed
}
Linear Types

Resources that cannot be duplicated or forgotten

Linear types enforce that every resource is used exactly once. Tokens can't be double-spent. File handles can't leak. Memory can't be used after free.

  • ✓ Double-spend impossible at compile time
  • ✓ Use-after-free impossible at compile time
  • ✓ Resource leaks caught by compiler
  • ✓ Zero-cost abstraction — no runtime overhead
The C! Difference

From discipline to construction

Traditional languages ask developers to avoid mistakes. C! makes mistakes structurally impossible.

✗ Traditional approach

Write code, then audit for buffer overflows, race conditions, injection attacks. Hope reviewers catch everything. Ship and pray.

✓ The C! approach

The type system makes these bugs structurally impossible. If it compiles, the vulnerability class is eliminated. No audit needed for what cannot exist.

✗ AI + traditional languages

AI generates code, but humans must review every line for security. AI can't understand intent from code alone. Hallucinations become vulnerabilities.

✓ AI + C!

AI reads structured intent annotations. Generates implementation. Compiler formally verifies correctness. If it compiles, the AI got it right. Trust the math.

Ready to build the future?

C! is open source and welcoming contributors — both human and AI. Join us in building the language that makes secure software the default.

Get Started Star on GitHub Join the Community