GLAIVe
We’re a non-profit limited company focusing on applying category theory to AI verification. Our tools are dependently typed theories, theorem provers, and whiteboards. People Seminar
Glaive Research Research Glaive is a research group building software infrastructure based on the theory of containers. We pursue three research programmes in this area: typed tactics for interactive theorem proving, structured architectures for machine learning, and Polylang, a programming language we're designing from the ground up. This area of research sits at the intersection of category theory, dependent type theory and programming languages, and has proven to be both remarkably expressive in encoding structure across all of these fields, and concrete enough to actually build software wi
Explore this link on the map →related reading
- Categories for AIcats.for.ai
- Tracing the thoughts of a large language model \ Anthropicanthropic.com
- Lean (proof assistant) - Wikipediaen.wikipedia.org
- 2510.01346arxiv.org
- "Why don't you use dependent types?"lawrencecpaulson.github.io
- Type theory - Wikipediaen.wikipedia.org
- GitHub - bgavran/Category_Theory_Machine_Learning: List of papers studying machine learning through the lens of category theory · GitHubgithub.com
- When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
- lf-lean: The frontier of verified software engineering | Theoremtheorem.dev
- Neural Networks, Types, and Functional Programming -- colah's blogcolah.github.io
- computational trilogy in nLabncatlab.org
- [2602.22631] TorchLean: Formalizing Neural Networks in Leanarxiv.org