Soundness and Security

A Hekate proof that verifies under Config::prod() shows that some trace satisfies the program you pinned, on the public inputs you hold. Each challenge that could let a false proof through is priced from a published bound, and the verifier rejects a proof whose computed terms fall below 100 bits. One term is undercounted today, and What is not promised gives its reach. This page covers the terms, the transcript order, the tests and the checks that stay with you. Hekate has not had an independent audit.

§ What a valid proof shows

A valid proof shows that some trace satisfies every constraint, pinned cell, fixed column and bus of one program, and nothing about what the program means.

Soundness is the promise behind it: a prover without such a trace makes the verifier accept with probability at most $\varepsilon$, and $-\log_2 \varepsilon$ is the soundness in bits. The statement is what the verifier holds before the proof arrives: the program, identified by its pinned program id, the public inputs and the main table's height, one Config and one transcript label. A program that misses a constraint admits traces its author never meant, and Preflight shows a forged trace that passes both preflight and the verifier.

The prover is the adversary. It chooses the witness and the height of every chiplet table, runs any binary or writes the proof bytes by hand, and sees each challenge before it answers. It cannot change what your build holds: System Architecture draws that boundary. The prover binary is closed source, and soundness does not rest on it: a modified build meets the same checks. Privacy does, because the binary reads the witness.

The verifier's own checks follow one rule:

A check on the verify path is safe if and only if its answer is a total function of data the verifier recomputes or compares by equality, with no case analysis over author-chosen structure.

From Liveness was a witness.

Its path runs sumcheck, the commitment openings, the bus sums, fixed columns recomputed from their shapes, boundary comparisons and the program id comparison, plus membership tests over the program it holds: every bus selector is a fixed column or absent, and every ordered bus has the shape the engine defines. Clock waivers are checked when the program compiles, and no verdict reads them.

§ What the 100 bits count

Every random challenge can let a false claim through with a small probability, and Hekate prices each from a published bound.

The commitment encodes each row of a grid of $R$ rows into a codeword of length $n$ at rate $\rho$, opens $t$ columns (num_queries) and batches $u$ terms into one opening. $N$ counts bus rows: each table's height times its bus endpoints, summed over the tables. With zero knowledge on, the outer argument opens $t_o$ columns (outer_queries) of a code of length $n_o$ for messages of $k_o$ symbols. Every other challenge tests a polynomial of degree $d$: a sumcheck round's degree, the variables of a random point, the terms of a combination.

The verifier computes the first five terms from the program, the table heights and the Config before it draws the challenges they price, and stops with SecurityTooLow when one falls below min_security_bits, 100 in Config::prod(). It computes the query and proximity terms once per proof, on the one commitment that holds every table, in integer arithmetic both sides reproduce exactly, and every rounding lowers the estimate.

The verifier does not compute the last row. The table limits keep $d$ small: a round has degree at most 15 and a table at most 32 row variables, and a combination reaches the floor only past $2^{28}$ terms.

Hekate quotes the weakest term as the soundness of a proof, with the hash taken as a random oracle. A non-interactive prover retries a challenge by changing a value it sent before it and hashing again: one that computes $2^k$ transcripts beats a challenge priced at 100 bits with probability up to $2^{k-100}$. Hekate buys no bits with proof-of-work.

No term of the form $x/2^{128}$ reaches 128 bits: each loses $\log_2 x$ bits to the size of what it ranges over, and more queries shrink none of them. The estimate that chose its own geometry derives the floor from these theorems and sets it beside other deployed systems.

§ Every value before its challenge

Fiat-Shamir soundness rests on one ordering rule: every value a check reads is fixed before the challenge the check depends on.

Each challenge is a hash of the transcript up to that point, and a value sent after it can be fitted to it: the check that reads the value then solves an equation where it should test a claim. Hekate shipped this once: a LogUp helper's value entered the transcript after the point that tested it, and no commitment bound it (Three unbound values).

A value is fixed in one of two ways: the transcript absorbs it, or a commitment binds it whose root the transcript absorbed earlier. Claims about committed columns may follow a challenge, because the opening holds them to a root fixed before it.

With zero knowledge on, the outer argument follows the opening in the same pattern: its auxiliary root, each test's response before the next challenge, then its column positions.

Some values never come from the prover: the verifier computes fixed columns, clocks and row numbers itself, and your build holds the program, whose id the transcript absorbs first. The floor, min_security_bits, stays out of the transcript: it is your verifier's policy, and no proof can move it.

§ How Hekate tests soundness

A soundness test builds what an attacker would: a witness consistent with every check except the one under test, run through the real prover and the real verifier.

