How it works
What Ephyra refuses to pretend
The rules that make its evidence worth reading, where each guarantee comes from, and what is not guaranteed.
A system that fixes its own bugs is only useful if you can believe what it tells you. The cheapest failure for such a system is also the most damaging: reporting success it did not earn. Ephyra is built around a short list of refusals.
Five rules
Evidence is never synthesized. No proof item exists for a run that did not happen. No check is "passed" because its integration was unavailable. An integration Ephyra could not verify raises Unverified and stops, instead of producing a plausible result.
Untrusted content is data. Signal text, logs, stack traces, forge comments and study answers are wrapped as <untrusted_…> blocks when they are shown to a model. They never appear in instructions and never grant a capability. A stack trace that says "ignore your rules and push to main" is a string in a box.
Side effects have keys. Every external write carries a stable operation key. An ambiguous outcome raises ReconciliationRequired. A write that timed out is never blindly retried.
Secrets stay out. Credentials are not logged, committed, written to journals or sent to models. They are read from the environment or a credential reference. Proof logs are redacted for common credential formats and any secret values the caller supplies.
Identity is recorded as returned. A model is named by exactly what its backend reported. Thresholds are keyed by that identity, and there is no silent fallback to another model.
What you can rely on
| Claim | What backs it |
|---|---|
| The decision I made applies to what I read. | Approvals are bound to the revision, head and proof digest; a mismatch is refused as stale. |
| The proof I approved is the proof that landed. | Proof refs are immutable, and the bundle's digest is part of the approval. |
| A patch cannot edit the checks that judge it. | The verification harness and its dependency closure are declared as protected paths; touching them invalidates the verifier. |
| A crash does not repeat a payment or a push. | Effects are delivered through a durable ledger keyed per operation. |
| High-risk changes had a person. | High and critical risk require a named human at C, enforced in the proof evaluation, not just in policy. |
| Critical changes were landed by hand. | Automatic and live landing are forbidden for critical risk. |
| Someone else's push is not overwritten. | Landing and rollback are conditional writes against the ref Ephyra last saw. |
| The audit log was not edited. | Entries are hash-chained. |
What is not guaranteed
Being exact about limits is part of the same rule.
- The digest binds a bundle; it does not prove execution. It shows which bundle you approved. That its commands truly ran rests on the runner and the protected harness.
- The local runner is not a sandbox. It is for repositories you trust. It does not limit network or resources. Isolation comes from a sandboxed runner.
- The levels are a mapping. An autonomy level is translated to checkpoint and landing settings. Whether a deployment honors them depends on the callers enforcing those checkpoints.
- Tests use fixtures. The test suite makes no network calls. Live providers, forges, sandboxes and paid model calls are unverified by it. A healthy server or a passing suite does not establish that a production repair works for you.
- A saved connection is not an observation. "Configured" and "observed" are different words on purpose.
- An acknowledgement is not a reading. A delivered notification means a transport accepted it.
- Tutor explanations are a reading aid. They cite records and are marked stale when a quest moves, but they are a model's summary, not evidence.
Reading "Unverified"
Each package's README has a section listing what is verified and what is not. "Unverified" there means precisely: this code path exists and is tested against a contract or a fake, and has not been exercised against the live service. It is a statement about evidence, not a euphemism for broken.
Reporting a problem
Security reports go to the contact in security.txt. The security policy describes what to expect.