Lily Labs logoLily Labs

Verified software composition

BriX

Software you can prove, built from blocks you can trust.

Most software is trusted the way medieval medicine was practised: by reputation, ritual, and testing a few cases. BriX makes software trustworthy the way a bridge is trustworthy — every part certified, every connection checked, every step of construction on record.

How it worksRequest a briefing

The problem

Thirty years. The same five failures.

The most damaging software disasters on record are not exotic. They repeat. And the industry’s answer to all of them is the same: test more, and hope.

1999

Mars Climate Orbiter

$327M

burned up over Mars

One team's software produced thrust in pound-force. Another's read it as metric. Both handled a perfectly valid number.

cause: pound-force read as newtons

1996

Ariane 5, flight 501

37 sec

from launch to loss

The guilty component had worked flawlessly for years — on Ariane 4. A faster rocket produced a value nobody had guarded against.

cause: correct part, fatal new context

2012

Knight Capital

$440M

lost in 45 minutes

A deployment reached seven of its eight servers. The eighth ran a stale component that misread a repurposed flag.

cause: reviewed source, wrong running software

2014

Heartbleed

64 KB

of memory, per request

A message said “I am sending 64,000 bytes” while actually sending one. Servers worldwide handed back whatever sat in memory.

cause: an input nobody had mapped

2020

SolarWinds

signed

and shipped to thousands

Attackers never touched the source code developers reviewed. They compromised the build system, and malicious code shipped inside digitally signed updates.

cause: the build betrayed the source

2021

Log4Shell

1 string

ran code on millions of servers

A logging library treated a specially crafted piece of text as an instruction to fetch and execute code.

cause: text treated as an instruction

2024

xz-utils backdoor

2 years

of politely earning trust

A contributor spent two years becoming a maintainer of a core Linux library, then inserted a backdoor. The library's name never changed — only its contents. Caught by luck.

cause: trusted by name, not by content

2026

And now AI writes code

all of it

automated, at machine speed

AI assistants generate software and pick dependencies faster than humans can review — with the same blind trust in names, the same untyped connections, the same unreviewed glue.

cause: every weakness above, accelerated

Testing runs a few cases and extrapolates. It cannot prove that every connection is valid, that every input has a defined fate, or that the thing running is the thing reviewed. These failures aren’t rare events to be tested away. They are what the standard way of building software permits.

The idea

What if software snapped together like bricks?

Every mature engineering field builds from certified parts. Nobody hand-forges a bolt for a bridge and hopes. Software is the last engineering discipline that hand-writes almost everything — and hopes. BriX changes the construction method itself, with three moves.

Move 1

Programs are assembled, not written

A BriX program is a wiring diagram of sealed blocks. Each block does one defined job — parse this, verify that, decide the other. The diagram is the program. There is no separate pile of text that “really” defines it, and no glue code hiding between the parts.

Programming stops being typing and becomes architecture: choosing and connecting proven parts.

A BriX assembly: three checked steps, sealed parts, and a wired exit for anything invalidFlowchart of a minimal BriX program read left to right. Three sealed blocks — read the message, check who sent it, carry out the order — are wired in sequence. Every connection between blocks passes checks before it is allowed to exist, shown as a chip on each wire reading checks pass. Each block carries a small sealed tick, meaning its contents are fingerprinted and cannot be silently altered. A dashed route leaves the first block and ends at a dashed box labelled anything invalid ends up here, never ignored: bad input always has a defined destination instead of an undefined fate. The caption beneath states that the finished assembly becomes a proven part itself, ready to be used as a single sealed block in a larger assembly.read themessagesealed ✓check whosent itsealed ✓carry outthe ordersealed ✓checks pass ✓checks pass ✓✗anything invalid ends up here — never ignoredthe finished assembly becomes a proven part itself
A minimal BriX assembly, read like a flowchart. Note the bottom route — bad input always has somewhere to go.

Move 2

Every block is identified by its fingerprint

Today, when software imports a library by name, it gets whatever currently answers to that name. That is how the xz-utils backdoor nearly reached most of the world’s servers — the name never changed, only the contents.

In BriX, a block’s identity is a cryptographic hash of what it actually contains — a fingerprint, not a filename. Change one bit and it is a different block, refused everywhere downstream. The fingerprint is recomputed before every single use, so tampering is caught at the door. Nothing can be quietly swapped, because a swap is a change of identity.

