Portfolio · Track 3 · Fundamental theory · Generative security
Foundations for AI-Native Proof Systems
Alessandro Chiesa · EPFL
Scaling Trust Creatorsubject to contract
This project will investigate whether the recurring structure of AI computations can support more efficient proofs than generic circuit-based approaches. It also explores self-proving models, and the boundary between computations that can remain black-box and those that must be decomposed for verification.
Outputs
Repositories, papers, and demos will be linked here as the work gets underway.
Where it sits in the portfolio
Arena partners
Environment & challenge design
Physical build & operations
Security & red teaming
Community partners
Industry partners
Digital partners
Open-source practice, use cases
Digital stack
Agents · agentic loop
Agents · new models
Agents · negotiation
Tools · TEE sandbox, auditing
Integration
Glues the stack together
Physical stack
Physical verification · bridges, sensors, actuators
Physical environments · evals, benchmarks, harness
Cyber-physical partners
Real-world data and environments
Theory of secure agent interaction
Generative security
Formal AI security
Secure agent interaction
Cyber-physical bridges
Physical verification theory
Secure hardware
Nature cryptography
Physical environments · evals, world models
An agentic security stack that turns task requirements into formal specifications, then selects or generates suitable cryptographic protocols and verifies them.
Builds the environment, scenarios, and mechanics agents are tested in.
Whether the recurring structure of AI computations can support more efficient proofs than generic circuit-based approaches, including self-proving models.
Cryptographic privacy techniques for AI workloads, such as private retrieval for RAG, so agents can use shared memory and sensitive data without exposing it.
Designs and operates the physical side of the Arena.
An automated mechanism and protocol design engine: agents specify the properties they need, and Dovetail designs a protocol proven in Lean to deliver them.
Sets the Arena’s security criteria and operating model, then red-teams it.
Tests how AI agents negotiate, procure, bid and cooperate under adversarial pressure, and hardens them against manipulation and leakage.
An agentic system for auditing cryptographic protocols and recovering their specifications, with a benchmark corpus to evaluate it.
Lets mutually untrusting agents prove facts about the companies they represent, and their physical-world processes, to each other. CCTI is also the programme’s integration partner.
Watermarks embedded in robot motion, so independent parties can verify which control policy is driving a robot using commodity cameras.
Grounds the programme in real production environments, providing real-world manufacturing data for other teams to design and evaluate cyber-physical trust tools.