Kodamai exits stealth with 'provably correct' AI agent platform
Saudi Arabia's First Mills deploys world’s first verified agentic AI platform
#SaudiArabia #AIAgents — AI infrastructure startup Kodamai has launched the world’s first enterprise AI agent platform built on mathematical first principles, emerging from stealth simultaneously in the UK and Saudi Arabia. Founded by Algerian-born physicist and serial entrepreneur Dr Maha Achour, Kodamai uses Category Theory, Type Theory and Neuro-Symbolic AI to produce agents whose every action is mathematically verified before execution and fully auditable after the fact. Saudi Arabia’s market-leading flour milling company First Mills (Tadawul:2283) has been named as its first enterprise customer.
SO WHAT? — The world’s largest software companies have rushed to build enterprise AI agent and agentic automation platforms to meet surging demand from regulated, mission-critical workflows. Kodamai’s brings a novel approach using mathematical verification to prove the validity of every AI agent. Existing enterprise platforms tend to deploy AI agents with plausible, not provable validity. Furthermore, Kodamai promises to replace layers of manual workflow oversight in live enterprise environments. If the platform delivers what it claims, it could close the trust gap that has kept autonomous AI agents out of mission-critical operations in regulated industries such as food production, financial services, healthcare and energy.
Here are some key facts and detail about Kodamai:
Kodamai has launched the Kelvingrove platform, the world’s first enterprise AI agent system built on Category Theory, Type Theory and Neuro-Symbolic AI. Every agent action is mathematically verified before execution, making outputs provably correct rather than statistically probable.
The platform separates natural language understanding from deterministic execution, meaning that LLM outputs are validated against formally typed interfaces before they are allowed to propagate through the agent network. Errors cannot silently pass from one agent to another.
First Mills, Saudi Arabia’s largest flour producer by market share, is deploying Kelvingrove across all four of its production facilities. First Mills is recognised as a cornerstone of the Kingdom’s food security ecosystem, adding strategic weight to the commercial announcement.
According to Kodamai, First Mills is the first deployment of mathematically verified AI agent infrastructure at this scale anywhere in Saudi Arabia.
The deployment targets supply chain coordination, quality control and demand forecasting, operational areas where thousands of decisions are made daily and where errors carry direct financial and food security consequences.
Kodamai’s platform is compatible with any LLM and any enterprise system, positioning it as an operating layer that sits above existing AI tools rather than replacing them.
The Kelvingrove platform is built on three interlocking mathematical disciplines:
Category Theory structures every agent, workflow and system relationship formally.
Type Theory gives each agent a verified interface contract.
Neuro-Symbolic AI ensures LLM outputs are governed before they act.
Kotamai founder and CEO Dr Maha Achour previously founded Metawave in 2017, a company specialising in advanced wireless communication and radar technologies.
Kodamai targets regulated industries where AI errors carry significant consequences, including manufacturing, financial services, healthcare, energy and logistics: sectors where regulatory-grade explainability and full auditability are operational requirements, not optional features.
ZOOM OUT — Kodamai's platform draws on decades of foundational mathematics that most enterprise technology companies have never touched. Category Theory, originally developed as an abstract language for mathematics itself, provides the compositional structure that governs how agents relate and interact. Type Theory gives every agent a machine-checkable interface contract, drawing on research that produced formal verification systems such as Coq, Lean and Agda. The combination creates what mathematicians call correctness by construction: a system that cannot be deployed unless its correctness has been formally proven. So, this is not a software engineering claim: it is a mathematical one.
[Written and edited with the assistance of AI]
Read more about agentic AI:
GSMA & Khalifa University test AI telecom agents (Middle East AI News)
GSMA whitepaper sets out role for agentic AI in 6G (Middle East AI News)
Cisco: 60% of Saudi firms aware of AI security threats (Middle East AI News)
Salesforce launches Agentforce AI agents in Arabic (Middle East AI News)