AI Verified Hardware for AI (AIVHAI)

Introduction

Led by Capabilities Limited, in collaboration with Sigil Logic Inc, lowRISC CIC, Cherified Systems Inc, and Google Research, the AIVHAI project is developing verified, open-source hardware foundations for secure edge AI devices, such as augmented-reality headsets, biometric systems and defence equipment. The team will integrate Google Research’s Coral NPU edge AI accelerator into a CHERI-enabled application-class processor, Capabilities Limited’s CVA6-CHERI, and formally prove that AI models from different, potentially mutually distrusting vendors remain securely isolated from one another, as well as ensure universal, strong, hardware-enforced memory safety. The longer-term vision is to provide hardware-level security guarantees for AI systems operating in sensitive real-world environments, even where an attacker has control of software running on the device.

​

This project is funded by the UK’s Advanced Research + Invention Agency (ARIA) as part of the Safeguarded AI programme, which is testing whether mathematical techniques that prove software and hardware behave exactly as specified — can make high-assurance cyber defence practical at a scale previously out of reach.

​

The AIVHAI vision

• Build a formally verified, open-source, CHERI-enabled edge AI hardware accelerator

• Protect and confine AI models, AI agents, and the software acting on their behalf, by using CHERI memory protection and compartmentalisation

• Prove end-to-end hardware and software security properties using Sigil’s platform for rigorous engineering, HOARDE

​

The AIVHAI approach

AI accelerators are critical new hardware Trusted Computing Bases (TCBs) through which essentially all sensitive data from mobile and small IoT devices passes: biometrics, user input, text messages, email, web browsing, photos, video, …

​

Current AI accelerators have weak security models (if any at all!) that are detached from those of the application cores where AI agents (and software acting on behalf of those agents) run, risking software vulnerability, cross-model leakage, proprietary parameter theft, user data theft, and agents that escape confinement.

​

The AIVHAI edge AI accelerator will protect and confine AI models, AI agents, and AI-driven software using formally verified, CHERI memory safety and compartmentalisation that is unified across general-purpose and accelerated compute.

​

Technical approach

This project will:

• Atom smash CapLtd’s CVA6-CHERI application core with Google’s Coral Neural Processing Unit (NPU), implementing CHERI memory protection and compartmentalisation across compute and acceleration.

• Create new CHERI-based compartmentalisation firmware that protects and confines models, agents, and the software they interact with.

• Use Sigil Logic’s AI-assisted formal verification tooling, HOARDE, to ensure architectural, hardware, and software CHERI security properties are correct end-to-end across the hardware-software design.

• Formally prove the isolation properties of the compartmentalisation firmware using Cherified Systems’ Rocq-based proof methodology.

• Make the resulting hardware, software, and formal artifacts available through lowRISC’s open hardware ecosystem.

​

Coming soon: The code

The AIVHAI project started in September 2026, and is developing the AIVHAI edge AI accelerator as “open source since inception.” GitHub repository links for code, documentation, assurance, material, and other content will go online over the course of 2026Q4.

​

The team​​​​​​​​​​