A test that changes one cell of an honest trace shows that some constraint reads that cell. Hekate's Keccak and AES exploit suites were built that way, and they passed while seven soundness gaps stood open in those two chiplets (Shapes the honest prover never builds). The Hekate repository keeps these suites:

• security_exploits.rs, bus_security.rs and chiplet_security.rs: proofs rewritten field by field, from opened columns and claimed bus sums to table heights, claim counts and the configuration.
• chain_existence.rs: witnesses that keep every gate low and still carry a chosen public value into the cell the host reads.
• ordered_bus.rs, Keccak's output_pairing.rs and AES's call_pairing.rs: calls that trade answers, a rotated chain of calls, a responder taller than its calls.
• sbox_parity_forgery.rs and lookup_parity_forgery.rs: equal messages on one side of a bus, which cancel in a binary field.
• mlkem_pipeline.rs and mldsa_pipeline.rs: ML-KEM outputs matched against the ml-kem crate, signatures from the ml-dsa crate, and forged witnesses that each name the check that must reject them.
• generator.rs: a fixed-seed corpus of random geometries, gates, bus topologies and witnesses, in the ordinary test run. Each honest sample verifies, and its forged public input and drifted program id are rejected.
• liveness.rs: every bus selector of every shipped table is a fixed column or absent.
• mixture_proximity.rs: the per-query pass rate of a worst-case commitment, built from a minimum-weight codeword, measured against the bound the query term prices.

hekate-scribble draws random tampers against your own circuits, which shows the constraints you wrote are wired: Preflight covers it. The tests for hiding are on Zero Knowledge.

§ What stays with you

The verifier checks a proof against the program you hand it, and the checks below are yours.

• Pin the audited program. Compile in the program id printed at audit time, one per height when the program pins a row by its height, and build the program from the audited source.
• Verify under Config::prod(). The verifying side's configuration decides what it accepts, and under Config::dev() it accepts proofs with four column queries and no floor.
• Accept only Ok(true). A forged proof can produce Ok(false) or an error, and Verifier Logic lists which checks give which.
• Determine every published cell. A boundary pin ties a cell to a public input, and constraints the prover cannot switch off have to determine that cell, or the prover picks it; AIR Constraints works through one.
• Read every committed column in a constraint of its own table. A column that appears only in a bus key and in the trace generator is a value the prover picks, whatever the bus sum says about it.
• Constrain each request a chiplet answers. A chiplet computes what the request names: pin every field your statement relies on, such as the opcode of an IntArithmeticChiplet call.
• Constrain every Bit the prover fills. The commitment binds a Bit cell only as a 32-bit value, and assert_boolean holds it to 0 or 1.
• Emit requests in the order you mean. On an ordered bus request $t$ meets response $t$, and the engine cannot tell an intended order from a mistake: LogUp Buses.
• Keep the witness private. A fresh seed for every proof, the ct prover for private data, and heights chosen from public data: Zero Knowledge.

§ Postmortems

Each postmortem states what broke, how it was found, what fixed it and what the release still does not promise.

§ What is not promised

These limits stand today.

• Key width in the bus term. The verifier prices the bus challenge for one event, $\gamma$ zeroing the denominator of some bus row: $N/2^{128}$. A bus whose two sides carry different messages can also sum to zero at the drawn $\gamma$ and $\beta$. A key of $k$ slots is a polynomial of degree up to $k - 1$ in $\beta$, and Schwartz-Zippel bounds the two events together by $\sum_e N_e \max(2, k_e) / 2^{128}$ over the bus endpoints $e$, with $N_e$ rows and $k_e$ key slots each. The verifier leaves out the factor $\max(2, k_e)$, worth $\log_2 k$ bits on a bus with $k$-slot keys: 4.7 on the Keccak bus, whose keys carry 25 lanes and a rank. The check admits up to $2^{28}$ bus rows, and once the rows weighted by key width pass $2^{28}$, this term sits below 100 bits.
• 128 bits. No configuration provides the 256-bit challenge field they need.
• Terms nobody has found. The terms above are the ones identified: "How many terms a soundness argument has is not something the argument tells you" (The estimate that chose its own geometry).
• Circuit semantics. No engine decides whether a circuit computes what its name says. The pinned id fixes which circuit a verifier checks, and Primitives states what each chiplet proves and what it leaves outside the proof.

§ Next steps

• PIOP Protocol: the reductions behind each term.
• Zero Knowledge: what a valid proof hides, and the tests behind it.
• Verifier Logic: run the verifier and read its result.
• Preflight: find a broken constraint before you prove, and what a clean report misses.