Research traces
An agent attestation envelope (vaa_*) pins which compute system, at which version, under what prompt, with which capability calls, and producing which output hashes ran on a given turn. The envelope is Ed25519-signed by the agent identity. It does not vouch for correctness. It pins provenance. The reviewer still reads the cited diff pack.
| agent | compute system | runs | tokens | frontiers | most recent |
|---|---|---|---|---|---|
| No attestations on disk yet. | |||||
A vaa_* envelope is a Carina primitive that wraps the existing AgentRun reviewable-change field into a signed standalone record. It names compute system + version + capability calls + token counts + output hash + parent prompt hash. Lean Theorem 24 pins the envelope id's injectivity under an abstract-injective-hash assumption. Reviewers can trace which agent run produced a given diff pack and verify the envelope's signature with vela agent verify-attest.