FIG. 01 - ICARUS AGENT
WING SPAN ≈ 2.4 m
WING SPAN ≈ 2.4 m
42.3601° N · 71.0589° W
ALT. 1,240 m
ALT. 1,240 m
Guardrails don't clip an agent's wings, but teach it to fly.
Verified contracts block bad actions and turn every success and failure into data that makes agents more capable, more efficient, and cheaper to run.
Built by leading researchers in ML/Formal Methods at UIUC/Stanford
§ RESEARCH
Research News
1ST PLACE
AI4Math · ICML 2026
View leaderboard →
Won the AI4Math Lean theorem-proving competition
Our agent took 1st place in the TCS Lean formal-theorem-proving track at the AI4Math Workshop, ICML 2026.
BEST PAPER · H.M.
AI4Math · ICML 2026
Read paper →
SEVerA: Verified Synthesis of Self-Evolving Agents
D. Banerjee*, C. Xu*, G. Singh
Best-paper honourable mention: formally verified contracts wrap every model call, giving 0 constraint violations across every benchmark while outperforming unconstrained baselines.
DEMO
2026
View on GitHub →
Daedalus, our computer-use agent, learns to play Tetris
It composes the task from small verified skills and self-improves its play across runs. Games are a controllable proxy for real-world long-horizon control.
§ TEAM
The team who read the myth as a warning.
We're researchers specializing in formal methods and machine learning. We think safety is top priority, not an afterthought.
Calvin Xu
Co-Founder · CEO
PhD CS @ UIUC. ML × Formal Methods. Ex-MIT Lincoln Lab, Intern @ Meta/TikTok.
Debangshu Banerjee
Co-Founder
PhD CS @ UIUC. ML × Formal Methods. Ex-Google, Intern @ Amazon/Google.
Tarun Suresh
Co-Founder
PhD CS @ Stanford. Agentic self-improvement & efficient LLM inference. Prior: Intern @ Nomic AI, Bloomberg.
Gagandeep Singh
Advisor
Asst. Prof. CS @ UIUC. Formal Methods × ML. PhD @ ETH Zurich. FOCAL Lab sponsored by NSF, Amazon, Google, Qualcomm, Bloomberg, Open Philanthropy.