Blog
Design patterns, formal methods, and the computer science theory behind our tools. We ground agentic software engineering with scaffolding from CS theory to create more reliable and deterministic outputs.
Building Agent Tools for Locked-Down Environments
We built our tools as Claude Code plugins, then tried to run them on a locked-down work laptop. Much AI-assisted work happens on machines that will not install one. Here is how we adapted.
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.
Building L1 Tools for L4 Agents
When agents need a visual interface, the most important design decision is where to draw the boundary between deterministic rendering and agentic composition.
The Verification Gap
As code moves from deterministic to agentic, the gap between what we can specify and what we can verify widens at every level. Five levels of code, five verification paradigms, and the case for formal methods in an agentic world.
AI Coding + Grounding and Formal Methods = Agentic Software Engineering
Formal specifications improve code reliability, but the cost of writing them kept them out of most projects. AI removes the time penalty. We're testing whether the payoff is as significant as we think.
Composable Tools: Integration Without Coupling
Our tools discover and enrich each other through filesystem conventions and shell hooks. Six integration layers, from sentinel checks to agent orchestration, with no shared code required for the first four.
The Accountability Gap
When a human writes code, someone is accountable. When an LLM writes code, the terms of service say nobody is. Verification was always important. Now it is load-bearing.
The Six Problems of Agentic Engineering
When engineering teams adopt AI agents, six distinct coordination problems emerge. Each operates at a different layer and timescale. No single tool solves all six, and that is healthy.
Choosing the Right Projection
The library-vs-service debate is old. What's new is that agents, apps, and humans all need to reach the same capability. Here's how we decide which integration point to use when.
Universal Access to Capability
We tried building every tool as a Python library with thin projection layers: CLI, MCP, and REST from one codebase. Here's what we learned.
Design Decision Logs When AI Is Your Co-Author
AI assistants re-propose rejected approaches because context is ephemeral. Design decision logs, adapted from Michael Nygard's ADRs, are one way to solve this while the ecosystem builds better solutions.