Research
Research papers.
Working papers and field reports on the execution boundary for AI agents: policy evaluation, receipts, approval control, formal proof, and adoption pressure in regulated organisations. Formal-methods papers do not verify the Go implementation line by line.
- Papers
- 11
- Backed
- 6
- Categories
- 6
A bounded TLA+ model of fail-closed AI execution
We present the current HELM OSS TLA+ model for a six-gate guardian pipeline and the TLC model-checking result for four safety invariants: fail-closed behavior, default deny, unanimity before allow, and freeze override. The model is intentionally bounded and does not claim full proof of the production implementation. It is a repo-backed working paper about what is modeled, what was checked, and what remains outside the proof boundary.
All papers
Cryptography / Formal methods / Operations / Protocol / Research / Systems
A bounded TLA+ model of fail-closed AI execution
We present the current HELM OSS TLA+ model for a six-gate guardian pipeline and the TLC model-checking result for four safety invariants: fail-closed behavior, default deny, unanimity before allow, and freeze override. The model is intentionally bounded and does not claim full proof of the production implementation. It is a repo-backed working paper about what is modeled, what was checked, and what remains outside the proof boundary.
European Union AI Adoption: The Continent Built the Rulebook and Forgot the Stack
The European Union spent five years writing the world's most detailed AI rulebook and is now discovering that nobody on the continent owns the layer the rulebook depends on. This piece maps the gap between regulatory ambition and deployment infrastructure, separates training- data disputes from agent runtime authority, and shows where guarded execution layers could repair the policy without enlarging it.
France AI Adoption: Sovereign Capital, Cultural Defence, and the Boundary Nobody in Paris Has Costed
In February 2025 President Macron announced 109 billion euros of AI investment at the Grand Palais and made France the only European country with a credible answer to Stargate. The capital is real. The deployment substrate beneath it is not. This piece maps French AI adoption, separates training-data disputes from agent runtime authority, and shows where the missing layer would convert sovereign compute into governable enterprise systems.
Germany AI Adoption: The Industrial Engineer's Country, Without an Industrial Boundary
Germany has the deepest applied-engineering culture in Europe, the largest industrial base on the continent, the strongest Mittelstand procurement discipline anywhere, and almost no published specification for how an autonomous AI agent should be governed inside a regulated manufacturing environment. This piece maps German AI adoption, separates training-data disputes from agent runtime authority, and shows where the missing layer would convert engineering rigour into governable enterprise systems.
United Kingdom AI Adoption: From Safety Institute to Security Institute, Without the Substrate Between
In February 2025 the United Kingdom renamed its AI Safety Institute the AI Security Institute, pivoted from abstract harm to chemical, biological, cyber, and fraud threats, then paused the country's largest planned compute build the next year. This piece maps the British AI deployment reality, separates training-data lawsuits from agent runtime authority, and shows where the substrate beneath the rebrand still has not been built.
United States AI Adoption: The Gap Between Hollywood Lawsuits and Enterprise Reality
The United States leads the world in AI commercialisation and treats enterprise AI risk through the lens of Hollywood lawsuits and abstract safety theatre. This piece maps the actual deployment pattern, separates surface fears from operational risk, and shows where guarded execution layers unlock the productivity gain that copyright disputes and compliance theatre cannot reach.
The execution receipt
An execution receipt is a portable record that a proposed agent action was evaluated before it touched the world. This paper specifies the receipt's role, minimum fields, hash binding, signature envelope, and offline verification path for governed AI tool calls.
Why deny rate is the wrong metric
Raw deny rate is an attractive dashboard number for AI execution boundaries, but it is a poor measure of safety. This paper proposes a metrics model centered on replayability, false-allow discovery, escalation latency, policy coverage, and receipt verification.
Approval signatures for autonomous transactions
Human approval is often implemented as a chat confirmation or dashboard click. For high-risk AI actions, approval needs stronger semantics: signed intent, scoped authority, key rotation, replay safety, and evidence that the approval matched the action finally dispatched.
Freshness controls for AI execution policies
Policy freshness is a runtime safety property for AI agents. This paper defines stale-policy failure modes, freshness windows, receipt evidence, and fail-closed controls for execution boundaries that evaluate tool calls before side effects.
Execution boundaries, not general-purpose agent frameworks
General-purpose agent frameworks improve orchestration, memory, and tool routing, but they do not by themselves create an auditable authority layer. This paper argues that production agent systems need a separate execution boundary: a deterministic policy and evidence plane that evaluates every consequential action before dispatch.