In Code They Act, In Proof We Trust
Erik Meijer
- When
- Tuesday, June 304:50 PM – 5:10 PM · 20 min
- Where
- Main StageSan Francisco, CA · imported from ai.engineer's public schedule feed
About this session
AI agents today execute on blind trust, and the failure modes are already in the headlines: a dealership chatbot agreeing to sell a $76,000 Chevy Tahoe for $1, a coding agent wiping a production database during a code freeze, an "agent skill" quietly installing a keylogger on a developer's machine. These are not edge cases. They are the predictable consequence of allowing agents to act without any mechanical guarantee of correctness or safety. Execution is irreversible. You cannot unsend a message, unwire a payment, or un-delete a database. In that regime, permitting an unsafe action costs far more than withholding a safe one, and thus the economically rational choice is to refuse to let agents act on unchecked intent alone. Automind is an agent harness that enforces this discipline by construction. Before any action runs, the agent must submit its execution plan together with a machine-checkable proof of safety and correctness, written in Universalis, a literate logic programming language designed to be read by humans and verified by machines. A small, auditable checker decides whether the plan is allowed to execute. By left-shifting the trust boundary, we no longer have to trust the agent's proposal, or even its proof; only the checker. Policy compliance becomes a static property, established before the first side effect. We can finally demand formal proofs, not vibes, from the agents we deploy.
Speaker
Research Scholar, Leibniz Labs
Erik Meijer has spent more than three decades designing programming languages and developer tools that help humans express intent more clearly to machines. His work has influenced languages and technologies including Haskell, Mondrian, Cω, C#, Visual Basic, Dart, Hack, LINQ, and Rx. Today, he is building Universalis, the world's first programming language for AI agents. By combining formal verification with large language models, Universalis aims to make agentic systems safe, transparent, and trustworthy enough for real-world knowledge work.
More in Harness Engineering
- The 2026 State of AI EngineeringThursday, July 2 · 9:00 AM – 9:20 AM · Main Stage
- The Unreasonable Effectiveness of Separating the Task from the ModelThursday, July 2 · 9:40 AM – 10:00 AM · Main Stage
- How Anthropic Builds: Lessons from LabsThursday, July 2 · 10:00 AM – 10:20 AM · Main Stage
- Tokens Should Have JobsThursday, July 2 · 10:45 AM – 11:05 AM · Main Stage
- Harness Engineering: Building the Production Cage for Powerful Domain AgentsThursday, July 2 · 12:05 PM – 12:25 PM · Main Stage
For developers: this programme is open data — JSON, iCal, schedule XML and an MCP endpoint.Show endpointsHide
- JSONEvery published session and speaker, in one request./aie-worldsfair-2026-import/feed.json
- iCalSubscribe in Google, Apple or Outlook Calendar./aie-worldsfair-2026-import/feed.ics
- Schedule XMLfrab / pentabarf — the format conference apps import./aie-worldsfair-2026-import/feed.xml
- MCP + RESTPoint Claude at the programme. OpenAPI 3.1 included./agents
No key, no signup, CORS open. Everything here is generated from the same data the organisers edit.