I. The problem
Spend a note without revealing it
Start with a private note representing some tokens. To spend it, the owner must prove three things: that the note exists, that it belongs to them, and that it has not been spent already. Aspis checks those facts without revealing the note or the owner.
The public pool stores commitments to many notes. A commitment is a cryptographic record that lets the owner refer to a note without publishing it. When a note is spent, everyone sees the public payment details and the proof. They do not see the note, its position in the pool or the private key.
Each note also has a nullifier: a serial number revealed only when the note is spent. The program rejects a nullifier it has already recorded, which prevents the same note being spent twice. The nullifier does not identify the hidden note.
The program verifies the proof, records the nullifier and updates the pool. A withdrawal also sends tokens from the pool vault. These operations occur in one Solana transaction: all the account changes are committed together, or none of them is.
II. The proof
What “Circle STARK” means here
“Circle STARK” is a compact name for four separate ideas.
Zero knowledge
The prover shows that a payment follows the rules without publishing the note, its owner or the private key used to spend it.
STARK
A STARK lets the verifier check a long calculation by testing a much smaller proof. It reduces the calculation to polynomial claims and samples them at unpredictable points. A false claim has only a small, quantified chance of passing.
Transparent
All parameters used to create and check proofs are public. Nothing comes from a ceremony at which secret material must later be destroyed.
Circle
The polynomial evaluations use points on an algebraic circle. This lets Aspis work efficiently over M31: the integers modulo 2³¹ − 1.
The verifier runs directly
Some systems first compress a STARK into another proof, often Groth16, and put only that wrapper on chain. The wrapper is smaller, but it normally introduces a trusted setup. Aspis runs the Circle STARK verifier itself, using public parameters from the proof through to the account update.
III. The Solana result
The complete V7 withdrawal used 1,201,757 CU
Solana measures program work in compute units (CU), with 1.4 million available to a transaction. These figures cover the whole Aspis instruction: proof verification, account checks, the pool update, the nullifier record and, for a withdrawal, the token transfer.
| Payment | New storage page needed? | Compute units | Transaction bytes |
|---|---|---|---|
| Private transfer | No | 1,145,890 | 799 |
| Private transfer | Yes | 1,191,463 | 832 |
| Withdrawal | No | 1,136,135 | 964 |
| Withdrawal | Yes | 1,201,757 | 997 |
I measured V7 against a local Solana runtime; it has not run on a public cluster. The repository records the exact programs, proof inputs, logs, hashes and resulting accounts for each case.
IV. The checked mathematics
Lean 4 checks the three difficult V7 theorems
Lean is a proof checker: it accepts a theorem only when each step follows from earlier definitions or theorems. Previous Aspis releases cited papers for three difficult results. The V7 repository contains machine-checked proofs of the specialised versions used here.
The candidate list has a fixed limit
After the first decoding checks, a dishonest prover may still leave several candidate answers. The Lean theorem gives an exact upper bound on that list.
Folding cannot repair a false claim
The verifier reduces a large table in several rounds. Lean proves that these folding steps do not turn a false opening claim into a true final one.
A hash can stand in for the verifier
In an interactive proof, the verifier asks fresh random questions. Lean checks the theorem used when those questions are instead derived from the transcript hash.
Standard foundations reported by Lean
propext · Classical.choice · Quot.soundThese are normal parts of Lean's mathematical foundations. Aspis adds no project-specific axiom, and none of the three results above is imported as an unproved theorem from a paper.
Rust and the theorem
Relating the proof to the program
A proof of the mathematical verifier is not automatically a proof of its Rust implementation. The source work translates selected Rust paths into Lean, then proves that those functions implement the model.
- 01Production Rust
The selected verifier code parses proof bytes, follows branches and prepares account changes.
- 02Charon records the Rust
Using the compiler's typed representation, Charon records the chosen functions, loops and branches.
- 03Aeneas produces Lean functions
Aeneas translates that record into Lean. The result models the code; further theorems are still needed to show it is correct.
- 04Lean proves the correspondence
Theorems then show where the translated functions agree with the mathematical verifier on inputs, results and state changes.
The Rust may parse a byte differently, take another branch, reuse an earlier hash value or update the wrong account. A theorem about the model says nothing about such mistakes until the implementation has been related to that model.
This correspondence is complete for selected V5 paths and archived with that release. The V7 mathematical proofs are further ahead than the source work: several final links to the current Rust remain open.
V. The mainnet record
V5 completed a private spend on Solana mainnet
V5 is the on-chain baseline. At Solana slot 435,019,536, the program checked a 75,358-byte proof, updated its pool and recorded the note's nullifier. The transaction reached finality.
- Network
- Solana mainnet
- Proof size
- 75,358 bytes
- Slot
- 435,019,536
- Status
- Finalized
The mathematical verifier
Lean checks the payment rules, polynomial identities, finite calculations and probability bounds used by the verifier.
The Rust correspondence
Charon records selected Rust functions, Aeneas translates them into Lean, and further theorems relate those functions to the mathematical verifier.
The deployed V5 program
Pinned source code, compiler and build tools reproduce the Solana program used for V5, byte for byte.
The V5 transaction
The repository archives the proof bytes, program, accounts before and after the spend, transaction record and later cleanup.
Questions
Common questions
- What is Aspis ZK?
- Aspis is an open-source experiment in private payments on Solana. The spender proves that the payment is valid without revealing the note, its position in the pool or its owner.
- Can Solana check a STARK proof directly?
- In local runtime tests, the complete V7 Circle STARK payment path fits below Solana's 1.4 million CU transaction limit. The largest measured case uses 1,201,757 CU. V7 has not yet run on a public cluster.
- Does Aspis need a trusted setup?
- No. The prover and verifier parameters are public; there is no ceremony that creates secret material which must later be destroyed.
- Does Aspis wrap its STARK in a Groth16 proof?
- No. The Solana program runs the Circle STARK verifier itself. Some systems wrap a STARK in a smaller Groth16 proof before checking it on chain; Aspis does not.
- Has Aspis run on Solana mainnet?
- V5 completed a private spend and state update on mainnet, and the transaction is finalised. V7 is the current design and has so far been measured only in local Solana tests.
- What has been formally verified?
- Lean checks the decoding bound, the folding argument and the theorem used to derive verifier challenges from a hash. Selected Rust functions have also been translated into Lean. Several final links from the V7 Rust to the mathematical model remain unfinished.
- Why translate Rust into Lean?
- A proof of a mathematical model does not by itself prove the program. Charon records selected Rust code, Aeneas translates it into Lean, and further theorems relate those functions to the model. That final step can expose a mismatch in parsing, branching, hashing or account updates.
VI. Current position
Results, limits and unfinished work
Current code
Complete transfers and withdrawals stay below 1.4 million CU in the local tests. The main mathematical results are checked in Lean. Several source-level links to the current Rust remain unfinished, and V7 has not been sent to devnet or mainnet.
Public mainnet result
One complete private spend ran on Solana mainnet. The repository archives its program, proof, public inputs, account changes, cleanup and formal record.
I have published the proofs, tests, reproducible builds and V5 chain record, but no independent cryptographic or Solana security review has been completed. Treat Aspis as research software.