Eduardo Aguilar Pelaez
CTO & Co-founder at Legal Engine
Building AI systems that transform how legal professionals work
PhD & MBA, Imperial College London
About
I'm a technical founder who bridges deep engineering research with business strategy and product thinking in AI for professional services.
As CTO and Co-founder of Legal Engine, I lead the development of AI-powered voice agents that help law firms handle client intake, matter routing, and legal directory submissions. We're building technology that lets lawyers focus on legal work instead of administrative overhead.
My career spans research to production: a PhD in wearable medical devices at Imperial College London, where my work on acoustic breathing monitors was commercialised and is now CE-marked for clinical use. I've held executive roles at companies reaching millions of users, reported directly to the CEO at Canonical (Ubuntu), and served as a voting member of the Cloud Native Computing Foundation.
I've published 11 peer-reviewed papers with 186+ citations, hold 2 patents, and have been featured in Forbes and WIRED. I've spent 18+ years as a reviewer for IEEE conferences and served on grant selection committees for Cancer Research UK.
I believe in building products that actually ship and solve real problems. No buzzwords, no vaporware - just working software that makes a difference.
Work
Legal Engine
Co-founder & CTO 2023 - PresentBuilding AI voice agents for UK law firms. Our technology handles inbound calls, intelligently routes matters to the right lawyers, and automates legal directory submissions.
- Launched AI voice agents processing calls for Top 100 UK law firms
- Built ElevenLabs voice AI integration with enterprise-grade security
- Developed proprietary Composable Skill Compiler for deterministic AI workflows
- Scaled from concept to live production with paying enterprise customers
Converge
Head of Product & Reality Capture Engineering 2021 - 2023Led product strategy and engineering for construction technology startup. Developed PrecastDNA tracking system using radio signal trilateration.
- Generated £500k+ revenue from material tracking technology
- Secured major distribution partnership with Fortune 500 company
- Led to patent application for novel tracking methodology
Direct report to founder/CEO. Led strategy for AI, cloud applications, and high-performance computing pillars serving 40M+ users globally.
- Primary voting member at Cloud Native Computing Foundation (CNCF)
- Managed partnerships with NVIDIA, AMD, Intel, and major automotive OEMs
- Contributor to Kubeflow ML workflow platform
Executive leadership at the UK's largest patient engagement platform, integrated with over 50% of GP health records.
- Platform serving 12M+ active users
- Managed product, data, design, and operations teams
- Critical national healthcare infrastructure
Led technology development for healthcare innovation centre. Built medical devices and ran clinical trials.
Three-year progression from IoT Engineer to General Manager, leading the Sherlock keyless entry system for luxury hospitality.
- Designed and built Sherlock keyless entry system (later spun out as Klevio)
- Led mobile and eCommerce products achieving +87% checkout conversion
- Delivered 4x faster mobile single-page application
- Managed global IT infrastructure through Accor acquisition
Ervitech (Imperial College Spin-out)
Co-founder & Principal Engineer 2010 - 2011Commercialised PhD research into wearable breathing monitors. Technology later incorporated into CE-marked medical devices for sleep apnea diagnosis.
Selected for the competitive CERN Summer Student Programme (24% acceptance rate). Worked on electronics and FPGA programming for the ATLAS Beam Condition Monitor, contributing to the infrastructure used in the 2012 Higgs boson discovery.
Mars Rover research placement at the Laboratory of Robotics and Planetary Exploration (CAB-CSIC-INTA) in association with NASA. Designed FPGA-based control systems for ultrasonic instrumentation.
Recognition & Expertise
Awards
- IET Innovation Award Winner (2009) - Information Technology category for wearable breathing monitor. Also finalist in three additional categories.
- Royal Academy of Engineering Travel Grant (2007) - Competitive research collaboration grant.
Patents
- Wearable Breathing Monitor (EP2593007B1) - Novel acoustic sensor and signal processing for respiratory monitoring. 16 citations.
- Material Tracking System (WO2024152019A1) - Radio signal trilateration for construction logistics.
Industry Leadership
- CNCF Voting Member (2019-2020) - Strategic decision-making for Kubernetes ecosystem, representing Canonical.
- IEEE Conference Reviewer - 18+ years reviewing for EMBC and ISCAS conferences.
- Cancer Research UK - Technical evaluator for Pioneer Award grants (£200k breakthrough research funding).
- IET Innovation Awards - Judge on national engineering award panel.
Education
- MBA - Imperial College Business School (2017-2019)
- PhD, Electrical & Electronic Engineering - Imperial College London (2006-2010). Wearable medical devices and signal processing.
- MEng, Electrical & Electronic Engineering - Imperial College London (2002-2006)
AI & Voice Technology
Building production AI systems with ElevenLabs, deploying voice agents at enterprise scale, and implementing responsible AI in regulated industries.
Cloud-Native Infrastructure
Kubernetes, GCP, workflow automation. CNCF voting member with deep expertise in scalable distributed systems.
Medical Devices
From PhD research to CE-marked products. Signal processing, wearable sensors, and clinical trials.
Product Leadership
Executive roles at scale: 12M+ users at Patient Access, Fortune 500 partnerships, direct report to founder/CEOs.
Writing & Media
Featured In
I write about building AI products, legal technology, and lessons from the startup journey. Follow me on LinkedIn for updates, or see my Google Scholar profile for academic work.
Blog
Longer-form thinking on AI, technology, and building products.
The Research Agenda
Seven open topics, every claim tagged with the kind of evidence behind it, and for each topic the result that would close it. Most of them have people working on them. What is missing is the connection.
2 November 2026The Predictions Ledger
Fifty-six dated bets, how to score them, and why most of them cannot show that the author knows anything. Nobody has agreed to do the scoring.
2 November 2026Who Pays to Keep It True?
A theorem stays proved when the money stops. An encoded statute keeps answering, and goes wrong. Mathlib shows how a formal library is kept. It cannot show who should pay when somebody else holds the clock.
2 November 2026The Last Person Who Knows How
A review step is a control only if the reviewer can still reject. That ability can wear out, or never form, while the sign-off log looks the same. This chapter is normative, contains no theorem of its own, and says why.
2 November 2026A Proof Is Not an Appeal
England and Wales presume a computer was working unless someone shows otherwise. Checkable evidence could earn that presumption honestly. It would still leave a person harmed by the rule with nothing useful to say about the run.
2 November 2026A Trace Is Not a Replay
In March I treated as one thing what are at least three different guarantees, and never said whether a fourth was available or needed. None implies another, temperature zero does not deliver the fourth, and a theorem of mine named for tamper evidence says nothing about tampering.
2 November 2026A Summary Is Not a Permission
An agent's memory holds a copy of what it may do, written by a model, under pressure to be short. That copy can widen the grant with no attacker in the room. A shorter record can permit more, and no check that reads only the memory can catch it.
2 November 2026Yesterday's Permission
A proof does not go stale. Everything that relied on it can. Revocation is a race with a measurable window, and a system that cannot state the length of that window, or list what the withdrawn fact has already produced, does not have revocation. It has a button.
2 November 2026Who Proves the Agent Is Yours?
Every hand-off in a delegation chain may only narrow. That rule is correct, old and easy to prove. It bounds every agent by the root, it does not stop an agent being talked into using its own authority for someone else, and it cannot say whose root it is.
2 November 2026Every Query Was Allowed
Permission is decided one question at a time. Knowledge accumulates across questions. Database researchers showed the gap in the 1970s, and agents wired into a law firm's systems inherit it, with a privileged fact at stake.
2 November 2026Perfect Compliance, Defeated Purpose
In August I wrote that a firm which games a safe harbour buys a burden shift and nothing more. The burden shift is what it came to buy. A witness in Lean, five corrections to my own essay, and a presumption that expires.
2 November 2026Disclosure Without a Predicate
From 10 December 2026, Australian privacy policies must disclose certain automated decisions. A machine can check some of that. It cannot check it by reading the policy, and the regulator's own model text fails the most literal check you could write.
2 November 2026The Translator Writes the Rule
Two defensible translations of one sentence can both compile, both run and both pass every check for conflicts and gaps. Whoever picks between them has made the rule, and the Catala team said so before I did.
2 November 2026Never Breaks a Rule, Never Finishes
Every prohibition of an act is satisfied by doing nothing. A limitation date is not, but the check that watches it fires only after the matter is already lost. What the agent owes is a handover while a human can still act, and that promise has its own way of being empty.
2 November 2026The Proof Passed. The Wrong Thing Ran.
A theorem about a model says nothing about what ran until every link between them has been discharged. Several of those links cannot be stated in the logic the theorem lives in, and the defect evidence I could find puts the failures at the links.
31 October 2026Lean-Ready English, in Lean-Ready English
A companion to Lean-Ready English written only in sentences the LangLib parser accepts, now with a narrative thread: connectives that never change a sentence's meaning, named referents, and a checked link graph. Each sentence shows its Lean meaning.
31 October 2026Lean-Ready English
A controlled English where every accepted sentence has one declared meaning in Lean, and LangLib, a library of the constructions that carry those meanings. The first slice compiles, proves round-trip fidelity for every sentence it accepts, decides ten of fourteen real acceptance criteria, and caught a mistake in the wind-tunnel essay. With an audiobook.
30 October 2026Mathematics Went First
Three mathematicians on the Lex Fridman Podcast describe the first field where AI proofs became cheap to produce and to check. What they trusted rested on statements short enough to read, built on a reviewed library, Mathlib, that mathematics already had; the proofs were the cheap part. The parallels with these essays, where the guests are right and the essays were too narrow, and why law will be late, because writing its statement library is an exercise of authority. With an audiobook.
30 October 2026Who Gets to Write the Specification?
Once a specification can be executed, writing it is an exercise of power. Correctness, validity and authority are different properties, and verification supplies only the first and at best the second. Robodebt, the 2020 A-level grades and Colorado's benefits system, a Lean example in which the kernel states exactly where three teams' rules disagree but cannot say which is right, Hart's secondary rules for executable policy, and three falsifiable predictions. With an audiobook.
30 October 2026Refactor the Workflow, Not the Worker
The unit of AI redesign is the dependency structure of a workflow, not the job or the task. Questions can move upstream; approvals cannot merge. Ford's invoiceless accounts payable, a Lean model in which a careless observation makes the dangerous redesign provably equivalent, why an AI belongs at the front asking questions rather than in the middle approving, and three falsifiable predictions. With an audiobook.
30 October 2026The Checking Threshold
DeepMind argues that coordination, not competence, decides when AI transforms the economy. A reply: coordination bundles transmission, which copying a model makes nearly perfect, with correction, which copying makes weak for the honest mistakes a model finds reasonable. On the largest observed agent swarm, DeepMind's own whistleblower experiment, why the threshold will be crossed first where handoffs can be machine-checked, and three predictions. With an audiobook.
30 October 2026Many Hands Make Heavy Work
Parkinson said work expands to fill the time available. It also expands to fill the people available, and then it stops. On the law of many hands: why tasks keep gaining collaborators past the point where the next one helps, why the stall is structural enough to appear in AI agent teams with no psychology at all, and why the fix is to price the addition. With an audiobook.
30 October 2026Floating Theories
A proof can hold every part of an argument together without holding any of it down. On floating theories, the four roots that anchor a claim, the nominal fallacy, why AI and formal verification make unanchored claims cheaper and more persuasive, and what to ask of anything sold as verified. With an audiobook.
28 October 2026Systemic Coping Syndrome
An organisation can become better at accommodating its dysfunction than correcting it. Why the people who would gain most from AI are often the least placed to act on it, why what such organisations lose is the capacity to compound, and how AI can make coping cheaper instead of ending it. With an audiobook.
13 September 2026Nobody Authorised the Combination
The OpenAI/Hugging Face breach and Anthropic's four disclosed incidents traced as capability-union failures: components individually authorised by reasonable people, the combination never checked. Traces the closure explicitly for each case, then says plainly what the Proof-Carrying Coalitions formalism does and does not cover, including a naming collision and a biased-reasoning finding that a capability-closure proof would not have caught.
11 September 2026AI and the US Economy: Move the Parameters Yourself
An interactive version of the Anthropic Institute's 2026 model of AI and the US economy, exposing the three parameters their own explorer holds fixed: how easily capital can be added, how readily work substitutes, and how much AI use leaves the paid economy altogether. Runs entirely in your browser, with a self-test against the paper's published figures.
11 September 2026The Number Anthropic's Economists Left as a Word
The Anthropic Institute's model of AI and the US economy does not say wages fall. They rise in every scenario, including the most extreme. But that conclusion rests on a single parameter, and the threshold below which it reverses is 2.08 against their assumption of 3.0; the paper says the wage falls if capital supply is 'sufficiently small' without saying how small. Plus why the GDP figures may not measure what the debate thinks they measure: work that leaves the market makes people better off and the statistic worse.
9 September 2026Nobody Is Paid to Delete
A corpus of rules written by authors with short tenure grows without bound, because deletion is a dominated strategy for every author and no volume of instruction can make it otherwise: an agent instance is scored within the session and bears none of the cost of what it wrote. The obvious fix, writing a rule that says retire a rule, is strictly counterproductive, since it cannot change behaviour and occupies bytes forever. The conservation law that would work has been tried nationally and abandoned, and my defence of it covers only half the failure. With a Lean 4 formalisation whose theorems are deliberately trivial, and which corrected me once.
16 August 2026Make the Safe Harbour Compile: Regulate the Predicate, Not the Prose
Vague regulation is not light touch. It is a tax collected in delay, and it buys no safety, because a rule too imprecise to check is also too imprecise to enforce at scale. But formalising the law is the wrong fix, since a legal standard's vagueness is a designed capability. Formalise the safe harbour instead: keep the standard, and make machine-checkable the thing you do to earn a presumption of compliance. EU AI Act Article 40 already provides the slot, and it is currently being spent on more prose. Part three of Building in Steel.
15 August 2026The Gun Did Not Win: Absorption, Not the Tool
Gunpowder was on sale to everyone; what varied was the capacity to absorb it. Maurice of Nassau's answer in the 1590s was drill, standardised calibre, a military academy and regular pay, and not one item on that list is a weapon. On Jeremy Black's reversal of the causal arrow, Whitworth's screw thread, the Model Context Protocol dropping its handshake, and why checkability rather than model quality is the axis that favours the countries currently being told they have lost the AI race. Part two of Building in Steel.
14 August 2026How High Can You Build in Mud?
A mud hut is a good building, and it has no datasheet. Human review is linear in the requirement count while the conflict surface is at least quadratic, and its live subset cannot be identified without doing the analysis, so past a crossing point you cover less while working harder. On why care cannot fix a combinatorial problem, why contradictory axioms leave the build green and every later theorem worthless, and what formal specification actually costs now that generation is cheap. Part one of Building in Steel.
9 July 2026A Dictionary Whose Definitions Compile
Every dictionary you have ever used is circular; a proof assistant makes circularity structurally impossible and forces the honest alternative: a declared primitive basis. A pilot dictionary in Lean 4 where woman = human and female and adult is a compiling definition, the taxonomy is proved rather than asserted, definitional strength is a data structure, and word-vector analogies like hitler minus germany plus italy are promoted or rejected by a kernel-checked verifier instead of trusted.
29 June 2026Verified Specification as Code: From Infrastructure as Code to a Specification the Kernel Checks
Infrastructure as Code took the human out of reconciling servers by hand. The product specification is the last place that loop still runs on memory and meetings. Verified Specification as Code makes the spec a formal, machine-checked artefact, so a one-line change like "let users share notes" computes its own blast radius instead of being reconciled by hand, and the requirements, access rules, and second-order effects are derived from it rather than remembered. The thesis of a three-part series.
29 June 2026Requirements as Data: A Bill of Materials for the Thing You Are Building
Prose is the wrong container for a requirement, and it fails slowly, silently, and totally. Write each requirement as a structured record against a schema, like a bill of materials inspected at goods-in, and a class of late, expensive, personal defects gets caught the moment it enters. The accessible, no-Lean first layer of the Verified Specification as Code series, and the floor the harder layers stand on.
29 June 2026When the Spec Can Contradict Itself: The Proof Kernel as an Examiner That Cannot Be Flattered
Model your requirements in Lean and a one-line change that contradicts a rule written long ago by someone now gone surfaces as a failed build, in seconds, not a quarter later in an incident review. On the proof kernel as an examiner that cannot be flattered, the three ways a green build still lies, the decidability boundary, and the one judgement no kernel can make for you. Layer two of the series.
26 June 2026When the Document Leaves the Factory: Provenance and the Adversarial Check at the Boundary
The companion essay closed the agentic control loop inside the factory. But documents leave the factory, and the comparator cannot cross a boundary you do not control. What can: provenance that travels with the artefact, and a human whose one irreplaceable job is the adversarial check on confident output. On semantic microplastics, how a single fabrication compounds as agents read each other's documents, the two-reader document as the interface between organisations, and why law is the sharpest instance.
26 June 2026Continuous Enforcement and Continuous Verification: Building Software Factories Like Toyota
Toyota cut the cost of the car by fixing the process, not the part. We can do the same for agentic code. An agent is a model in a loop, but a loop that stops when the model declares itself done is an unguided projectile. Continuous Enforcement makes the agent's recurring mistake non-committable; Continuous Verification makes 'done' a kernel checking the spec, not a model feeling finished. The comparator and the stop-cord the loop leaves out, plus why a small model in a tight loop beats a frontier model asked once.
27 March 2026The Agent Tending Problem: Why Your Coding Agents Need an Orchestrator, Not More Agents
Claude Code, Codex, and Gemini all block recursive sub-agent spawning by design. This is correct, but it creates an orchestration gap. The number of agents you can manage is governed by Little's Law applied to human attention. Manufacturing solved this decades ago with machine-tending systems. The AI agent equivalent is an orchestration layer, and the BEAM virtual machine was designed for exactly this class of problem.
26 March 2026Agentic AI and the Verifiable Trace: An Engineer's Response to the Data Protection Question
Simmons and Simmons identified eight data protection risks that agentic AI creates for businesses. This essay asks the engineering question that follows: what would an agentic system need to demonstrate, technically, to satisfy each of those concerns? The answer is a single architectural principle applied eight ways. Autonomous systems must produce machine-checkable evidence of their compliance, not merely assert it.
25 March 2026The Trust Stack: Why AI Concentrates Taste Instead of Distributing It
Every vibe-coder in the world is building on Supabase, not because they chose it, but because the language model did. Andrew Trask argues taste, trust, and rare data survive automation. He is right about the categories but incomplete about the mechanism. AI does not distribute taste to eight billion individuals. It concentrates it into opinionated defaults. The question is not who becomes a tastemaker, but who controls the defaults.
24 March 2026Why Compliance Needs an Open Foundation
Compliance does not only have a workflow problem. It has a semantics problem. This essay argues for OpenCompliance as a public proof layer that separates proof from attestation from judgment, makes trust artifacts more replayable and honest, and helps vendors, customers, and end users alike.
19 March 2026Holding Water With Our Hands: Why Law Needs a Chaos Monkey
Law is like holding water with cupped hands. The intention is good, but cases leak between the fingers. A chaos monkey for statute law, bombarding formalised legislation with synthetic fact-patterns, reveals where the law decides clearly, where it defers to human judgment, and where it says nothing at all. The third essay in the LegalLean series.
18 March 2026Legal Reasoning Needs a Wind Tunnel
A verified theorem is only as trustworthy as the translation layer that produced it. How factorial design, canonical semantic IRs, and Lean 4 equivalence proofs can harden LegalLean against real-world legal language variation. The question is no longer whether a machine can formalise one legal sentence, but whether it can preserve meaning when the legal world says the same thing six different ways.
17 March 2026From Roles to Morphisms: How AI Rewrites the Category of Work
A product manager is not a person. It is a bundle of typed transformations. Category theory gives us the precise language to say what AI changed and why: it applied a functor to the entire category of professional work. The consequences run from role collapse to hom-set universalisation to the emergence of solo founders and agent-entrepreneurs. At every step, the same question recurs: what morphisms can be delegated, and what invariants must humans set?
16 March 2026Elan: Why AI Agents Need an Operating System, Not a Framework
Most AI agent frameworks treat crashes as bugs. Elan, built on the BEAM virtual machine, treats them as facts of life. Introducing a BEAM-native multi-agent runtime with durable state, git-native provenance, and policy-governed tool orchestration, designed for long-running autonomous systems that keep their promises even when machines do not.
16 March 2026LegalLean: When a Computer Says 'You Owe Tax', Can You Check Its Reasoning?
Introducing LegalLean, a framework for verified legal reasoning built on Lean 4 dependent types. 44 machine-verified theorems across US tax law, immigration visa eligibility, and Australian telecommunications regulation. The key insight: encoding where law is deliberately vague as a first-class type, not hiding it.
15 February 2026Type-Checking the Constitution: Formalising Anthropic's Alignment Specification in Lean 4
Anthropic published its constitution for Claude under CC0. This essay takes them up on it: formalising the priority ordering, honesty properties, and principal hierarchy in Lean 4 to identify 19 free variables, structural impossibilities, and the trade-off surface Claude must navigate.
14 February 2026Impossibility Results Are the Thermodynamics Before the Physics
The fifth and synthesis essay in a series on formal methods, legal reasoning, and AI alignment. Tying together formalisation, impossibility results, process specification, and alignment margin into a methodology for reasoning about systems whose desired properties cannot all be satisfied simultaneously.
12 February 2026Alignment Margin: What Control Theory Offers AI Safety
The alignment community is operating without a concept that every control engineer takes for granted: a continuous measure of how far a system is from failure. Alignment margin, borrowed from control theory's phase margin, converts "is this system aligned?" into "how much perturbation can it absorb?"
11 February 2026From Fixed Functions to Negotiation Protocols
If no fixed decision function can satisfy all the fairness properties we want, can we specify the right process for reaching an answer? The shift from outcome specification to process specification dissolves impossibility results, but introduces new questions from mechanism design.
10 February 2026The Judge's Impossible Function: Why Section 25 Cannot Be Formalised
Attempting to formalise English divorce law in Lean 4 reveals an impossibility result: no fixed function can simultaneously guarantee that contributions always matter, that needs are always met, and that identical cases produce identical outcomes. Judicial discretion is the escape valve.
9 February 2026When the Law Is a Type Checker: Formalising O-1 Visa Criteria in Lean 4
The O-1A visa criteria formalise cleanly in Lean 4 because they have a specific structure: discrete categories, explicit threshold, binary predicates, independence from ordering. The question "does this applicant qualify?" reduces to type checking.
6 February 2026Power Without Promiscuity: Why Contained AI Agents Beat Unbounded Ones
OpenClaw proved that unlimited agency is a security nightmare. This essay argues that the distinction that matters for AI agents is not power but containment, drawing on the OpenClaw crisis, Google DeepMind's CaMeL research, and formal verification technologies to make the case for bounded, provably safe AI agents.
1 February 2026When the Hands Run Wild: OpenClaw and the Case for Formal Capability Verification
The OpenClaw security crisis validates the central thesis of "The Soul and the Hands": we've been obsessing over AI values while ignoring AI capabilities. A case study in why alignment alone cannot secure AI agents, with concrete proposals for formal capability verification.
1 February 2026The Soul and the Hands, Part III: Proof of Concept
Empirical evidence from Harmonic's Aristotle theorem prover. I submitted capability theorems to an AI system that generates machine-verified proofs in Lean 4. The results demonstrate that AI can already generate the formal proofs needed for capability verification.
1 February 2026The Soul and the Hands, Part II: From Intuition to Proof
A technical companion exploring how formal methods from operating systems (seL4) and hardware (CHERI) can provide provable capability bounds for AI agents. Includes a Lean 4 sketch and research directions for the intersection of theorem proving and AI safety.
31 January 2026CaMeL and the Future of Prompt Injection Defense
Prompt injection is the SQL injection of the AI era. Google DeepMind's CaMeL architecture represents the most serious attempt yet to address this problem, not through better detection, but through architectural constraints that make certain attacks structurally impossible.
31 January 2026The Energy Pinch Point: Calories, Joules, and the Coming Equilibrium Between Human and Artificial Intelligence
As AI systems consume an ever-larger share of global electricity, the allocation of finite energy resources between sustaining human life and powering computational intelligence becomes a defining challenge. I introduce the concept of the "Energy Pinch Point" and explore its economic, ethical, and societal implications.
30 January 2026Your Security Questionnaire Wasn't Built for AI
The last security questionnaire we received had 247 questions. Question 83 asked about our clean desk policy. Question 84 asked whether we train AI on customer data. Both got equal weight. This is insane. Here are the five questions that actually matter when evaluating an AI vendor's security posture.
27 January 2026The Soul and the Hands: A Third Path for AI Alignment
Dario Amodei and Emmett Shear represent two of the most thoughtful voices in AI safety, and they disagree on almost everything except the stakes. I propose a complementary approach: Formal Capability Verification.
26 January 2026Building Formal Reasoning into Legal Automation: The Case for Convergence
Exploring how formal methods, composable AI skills, and systematic requirements engineering create defensible legal systems. The convergence of these three concepts enables legal teams to build systems that are not just capable, but verifiable.