Certificate Manifest Schema

Schema reference for the proof-carrying certificate manifests that rz --emit-certificate <DIR> produces.

Table of contents

Overview
Manifest JSON shape
- Top-level fields
- Obligation entry fields
Outcome semantics
Verification flow
Compatibility
See also

Overview

When you compile a Resilient program with --emit-certificate <DIR>, the compiler writes:

One <fn>__<kind>__<idx>.smt2 file per discharged Z3 obligation (see format_cert_filename in cert_sign.rs).
A manifest.json enumerating every obligation, its certificate filename, and a SHA-256 over the certificate bytes.
(Optional, with --sign-cert <key>) Ed25519 signatures attached to each obligation entry, signing the certificate bytes.

The manifest is the proof-carrying binary artifact: hand it to a downstream consumer alongside the binary, and they can re-verify every obligation through Z3 with rz verify-all <DIR>.

Manifest JSON shape

The current writer emits the two top-level fields below. Verifiers must tolerate unknown top-level and obligation-entry fields, so future releases can add optional metadata such as schema version, compiler version, Z3 version, or timestamps without breaking older consumers.

{
  "program": "examples/sensor.rz",
  "obligations": [
    {
      "fn": "read_sensor",
      "kind": "requires",
      "idx": 0,
      "cert": "read_sensor__requires__0.smt2",
      "sha256": "8c1f3e...",
      "sig": "a1b2c3..."
    }
  ]
}

Top-level fields

Field	Type	Required	Description
`program`	string	yes	Path to the source file (relative or absolute).
`obligations`	array	yes	One entry per discharged obligation. Order is stable.

Obligation entry fields

Field	Type	Required	Description
`fn`	string	yes	Function name the obligation belongs to.
`kind`	string	yes	One of: `requires`, `ensures`, `invariant`, `recovers_to`.
`idx`	integer	yes	Zero-based index within the function for this `kind`.
`cert`	string	yes	Filename of the `.smt2` file (no directory prefix).
`sha256`	string	yes	Hex-encoded SHA-256 over the cert file’s bytes.
`sig`	string	no	Hex-encoded Ed25519 signature when `--sign-cert` is used.

Outcome semantics

Each obligation entry corresponds to a verification outcome:

proven — Z3 returned unsat for the negation. The .smt2 file contains the unsat-core proof. This is the default for entries that appear in the manifest.
runtime — Z3 timed out or returned unknown; the obligation was retained as a runtime check. Runtime-only obligations do not appear in the manifest (the manifest only enumerates discharged proofs).

If a downstream verifier needs to know the full set of obligations (both proven and runtime-retained), inspect the source program rather than the manifest. The manifest is intentionally a positive record of “what we proved”, not a negative one.

Verification flow

$ rz --emit-certificate ./certs --sign-cert priv.pem prog.rz
... compiles, emits ./certs/manifest.json + per-obligation .smt2 files
... signs each cert with Ed25519

$ rz verify-all ./certs --pubkey pub.pem
... walks manifest.json
... for each obligation:
...   1. recompute SHA-256 over cert bytes
...   2. verify Ed25519 sig (if --pubkey supplied)
...   3. invoke z3 on the cert and check (check-sat) returns `unsat`
... exits 0 only if every obligation passes

A non-zero exit code from verify-all indicates one of:

A cert file was tampered with (SHA-256 mismatch).
A signature does not validate against the supplied public key.
Z3 disagreed with a proven obligation (this should not happen unless the Z3 version differs significantly).
The manifest itself is malformed.

Compatibility

The current manifest shape is the inaugural version.
New optional fields may be added at any time without changing the required field set above.
Removing or renaming a required field requires a versioned migration path in this doc.
Verifiers MUST tolerate unknown top-level and obligation-entry fields (forward compatibility).