Glaive-Research
We are a non-profit limited company focusing on applying category theory to AI verification. Our tools are dependently typed theories, theorem provers, and whiteboards.
Blog
- Bootstrapping Data Structures From Fixpoints of Containers
- Generalised Tensors in Idris
- Q4 2025 report
- Categorical Pipelines
- Compiler Engineering for Substructural Languages I: The Problem with Polymorphism
- What Kind of Free Category is the Controllability Matrix?
- Generalized Transformers from Applicative Functors
- Programming Pipelines Using Dependent Types
- Building a Neural Network from First Principles using Free Categories and Para(Optic)
- How to Stay Locally Safe in a Global World