Legal Engine builds AI systems that law firms trust with their most confidential work. This page describes the engineering standard we work to. Not an aspiration, not a direction of travel: the level at which the team operates.
We are a very small team competing against companies many times our size, and we win on leverage. Formal methods make whole classes of defect impossible rather than merely unlikely. Enforcement mechanisms hold our standards without anyone having to remember them. Fleets of AI agents do the volume of the work while humans supply judgement, architecture and approvals. That leverage compounds only if every engineer operates at the top of it.
The following is the floor, assumed of any senior engineer. We state it only so there is no ambiguity that it is necessary and nowhere near sufficient. Working through a single seam rather than scattering a concern across the codebase. Scoping least-privilege and tenant isolation from the first line, seeing the second customer's blast radius before it exists. Assuming crashes, retries and concurrency by default, so operations are idempotent (safe to repeat without changing the result) and durable. Holding a clear line between "it works" and "it is proven for this named customer." Operating in the open with review gates and an evidenced audit trail. Making a rule hold with a mechanism rather than a memory. Distrusting the surface, including your own, because a thousand green tests over one untested critical boundary is worse than none.
We evaluate work by V = ∫0T [u(t) − c(t)/α] e−rt dt, where c is the human maintenance cost an asset imposes and α is the fraction of a maintainer's time we are willing to spend servicing it. At our calibration this puts a 250× shadow price on maintenance time: an asset must return two hundred and fifty units of value for every unit of ongoing cost, or we do not build it. The operational test is the walk-away test: if the person who built this vanished for two months, would it still deliver value with zero attention from anyone?
The consequence is severe and we mean it. Unavoidable cost alone (vendor drift, CVEs, OS upgrades) already exceeds the whole maintenance allowance, so the budget for preventable error is negative. Systematic error must be driven to approximately zero, and the unavoidable kind driven down by mechanism: auto-renewing certificates, automated dependency upgrades, self-healing pipelines, runtime drift detection. "I'll maintain it" is not a mechanism.
Natural language admits multiple interpretations; interpretations diverge as they propagate; the cost of ambiguity compounds while the cost of formalisation is paid once. So for our hardest logic we write Lean 4 and let the kernel check it. The agent platform at the core of our next generation of products carries machine-checked safety theorems: that no action can cross a tenant boundary, that authority cannot escalate, that egress is gated, that injected content is treated as data and never as instruction. These are proved, not asserted, with zero sorry, and the proof gate blocks the deploy. We formalise customer requirements the same way, so a specification is something a kernel can check rather than something a meeting can reinterpret.
We hold a hard line against verification theatre. Three failure modes survive a green build: a proposition that is trivially true, a claim holed with sorry, and, most dangerous of all, a wrong predicate that compiles perfectly. Automated gates reject the first two. Only human discipline catches the third.
Which is the honest limit, and we state it plainly rather than sell past it: a kernel checks code against a specification a human wrote. It never checks that the specification encodes what was actually wanted. Formal methods relocate judgement, from "is this code correct" to "is this predicate right", and that relocation is real, valuable and finite. Human judgement does not vanish; it shrinks and stabilises.
Requirements are structured data, not prose, and the specification is modelled so a proof kernel acts as an impartial examiner. The point is sharper than "tests catch regressions": when a one-line change falsifies a rule written long ago by someone now gone, not merely leaves it unproved, the kernel refuses to certify the build and tells you in seconds, rather than a quarter later in an incident review. A contradiction between two requirements is a compile error, not an agenda item.
We also detect false precision. When an input is genuinely vague, emitting a crisp answer about it is worse than refusing. A system that cannot mark its own formalisation boundary, here is what I proved, here is where human judgement must enter, is not trustworthy no matter how confident it sounds.
We build enforcement gates: deterministic checks wired into the commit path, the CI run and the agent's own tool calls, that block the unsafe action and return a didactic explanation of what fired, why the rule exists, what to do instead, and how to override it deliberately. These gates speak to the AI agents as much as to the humans, so an agent reaching for the wrong pattern is corrected inside the loop.
The discipline is borrowed from the Toyota Production System and we mean it literally. Jidoka: stop the line the instant a defect appears. Kaizen: every defect becomes a permanent change to the process, so the class of error is closed rather than the instance. And no temporary countermeasures, because the gravest failure mode is the workaround that quietly becomes the architecture.
Coding agents have collapsed the cost of emission, producing a diff, from hours to seconds. They have not collapsed the cost of verification, understanding a diff, by anything like the same factor. That asymmetry, not compute and not model quality, is what binds. The binding constraint is human attention, and it follows that the most expensive thing an agent can do is consume the human it was meant to free.
The way out is to close the loop. Continuous Enforcement makes mistakes non-committable rather than discouraged. Continuous Verification makes "done" computable against a specification rather than self-declared. Once that loop is closed the economics invert: a small, inexpensive model inside a tight loop, proposing, taking a hard verdict, and revising, converges on a verified target that a frontier model asked once, with no comparator, only approximates with great confidence. The non-negotiable structural property is that the comparator must be independent of the actuator. A self-grading agent is not a verified one.
Our internal capabilities are expressed as structured, schema-valid data rather than prose, so they can be searched, composed and validated programmatically by the agents that use them. Every boundary is typed and validated. Every fact carries its provenance: where it came from, when it was true, when we last checked. And we enforce a wall between what is proved and what is merely suggested: statistical signals may propose, only verified facts may be premises. That separation is not a convention we try to honour, it is a property we prove.
Our systems are agentic and act on privileged legal data, so the question is never only "is this code correct" but "what is the closure of what this thing can do, and does it intersect what it must never do." Two agents that are each individually safe can be jointly unsafe through emergent dependency. Containment is an architectural property you prove, not a behaviour you hope for. Power without containment is the risk; containment is the moat.
Nothing in the codebase is correct because it is there. Existing code, config, schema, infra and prior decisions are claims to be tested, not givens to inherit. Names are not evidence: we audit what a thing actually permits, never what it is called. The discipline is refute-first. We do not say "kernel-verified" without having run the kernel, and we do not quote a number we cannot source. A criterion counts as verified only if you can also exhibit an input on which it comes out false. A check that passes everything you feed it is not a check; it is a mirror.
Every term, metric and category must cover everything it should and exclude everything it should not, without a paragraph of carve-outs afterwards. If you find yourself writing "X does not include Y or Z," the term is wrong. Readers integrate the noun and skip the qualifier, and a vague name propagates its vagueness into every system that consumes it.
The problems here do not stay inside the editor. Formalising a statute requires reading the statute. Pricing a mechanism requires real mechanism design rather than intuition. Advising a customer requires knowing what you would and would not yet promise them. Our engineers move between a proof, a contract clause, a customer call and a deployment without changing gear, because these are the same problem with the ambiguity dressed differently.
We work these ideas through in the open. They are not background reading; they are the standard itself, written out.
If this is how you want to build, talk to us.