filename vs fingerprint

today

import “compression-library”

→ whatever answers to that name today. Contents unknown.

BriX

use block cs_8f41…d2

→ exactly one thing in the universe. Recomputed and checked before every use.

Move 3

Every connection passes through gates

Before two blocks may be wired together, the connection has to clear five mechanical checks — like stamps at a border post. Do the data types match? Do the units match — because metres are not seconds and pound-force is not newtons? Does the receiving block get every guarantee it demands? No accidental loops? And does every possible rejection have a wired destination?

Fail any gate and the composition is refused before the software exists to fail at runtime — with a report naming the connection and the reason.

Five checks before any two parts connect — border control for dataTwo wiring attempts, one above the other. Top: a solid wire runs left to right from a block named part A to a block named part B, passing through five small checkpoint stamps, each marked with a tick and labelled in plain English: right shape, right units, promises kept, no tangles, and bad input has an exit. All five checks pass, so the wire reaches part B — the connection is allowed to exist. Bottom: a dashed wire leaves a block labelled part sending pounds, heading for a block labelled part expecting metric. It stops at a single highlighted stamp marked with a cross and labelled wrong units. The right-hand block is drawn dashed because the wire never reaches it — the mismatched connection is refused before the software is ever assembled. Caption: stopped before launch — the check the 327 million dollar Mars mission never had.Five checks before any two parts connectpart A✓✓✓✓✓right shaperight unitspromises keptno tanglesbad inputhas an exitpart Bpart sending pounds✗wrong unitspart expecting metricstopped before launch — the check the $327M Mars mission never had

And then it stacks. A composition that passes all gates is sealed: put into standard form, fingerprinted, stored as a new block. Verified assemblies become parts for bigger verified assemblies — turtles all the way up. Verification effort is spent once and reused forever, which is what makes proof scale in a way testing never has.

Tests of the tests

Who checks the checker?

Everyone has met the test suite that passes in the lab and means nothing in production. BriX takes testing personally.

Every block ships with its own attackers — sealed adversary blocks that throw boundary values, malformed inputs, unit mismatches, and known exploits at it. A block enters the catalogue only when it survives.

And every attacker is paired with a discriminator — a sealed checker that proves the attack actually bites. Because a test that doesn’t bite is worse than no test: it manufactures confidence.

The admission record stores the fingerprints of exactly which attack and which discriminator were used. “It was tested” is never a stale claim.

Every part is attacked before it’s trustedDiagram of how a part earns its place in the BriX catalogue. On the left sits the part being tested. To its upper right, a dedicated attacker tries everything to break it — drawn as three strike arrows hitting the part. Below the attacker sits a referee whose dashed arrow points at the attacker, not the part: the referee’s job is to prove the attacker really tried, so a weak or lazy attack never counts as a pass. Only when the part survives a genuine attack is it allowed onto the shelf — shown as a sealed bar at the bottom reading “survived — allowed onto the shelf”. Nothing is trusted until it has been attacked, and the attack itself has been checked.the partthe attackertries everything to break itthe refereeproves the attacker really triedchecks✓ survived — allowed onto the shelf
One unproven part makes the whole assembly count as unprovenA horizontal chain of five blocks joined like links in a physical chain. Four blocks are labelled proven, each with a check mark. The middle block is labelled unproven with a cross, drawn with a dashed outline in the accent colour — it is the weakest link. An arrow points down from the unproven block to a wide verdict bar reading: the whole assembly counts as unproven. A caption beneath adds that the verdict is computed automatically — nobody gets to claim otherwise. The assurance level of an assembly is always inherited from its weakest part, derived from the assembly graph itself rather than asserted by a vendor.proven ✓proven ✓unproven ✗proven ✓proven ✓the whole assembly counts as unprovencomputed automatically — nobody gets to claim otherwise

No hiding

The weakest part decides

Every block carries a verification level — from “exists and is fingerprinted” up to “formally checked”. When blocks are composed, the assembly inherits the level of its weakest constituent.

So one unreviewed part can never hide inside a reviewed product. A safety-critical deployment can mechanically refuse anything below its threshold. Assurance stops being a claim in a brochure and becomes a property computed from the graph — and marketing doesn’t get a vote.

The consequence

Not mitigated — inexpressible

Go back to the disaster cards. In BriX, those aren’t risks to manage down. The architecture has no way to say them.

