Sigil Logic to Lead Rigorous Engineering for Secure AI Hardware

Today we're announcing AIVHAI ("AI Verified Hardware for AI"), a 15-month project funded by ARIA under its Safeguarded AI programme. Together with Capabilities Limited, lowRISC CIC, Cherified Systems, and Google Research, we will build an open-source, 64-bit, CHERI-enabled application processor with an integrated AI accelerator. CHERI provides hardware-enforced limits on which memory software can access. Sigil Logic will lead the project's rigorous engineering process, including its formal verification. This work connects specifications, models, and verification evidence throughout development, including proofs that the hardware and firmware keep AI models isolated from one another. Our partners will use HOARDE, our rigorous engineering platform, in their own work on the hardware and software designs.

The project is led by Capabilities Limited, whose team pioneered the creation of CHERI and has spent more than a decade taking it from research into shipping silicon. We are excited to be working alongside them.

AI accelerators, the specialized processors that run AI models on phones, laptops, cars, and other devices, now handle the most sensitive data those devices hold: biometrics, messages, photos, and the inputs and outputs of the AI models themselves. Devices increasingly run AI models from different vendors on shared hardware, processing sensitive data and valuable model weights. An attacker who gains control of the code running one model must not be able to steal another model's protected weights or data, or tamper with its results. AIVHAI will enforce these boundaries through hardware and firmware.

The team will extend Capabilities Limited's CVA6-CHERI application processor core with AI acceleration hardware from Google's Coral NPU, so that the processor's CHERI protections also govern AI computation. New compartmentalization firmware will keep AI models isolated from one another and from the general-purpose operating system. The team will demonstrate the design on an FPGA prototype running two AI models in separate protected compartments alongside a general-purpose operating system. A software application will use both models while their private weights and data remain protected – while itself being protected by strong CHERI memory safety and compartmentalization. The hardware design, software, and proofs will be released as open source.

Our job is to lead the rigorous engineering process that connects specifications, models, implementation, and assurance evidence throughout development. As part of that work, we will use HOARDE to prove that the hardware and firmware protect AI models' weights, data, and results from unauthorized access or modification, even if an attacker controls another model's compartment or the general-purpose operating system.

That means proving that the instruction set enforces CHERI's protection rules, the integrated hardware implements that instruction set correctly, and the firmware preserves isolation between compartments. Together with other assurance artifacts and engineering evidence, these proofs will establish the security guarantees across the hardware and firmware stack. Every proof is checked by an independent proof checker, and an independent central Red Team works throughout the project to challenge the full assurance case behind the platform's security claims. More on the technical details below.

Verification of a hardware, firmware, and software stack of this size has historically taken decades of person-years. The seL4 microkernel, comprising roughly 9,300 lines of code, required more than 20 person-years of verification effort. In AIVHAI, we aim to develop the hardware, firmware, and proofs together on a 15-month schedule. HOARDE puts AI to work on the search-intensive parts of that effort, mining and generating specifications, driving proof search, and coordinating verification tools. The team will use the verification results to guide the design as it evolves. Independent proof checkers validate the resulting proofs. We do not believe a project of this complexity could be attempted on this schedule without AI-assisted formal methods.

HOARDE is Sigil Logic's platform for bringing formal methods into everyday engineering. Its AI agents specify, model, and verify a system, and maintain traceability across it. It is built on NINJA, the engineering method our founders have developed over three decades for high-assurance hardware, software, and deployed systems. AIVHAI puts HOARDE to work across the whole stack, from architecture and formal semantics through implementation to evidence on hardware. We are hiring hardware-verification engineers for this work and related efforts; the AIVHAI roles are US-based. See our open roles.

Capabilities Limited leads the project and owns the system architecture: the CVA6-CHERI application core, a CHERI extension of the OpenHW Foundation's CVA6 RISC-V core developed with lowRISC; the integration of Coral's vector and matrix unit into it; and the design and implementation of compartmentalization firmware, compiler, and operating-system platform. lowRISC CIC, stewards of the OpenTitan root of trust, leads hardware test infrastructure and continuous integration, the 64-bit version of Coral, and integration on FPGA. Google Research contributes to the Coral NPU work, along with a reference implementation and formal proof of the CHERI Vector Matrix Extension, and upstream compiler support. Cherified Systems leads the formal specification and proof of the compartmentalization firmware using its Rocq-based Guru framework.

Sigil Logic's verification targets:

1. The instruction set cannot be bypassed. The CHERI RISC-V instruction set, extended with the new vector and matrix instructions and modeled in Sail, never lets a sequence of instructions manufacture more authority than it was given. This property is capability monotonicity, the architectural definition of non-bypassability.
2. The hardware implements the instruction set. The CVA6-CHERI core with the Coral vector and matrix unit correctly implements that instruction set, the memory subsystem included and DRAM and I/O excluded. This holds for both the SystemVerilog implementation and its Guru specification of the datapath.
3. The firmware keeps the compartments apart. The compartmentalization firmware preserves the confidentiality and integrity of the AI models running above it and protects itself from those models and from the operating system.

We assume the adversary already has arbitrary code execution inside a model compartment or inside the operating system. The proofs address whether that control lets the attacker cross a protection boundary to access or modify another model's protected weights, data, or results. Side channels and physical attacks are outside the formal boundary for this initial work.

"AI accelerators have become the trusted computing base of so much, and almost none of them can say what they guarantee," said Dr. Joseph Kiniry, co-founder and Chief Scientist of Sigil Logic. "We aim to prove that a model running on this hardware cannot read its neighbor's weights, cannot tamper with its neighbor's results, and cannot reach anything it isn't supposed to. What makes this a 15-month project rather than a 15-year one is that AI-assisted formal methods have become effective enough to prove and secure real hardware and software. That is the thesis Sigil Logic was founded on, and I am excited to demonstrate it."

The project will deliver an open-source design and working FPGA prototype intended for adaptation into future commercial chips. Learn more on the AIVHAI project website.

AIVHAI is funded by ARIA through the TA2 Cybersecurity track of its Safeguarded AI programme, led by Programme Director Nora Ammann. The track is backing eight R&D Creator teams with £22 million to test whether AI-enabled formal methods can make high-assurance cyber defence practical at scale, while building UK capability in AI and formal methods.