ci: run the proofs and the interpreter that nothing was running

[rrrodzilla]

Closes #15. (#11, which blocked it, is merged.)

The Taskfile defined kani and miri tasks and both crates carry real harnesses — agent-uri/src/kani_impls.rs (6 proofs) and agent-uri-attestation/src/proofs.rs (13 proofs) — but no job ever ran them. Nineteen proof harnesses sat in the tree proving nothing.

Both new jobs sit on the existing weekly schedule plus workflow_dispatch, beside fuzz, for the same reason fuzz is there: a model checker exhausts a state space and Miri is roughly two orders of magnitude slower than native. Neither is something a pull request should wait for.

Scope, and why it is not --workspace

Job	Runs	Not
kani	agent-uri, agent-uri-attestation	The other crates carry no harnesses; --workspace would compile the CLI, the eval harness, and libp2p to prove nothing
miri	agent-uri, agent-uri-attestation (--lib)	agent-uri-dht, -dht-libp2p, and the CLI test against tokio, real sockets, and the filesystem, none of which Miri can execute

Pointing Miri at the networked crates would produce a job that fails every week for reasons that are not defects, which is worse than no job.

Two details that are load-bearing

Miri needs -Zmiri-disable-isolation. This is not a guess — running without it fails concretely:

error: unsupported operation: `clock_gettime` with `REALTIME` clocks
       not available when isolation is enabled
  inside `chrono::Utc::now`
  note: inside `claims::AttestationClaimsBuilder::build` at claims.rs:378

The flag relaxes no undefined-behaviour check — those are what the job is for — it only lets the attestation tests read the clock they were written against.

The Kani version is pinned (KANI_VERSION: 0.67.0) so a run is reproducible and an upstream release cannot turn a green week red on its own. ~/.kani is cached separately from Swatinem/rust-cache, which does not reach outside the cargo directories, keyed on the version that produced it.

The Taskfile now runs exactly these commands, so a local run and a CI run agree rather than drifting.

Verification status — please read

I could not complete a full local run of either tool: CBMC and Miri both exhaust this workstation's session and kill it. What was verified locally before that happened:

• cargo kani -p agent-uri-attestation --harness matching_issuers_succeed — passes, 0 of 400 checks failed. (Also the evidence for Move kani-verifier out of regular dev-dependencies #18, that the kani-verifier dev-dependency was unnecessary.)
• cargo +nightly miri test -p agent-uri --lib — passes, 196 tests.
• cargo +nightly miri test -p agent-uri-attestation --lib without the flag — fails as quoted above, which is what established the need for it.

What is not yet confirmed end-to-end: the full 19-harness Kani run, and the attestation crate under Miri with isolation disabled.

Both are cheap to settle on GitHub's runners, which is where these jobs live anyway. After merge, trigger CI via workflow_dispatch on main; the kani and miri jobs will run. If either turns up something, it is a real finding about the code or a scope adjustment to this file, and either way it is better learned there than not at all. I did not want to present these as verified when they are not.