Failure classWhy BriX cannot express itThe incident it answers
Silent dependency substitutionIdentity is the fingerprint of the content. A changed dependency is a different identity, refused everywhere.xz-utils (2024)
Unit and meaning mix-upsThe unit gate rejects the connection at assembly. Two ports can both carry a number and still be refused.Mars Climate Orbiter (1999)
Correct part, fatal contextEvery input has a defined accept-or-reject fate. The out-of-range value is a wired rejection, not undefined behaviour.Ariane 5 flight 501 (1996)
Memory disclosure via malformed inputThe malformed message is a rejection with a destination, not a memory read.Heartbleed (2014)
Injected code via crafted inputInput is typed data with a defined fate — never an instruction.Log4Shell (2021)
Build-time code insertionArtifact attestation chains the shipped binary to the verified source graph. Deployment refuses artifacts that don't verify.SolarWinds (2020)
Wrong or stale version deployedDeployment-time fingerprint checks refuse any artifact whose attestation doesn't match.Knight Capital (2012)

One honest note. BriX moves correctness inside blocks onto proofs and sealed evidence, and correctness between blocks onto mechanical gates. Asking the system to do the wrong thing remains a human problem. BriX shrinks the failure surface to that question — which is where human attention belongs.

Why this matters now

AI writes code faster than anyone can read it

Every defence and infrastructure organisation now faces the same choice. Ban AI coding — and fall behind. Or trust it — and inherit every failure pattern above, automated. BriX is the structural third answer: let AI assemble, because assembly is checked.

An AI that can only select from the verified shelf cannot introduce a buffer overflow, an injection flaw, or a swapped library — no sealed block contains those classes, and every connection it proposes passes the same gates as a human’s. When the AI gets it wrong, it picks a weaker-but-valid block or proposes a connection the gates refuse. Failure degrades to suboptimality, not to exploitability. And an AI proposing a genuinely new block gets no shortcut: same attacks, same discriminators, same admission bar.

It doesn’t matter whose AI it is. The architecture checks the work.

Certification is authorship-independent — human, AI, or generator, the chain of evidence is identical.

Status

Where it is today

As of , BriX is a working system with a real catalogue — not a slide deck.

1,500+
sealed catalogue entries
10,000+
adversarial checks passing
5
assembly gates operating
2
runtimes cross-checked

Every catalogue entry is content-fingerprinted, and new blocks seal together with their attacks in the same change — the testing discipline is practised, not aspirational. The five gates run today, including the unit gate that catches the Mars Climate Orbiter class of error. The storage layer re-derives fingerprints on write and on read and refuses mismatches. Blocks are built and verified by separate sessions: the producer never reviews their own work.

Not finished — and it says so. Several architecture extensions are designed but not deployed, each queued for its own patent filing: cross-organisation sharing of verified block libraries, hardware-vouched input where software touches the world, bringing the full compiler chain inside the evidence discipline, and a memory-and-parallelism architecture in which whole failure classes have nothing to act on. Like every system today, BriX currently runs on standard external runtimes that remain a conventional trusted base; retiring that base is on the roadmap. The trust spine — fingerprints, gates, sealing, attack-paired admission, storage enforcement — is the part that is real first.

Patent pending.

Who this is for

Where “probably fine” is not a certification basis

Defence and critical national infrastructure
Provable custody chains from sensor to command. Certification by chain-verification rather than test-sampling. A defensible answer to “can we let AI write mission software?”
Medical devices
Every input mapped to a defined fate — the discipline infusion pumps and radiotherapy controllers have historically lacked. Weakest-link inheritance stops a reviewed shell hiding an unreviewed part.
Finance
Deployment attestation — the Knight Capital answer. Unit gates for gross-vs-net, currency, and timezone confusions. And verified computation designed to reproduce the same fingerprinted result across different hardware.
Distributed and federated AI
Fingerprint comparison before co-operation — “are we running the same verified software?” answered before any payload flows. An assembly regime under which AI coding is governable instead of banned or blindly trusted.

In the lab

Evidential discipline, applied to software itself

The lab’s three layers make AI claims auditable: no claim without a source, no result without a condition that could kill it. BriX applies the same discipline to software construction: no block without evidence, no connection without a gate, no artifact without provenance.

Written enquiries only: curious@lily-labs.co.uk

Request a briefing