X730 Certification Record
The X730-MP4-Lux 1.0 record describes the certified application-processor core, its CHERI-RISC-V modes, verification evidence, and system-integration assumptions.
This is the public certification record for the product and version named below. It preserves the scope and principal answers published when the certification was granted.
Product information
- Certification date: 26 March 2026
- Certification programme version: 1.0
- Organisation: Codasip
- Organisation type: commercial company
- Product: X730-MP4-Lux
- Product type: processor intellectual property — CPU
- Reference:
release-Orleans-Lux-1833-FRZ-rc01-11.3.1 - Version: 1.0
- Derivative of a qualified product: no
- Product information: Codasip X730
The X730 is a commercially licensable 64-bit application-processor core implementing CHERI-RISC-V. The baseline design is described as an in-order, dual-issue, nine-stage processor with a memory-management unit, extended to handle capabilities and CHERI instructions.
Architecture and scope
The certified product implements CHERI-RISC-V 0.9.3 extensions for pure-capability execution, hybrid execution, capability-aware page-table entries, and related functions. It also implements application-class RISC-V integer, floating-point, atomic, compressed, bit-manipulation, virtual-memory, cache-management, privilege, and debug extensions described in the submitted record.
Pure-capability mode uses capabilities for pointers throughout protected software. Hybrid mode allows capability-aware and conventional integer-pointer code to coexist, supporting staged software migration.
Verification evidence
The applicant described approximately 17 verification environments combining formal property checking and simulation. These included:
- formal proofs for CHERI checks and calculations;
- a memory-subsystem environment focused on coherency in multi-core configurations;
- isolated pipeline simulation with random instruction streams checked against the RISC-V Sail model;
- formal equivalence checking for implementation changes such as clock gating.
Results were tracked against requirements so that each specified behaviour had coverage in at least one environment. The record reports more than 40 person-years of verification effort. It also states that Codasip’s processes had been reviewed by TÜV SÜD and that 32-bit configurations generated from the same code base had received ISO 26262 certification. Those statements provide process context; they do not extend that separate certification to the X730 product record.
Memory access and debug
In pure-capability mode, the submitted record identifies no normal memory operation without an explicit capability. In hybrid mode, the program-counter capability or default data capability supplies authority for integer-pointer access. Hardware page-table walks are not bounded by capabilities.
Debug mode disables CHERI checks and is not expected to be active during normal operation. Entry uses the standard RISC-V debug mechanisms, and the surrounding system-on-chip is expected to control the external debug interface.
Capability tags
The record identifies no operation that can set a capability tag on an arbitrary value. Capability-aware memory paths preserve tags, while non-capability writes clear them. Correct behaviour across caches, memory controllers, direct-memory-access engines, and other bus masters depends on the system-on-chip integration described by the product implementer.
Temporal memory safety
The X730 implements the four-bit page-table-entry scheme described by Cornucopia Reloaded. Capability dirty tracking identifies pages to which capabilities have been stored, and a load barrier prevents capabilities from being loaded from pages that have not yet been swept for stale references. Freed memory remains in quarantine until those references have been found and invalidated.
The mechanism combines processor support with software management. The property delivered to an application therefore depends on the allocator, operating system, virtual-memory configuration, and integration around the core.
Certification boundary
The certification covers X730-MP4-Lux version 1.0 and the configuration described in the submitted record. It does not automatically certify a chip, board, operating system, virtualisation stack, application, debug policy, or deployed product that incorporates the core.