How Verification WorksDON'T TRUST — VERIFY
The model witnesses in · deterministic checks · signed verdicts out
Omenion never runs your solver. You submit the witness — the decomposition, partition, network, assignment, or proof — and a deterministic checker recomputes the claim from scratch: exact arithmetic, exhaustive enumeration where the math allows it, the Lean kernel for proofs. Same witness, same spec, same verdict, every time, on any machine. The asymmetry is the product: finding a witness can take a datacenter; checking it takes milliseconds.
Because the checker is deterministic, the verdict can be signed. Money moves on that signature — escrow holds open on pass, payouts release after the dispute window — so the signature, not our database, is the source of truth you can hold us to.
The attestation envelope returned with every verdict
| v | envelope version (currently 1) |
| problem_id | slug of the axiom the witness was checked against |
| verifier_kind | which deterministic checker ran (see registry below) |
| artifact_hash | SHA-256 of the exact witness bytes that were checked |
| verdict / verdict_code | pass · fail · malformed — the binding result |
| reason | machine-readable failure reason (absent on pass) |
| output_hash | domain-tagged SHA-256 binding verdict + witness + key metrics (cut value, mult count, …) into one digest |
| elapsed_ms / fuel_cap_ms | observed runtime and the wall-clock cap it ran under |
| attested_at | ISO-8601 timestamp of attestation |
| worker_key_id | kid of the Ed25519 worker key — attached after signing |
Verify it yourself Ed25519 · published key
The signature covers the attestation JSON exactly as returned (witness-tier verifiers sign before worker_key_id is attached; the WASM runtime signs the full envelope). The public key is served at GET /api/v1/attestation-key — current kid: ScyyOgrDqjmXme_w6IOfbWpBXR8iXnEbSk_rfutr5-g. Changing a single bit of the verdict, the witness hash, or the metrics invalidates it.
# pip install cryptography — full script: examples/verify_attestation.py
key = GET /api/v1/attestation-key # Ed25519 public JWK, kid pinned
att = dict(result["attestation"]); att.pop("worker_key_id")
Ed25519PublicKey.from_public_bytes(b64url(key["x"])).verify(
b64(result["signature"]),
json.dumps(att, separators=(",", ":")).encode()) # raises if tamperedVerifier registry what each checker actually does
| matmul_bilinear_decomposition | the (u, v, w) decomposition reconstructs the full matmul tensor in exact integer arithmetic (ℚ or GF(2)) — every entry, no sampling; multiplication count ≤ record checking is a triple loop; finding one is AlphaTensor-hard |
| sorting_network | sorts all 2ⁿ binary inputs (0-1 principle ⇒ sorts everything); comparator count ≤ budget exhaustive over the binary cube — no randomness, no heuristics |
| max_cut | partition is 0/1 per vertex; recomputed cut weight ≥ the record-to-beat threshold record bounties: verifying an improvement is cheap, proving optimality is not (and isn't claimed) |
| sat (WASM) | assignment satisfies every clause — evaluated inside a content-hashed Rust→WASM binary in an isolated worker the verifier binary itself is pinned by hash (below), so the checker can't drift silently |
| lean4_proof_check | Lean 4 type-checks the proof of the exact required theorem; no new axiom declarations; no sorry; resource-capped the Lean kernel is the trust anchor — single-file core-only today (no Mathlib yet; see docs) |
What we don’t claim scope, honestly
- Record bounties (max-cut, matmul, sorting networks) verify improvement, not optimality — beating the threshold is the claim, nothing more.
- Lean checking is single-file, core-only today; Mathlib-dependent axioms aren’t verifiable yet. Gaps tracked publicly in
docs/verification-architecture.md. - Benchmark / simulation axiom kinds are listed but not yet automated — submissions to them are rejected with 422 rather than queued into a black hole.
- All verifiers run under wall-clock and memory fuel caps; an exhausted cap is a
failwith that reason, never a silent pass.