What if rigour were fast and free?
AI is writing more of the code. How can teams verify it and be accountable for it? The practices that produce trustworthy software — formal specs, structured requirements, verified transformations — were always effective, just too time-intensive and inaccessible. We’re building open source tools to try to solve that.
What we are building
Decades of computer science and software engineering research — structured product discovery, test driven development, formal methods, and behavior-preserving transformations — have always worked. They were just challenging to apply consistently and time-cost effectively in most commercial settings. We believe that AI makes it feasible to learn and consistently apply these practices even under pressure and constraints. We build across four layers.
What we are reading
All readings →Prediction: AI Will Make Formal Verification Go Mainstream
Kleppmann argues AI removes the human bottleneck from formal verification — the same thesis driving our work, arrived at independently.
martinfowler.comLLMs Bring a New Nature of Abstraction
Fowler argues LLMs create a new kind of abstraction — probabilistic rather than deterministic — and explores what that means for how we build software.
arXiv preprint (2507.13290)Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
Proposes using formal verification to check LLM-generated code against natural language intent — closing the gap between what you asked for and what you got.
What we are learning
All posts →Using Formal Methods on a Concurrency Bug
Two Lux processes could claim one screen slot. The bug survived sixteen rounds of fixes. Here is why a passing test was not enough, and what we did instead.
Using Formal Methods on a Recurring Connection Bug
A connection bug in Biff kept returning after every patch. We modelled it in Z, and the model reproduced it as a deadlock and proved the connection can never get stuck.
Right-Sizing MCP Servers
We built every MCP server the same heavy way, then learned the shape turns on two questions: how heavy and session-agnostic the resource is, and how much per-session context the server itself must carry.