We're a research group based in Glasgow focusing on applying category theory to AI verification. Our tools are dependently typed theories, theorem provers, and whiteboards.