Ax·01
Proof over promise.
If a safety property matters, a machine should check it — every run, every time. We build systems whose good behaviour is demonstrated: replayable, auditable, provable.
Lorena Labs · London · MMXXVI
A logical
renaissance.
We build mathematical instruments for the age of intelligent machines — systems free to reason, bound by rules we can prove, worthy of the trust a renaissance runs on.
Artificial intelligence may be the most consequential technology humanity has ever built. We believe its benefits are enormous — and that they arrive only if it goes safely.
Lorena takes its name from the logical renaissance — our conviction that the oldest instruments of certainty (logic, mathematics, proof) are how a young technology earns lasting trust. A deployed system shouldn’t merely seem aligned. Within the bounds that matter, its behaviour should be something you can check.
So that is what we build: frameworks where AI reasons freely but acts only through rules made explicit, and development systems that measure — loop by loop — whether software truly got better. Not guardrails bolted on afterwards. Foundations, laid first.
Ax·02
Freedom inside boundaries.
The best systems aren’t the most constrained — they have the clearest limits. Let a model reason without bounds, and let only lawful actions reach the world.
Ax·03
Benefit, broadly shared.
Done well, AI is a renaissance for everyone — not an experiment run on them. Safety isn’t about slowing the future down. It’s about making sure it arrives well.
TarskiVerified agentic backendsA platform for building software on logic programming. Behaviour is written as scenarios, hard limits as invariants, and every effect carries provenance — so you approve a contract and its evidence, never ten thousand generated lines.Stella LoopProduct development, in loopsAn agent-native product development system. Point every human and agent at a shared North Star, run the loop, and see after each pass whether the product actually got better.JacqOSAn operating system for agentsA mathematical boundary between AI reasoning and real-world action. Agents reason freely inside a sealed inner world; only actions that satisfy your rules ever reach outside.
⊨ separate constructions, one theorem — capable systems, lawful actions.
Founded by a mathematician who thinks trust should be earned the old way — by proof.
Founder & Director
Dr Adam Harris
DPhil in Mathematics, University of Oxford — mathematical logic and arithmetic geometry. Previously created JacqOS, Lorena’s founding construction.
Meet the peopleBuilding carefully,
in the open.
Lorena Labs is at the beginning — of the company, and of the renaissance it’s named for. If proofs and products excite you in equal measure, we’d love to hear from you.
Write to us
adam@lorenalabs.com