AI security, formal verification, and contained agency. Essays by Eduardo Aguilar Pelaez, CTO and Co-founder of Legal Engine.
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. Part three of Building in Steel.
Gunpowder was on sale to everyone; what varied was the capacity to absorb it. On Jeremy Black's reversal of the causal arrow, Maurice of Nassau in the 1590s, Whitworth's screw thread, and why checkability rather than model quality is the axis that favours the countries told they have lost the AI race. Part two of Building in Steel.
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, so past a crossing point you cover less while working harder. Part one of Building in Steel.
Definitions as type-checked Lean code: honesty as a data structure, the Munchhausen trilemma resolved by declared primitives, and word-vector analogies promoted or rejected by a proof kernel.
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 computes its own blast radius instead of being reconciled by hand. The thesis of a three-part series.
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.
Model your requirements in Lean and a one-line change that contradicts a rule written long ago 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.
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 semantic microplastics, the two-reader document, and why law is the sharpest instance.
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. Plus…
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 one architectural principle applied eight ways: autonomous systems must produce machine-checkable evidence of their compliance, not…
Compliance does not only have a workflow problem. It has a semantics problem. A case for OpenCompliance as a shared public proof layer that separates proof, attestation, and judgment.
Law is like holding water with cupped hands. A chaos monkey for statute law bombards formalised legislation with synthetic fact-patterns, revealing where it decides clearly, defers to human judgment, or says nothing at all.
A verified theorem is only as trustworthy as the translation layer that produced it. How factorial design, canonical semantic IRs, and Lean equivalence proofs harden LegalLean against real-world legal language variation.
Applying Lean 4 formalisation to Anthropic's constitution reveals 19 free variables, structural impossibilities in the priority ordering and honesty properties, and the trade-off surface Claude must navigate.
A synthesis of four essays on formal methods, legal reasoning, and AI alignment into a methodology: formalise properties, check mutual satisfiability, design processes for negotiating trade-offs, and measure alignment margin.
Introducing alignment margin: the maximum perturbation a system can absorb before any specified alignment property is violated. A continuous, measurable quantity borrowed from control theory's phase margin.
When outcome properties conflict, shift to process specification. Mechanism design applied to family law and AI alignment, with connections to incomplete contracts and therapeutic culture.
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.
The O-1A visa criteria formalise cleanly in Lean 4: discrete categories, explicit threshold, binary predicates, independence from ordering. The question "does this applicant qualify?" reduces to type checking.
The case for bounded, provably safe AI agents, using the OpenClaw crisis as a case study. When an AI coding assistant with unrestricted system access began autonomously modifying critical infrastructure, it demonstrated why architectural constraints matter more than alignment promises.
The OpenClaw security crisis validates the case for formal capability verification. When an AI tool designed for personal use was deployed in enterprise environments without architectural constraints, the results were predictable.
AI-generated Lean 4 proofs for capability bounds. Demonstrating that formal verification of AI agent capabilities is not just theoretically sound but practically achievable with today's tools.
Formal methods from seL4 and CHERI applied to AI agents. How hardware capability models and microkernel verification techniques can constrain AI agent behaviour at the architectural level.
Google DeepMind's architectural approach to prompt injection. CaMeL treats prompt injection as an architectural problem rather than a training problem, which is exactly the right framing.
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.
Five questions that actually matter when evaluating an AI vendor's security posture. Traditional security questionnaires were designed for a world of deterministic software, not probabilistic AI systems.
Proposing Formal Capability Verification as a complement to alignment. AI alignment research focuses on the soul; we also need to constrain the hands.
Applying verification to legal technology systems. The same formal methods that verify hardware and operating systems can bring provable correctness to legal automation.