Agents plan, adapt, and sometimes deceive
Agents don't just follow fixed instructions. They plan, adapt, and when many of them interact they can cooperate or collude. We study what agents really do, and where that goes...
Oracles · Assurance · Safety for Intelligent Systems
Agents are the new software.
Software used to be written line by line by people. Increasingly it is written, and run, by AI agents. OASIS studies them as a new kind of software: how they behave, how to build better ones, and how to know the code they produce is correct.
Evidence, not mirages.
The premise
Code is not correct because an agent wrote it. A system that reports its own success is not evidence of anything.
What we look for instead is something a sceptic could check: a counterexample, a proof, a trace that replays. We build the tools that produce those, and we try hard to break our own.
In a desert, the useful skill is telling water from the appearance of water.
Research
The agents that write the software
The most useful agents are the ones that write code, and stronger coding agents make stronger general-purpose agents. We work on how they plan, how they reuse learned skills, and...
Code is not correct because an agent wrote it
We build tools that check generated code automatically, pairing language models with bounded model checking and symbolic execution so that the verifier, not the model, has the final word on...
News
- Jul 2026 🏆 ACL 2026 Outstanding Paper Award for "Lying with Truths: Open-Channel Multi-Agent Collusion for Belief Manipulation via Generative Montage."
- Jun 2026 Congratulations to Ali Aljaberi, whose paper "AIALIB: A Threat Library for AI-Generated Code" is accepted to the ASE 2026 Tools & Datasets track.
- Jun 2026 Our UGRIP 2026 internship team (Dragos-Gabriel Monea, Yilin Liu, Rishika Mehta) won the Best Project Award for efficient, adaptive and extensible smartphone-native agent runtimes.
- May 2026 M.Sc. student Ali Aljaberi graduated and received the Future Tech Titan Award.
- Jan 2026 Ph.D. student Hamad Alshehhi received the Outstanding TA Award.
Projects
A claim is only as good as the thing that can check it.
AProver
Verification agents for AI-generated code. AProver drives bounded model checkers (CBMC, Kani, JBMC), writing the specifications itself and then triaging every counterexample as real or spurious, so what it reports are confirmed bugs rather than warnings to wade through.
ClawMobile
An agent-first phone. On Android the agent becomes the primary interface: it observes device state, drives apps with permission, and accumulates reusable mobile skills, running either inside the app or on a Termux/OpenClaw runtime.
Join us
We are recruiting PhD students and interns at MBZUAI, across autonomous agents, software engineering, formal methods and security.