VeriCHERI is a formal verification method for exhaustive verification of processors implementing CHERI.
This repository contains verification IPs that help a user setting up and running VeriCHERI. It contains in particular:
- A collection of functions to express monotonicity
- Functions and a property sketch to describe and prove a representability invariant