The substrate for software you don't fully trust.
In Lex, effects are part of the type. What a piece of code is allowed to do is checked before it runs and re-checked at runtime — from sandboxing a function an LLM just wrote, up to bounding what a learned policy may do to a robot. Trust by verification, not comprehension.
Alpibru is one founder and agentic AI. The stack below — a language, a runtime, a registry, and production stacks across finance, energy, and robotics — is the demonstration: it is possible because trust here is mechanical (typed effects, tests, tamper-evident attestation), not headcount. This is the new shape of a software company.
Trust by construction
Effects are the contract
A [net] function can't
touch the filesystem — the program is rejected at type-check, before it runs.
Capabilities, enforced
lex-os runs code in a sealed box with a granted budget; the supervisor mediates every command and can kill or reprovision.
Tamper-evident by default
Every action is a content-addressed, hash-chained event — an attestation trail you can replay and verify, not just trust.
See it live
The same idea — capability and audit enforced by construction — as two things you can actually go run, not just read about.
lex-code →
An experiment in verified AI coding — not something to switch to tomorrow. Point it at a task in plain English; it writes real Lex and closes the turn against the type checker and a declared acceptance, not a transcript claiming success.
curl -fsSL https://raw.githubusercontent.com/alpibrusl/lex-code/main/install.sh | bash
Build on Lex →
Install the toolchain and build on the stack below — effects, capabilities, and a tamper-evident trail, enforced by the type system.
The stack
Run it
## install the toolchain (Linux/macOS/Windows binaries)
# https://github.com/alpibrusl/lex-lang/releases
## a function that declares [net] cannot reach the filesystem:
fn fetch(url :: Str) -> [net] Result[Str, Str] { io.read("/etc/passwd") }
# rejected at type-check — the effect isn't in the signature.