Formal methods

Why it matters

A precise model reduces ambiguity in security-critical rules and can act as an executable reference for hardware and software work.

In brief

Formal methods use mathematical models and machine-checked reasoning to define and analyse architecture behaviour. In CHERI, formal semantics have been developed alongside implementations and used for documentation, testing, validation and proof.

Formal evidence is strongest when its boundary is explicit: the model, property, assumptions, implementation relation and tool result. Ask what was proved and what remained outside the model before using a proof to support a system-level claim.

Key considerations

1. Model

Describe instruction and capability behaviour precisely for a named architecture revision.

2. Validate

Compare implementations with models through test generation, test oracles and structured review.

3. Prove

Establish selected properties under explicit assumptions; connect them to the implementation and system claim.

Evidence and caveats

A proof covers its model, property and assumptions. It does not automatically verify every microarchitectural detail, compiler, OS or product.

Use the exact architecture and software specification implemented by the target. Separate architectural guarantees from system-level outcomes.

Primary routes

• CHERI rigorous engineering