This codebase is a scheme exploration for lightweight variants of SPHINCS+ (called SPHINCs-). It has not been audited, contains no security guarantees, and is not safe to use with real funds. Cryptographic parameters, key derivation, and contract logic have not been reviewed by any third party. Use on testnets only.
Welcome to SPHINCs-, a family of EVM-optimised variants of SLH-DSA and the recently proposed SLH-DSA-SHA2-128-24. They all achieve low gas cost for pure on-chain signature verification without any precompile which makes them useful today without any ethereum hardfork. The key modifications is substituting SHAKE256 with the native keccak256 opcode and a significant reduction of the signature budget. NIST initially standardized a scheme with a 2^64 signature budget which is a huge number. Ethereum's on chain data shows that among 64,294,251 Ethereum mainnet addresses that sent at least one transaction in 2025 99.99% had less than 3000 transactions annually. The variants described in the repo give a trade-off between signing budget per key pair, verifier cost in gas and signer keygen and signing keccak calls (hardware wallet friendliness).
One can simply build a smart account using any of these verifiers, they are stateless and they maintain 128bits up their specified limits. For a efficient design that works on constrained device you can use the JARDÍN account design (A combination of SPHINCs- with a smaller compact path) are available for this. The SPHINCS+ registration path, the FORS compact path, all the JARDIN contracts and signers lives in a separate repo: nconsigny/JARDIN.
There are different ways to construct the SPHINCS signature scheme. Existing litterature shows various ways to optimise for signature size or verify cost.
| Variant | Family | h | d | a | k | w | l | swn | Sig | sign_h | Verify | Frame | 4337 | sec_10 | sec_14 | sec_18 | sec_20 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| C7 | WOTS+C / FORS+C | 24 | 2 | 16 | 8 | 8 | 43 | 151 | 3,704 B | 4.3 M | 127 K | 210 K | 318 K | 128 | 128 | 128 | 128 |
| C11 | WOTS+C / FORS+C | 16 | 2 | 11 | 13 | 8 | 43 | 203 | 3,976 B | 292 K | 116 K | 202 K | 308 K | 128 | 128 | 104.5 | 86.1 |
| C13 † | WOTS+C / FORS+C | 22 | 2 | 19 | 7 | 8 | 43 | 208 | 3,688 B | ~10 M | 105 K | 188 K | 293 K | 128 | 128 | 128 | 128 |
| C12 | vanilla SPHINCs+ | 20 | 5 | 7 | 20 | 8 | 45 | - | 6,512 B | 36.6 K | 276 K | - | - | 128 | 127.8 | 109.1 | 95.4 |
| SLH-DSA-SHA2-128-24 | vanilla SPHINCs+ | 22 | 1 | 24 | 6 | 4 | 68 | - | 3,856 B | ~1.07 B | ~142 K | - | - | 128 | 128 | 128 | 128 |
| SLH-DSA-Keccak-128-24 | vanilla SPHINCs+ | 22 | 1 | 24 | 6 | 4 | 68 | - | 3,856 B | ~1.07 B | ~94 K | - | - | 128 | 128 | 128 | 128 |
- Family: the SPHINCS+ construction style (vanilla SPHINCs+ SPX, WOTS +). WOTS+C / FORS+C is the C-series compact construction with counter-grinding (ePrint 2025/2203). Plain SLH-DSA / SPHINCS+ is the standard FIPS 205 construction with no counter grinding: C12 and the two SLH-DSA-128-24 entries are the same algorithm at different parameter sets, with the SHA-2 row using the FIPS 22-byte ADRSc + SHA-256 hash.
- sign_h: hash-function calls during keygen + one signature, zero-memory signer (no inter-sign caching, the relevant case for a hardware wallet). A high number means a lot of work for the hardware. C12 the lightest is ~40 sec to sign on secure element.
- swn: small-Winternitz-number counter bits used by the WOTS+C / FORS+C grinding. Plain SPX and SLH-DSA don't counter-grind.
- sec_N: security bits at 2^N signatures per key. For SLH-DSA-*-128-24 (h=22, d=1) the hypertree is a single XMSS tree of only 2²² WOTS leaves, and the signing leaf is chosen pseudorandomly from the message digest, so WOTS-leaf collisions appear by the birthday bound (onset ~2¹¹ signatures), well before the named 2²⁴ usage cap. This is expected and absorbed by the FORS few-time layer (it is not a WOTS forgery); 128-bit security is carried with the FORS margin, not by one-time WOTS use. The "2²⁴" figure is therefore a recommended per-key usage cap, not a flat one-time-security guarantee. See docs/SECURITY-ANALYSIS.md for the budget/collision accounting. (review SLH-X-f2cap)
- Verify (pure): Foundry
gasleft()measurement of the assembly block. - Frame: total EIP-8141 frame-tx gas (ethrex). C12 / SLH-DSA-128-24 are not yet wired to frame accounts in this repo.
- 4337: total ERC-4337
handleOpstx gas (Sepolia). The 4337 wiring for C7 / C11 lives inSphincsAccount+SphincsAccountFactory; no SLH-DSA or C12 account exists here yet. - †: C13 uses the FIPS 205 §11.2.2 uncompressed 32-byte ADRS layout with keccak256, not JARDIN's. First verifier on the FIPS address layout (see the Address layout subsection below).
C13's parameter choice (h=22 d=2 a=19 k=7 w=8) was built around three goals: smallest signature, cheapest verify at full 128-bit security across the signature-count window, FIPS-aligned address layout. The numbers above bear out the design:
| Property | C7 | C11 | C13 | C12 | SLH-DSA-SHA2-128-24 | SLH-DSA-Keccak-128-24 |
|---|---|---|---|---|---|---|
| Sig size | 3,704 B | 3,976 B | 3,688 B ← smallest | 6,512 B | 3,856 B | 3,856 B |
| Pure-asm verify | 127 K | 116 K | 105 K ← cheapest at sec_20=128 | 276 K | 142 K | 94 K |
| Frame tx total (ethrex) | 210 K | 202 K | 188 K | n/a | n/a | n/a |
| 4337 handleOps total (Sepolia) | 318 K | 308 K | 293 K | n/a | n/a | n/a |
| Signature-count cap | 2²⁴ | 2¹⁶ | 2²² | 2²⁰ (h=20, d=5) | 2²⁴ ‡ | 2²⁴ ‡ |
| Security at the cap | 128 bit | 86 bit | 128 bit | 95 bit | 128 bit § | 128 bit § |
| Hash-call cost / sign (cold) | 4.3 M | 292 K | ~10 M | 36.6 K | ~1.07 B | ~1.07 B |
| ADRS layout | FIPS uncompressed | JARDIN | FIPS uncompressed | JARDIN | FIPS ADRSc | JARDIN |
‡ SLH-DSA-*-128-24 cap is a usage cap, not a leaf budget. h=22, d=1 ⇒ a single XMSS tree of 2²² WOTS leaves; the leaf is chosen pseudorandomly per message, so by 2²⁴ signatures leaves have been reused ~4× on average (and birthday collisions begin ~2¹¹). Unlike C7/C13, whose 2²⁴/2²² figures are the actual hypertree-leaf counts at full one-time-WOTS security, the SLH "2²⁴" exceeds its 2²² leaf space by design.
§ 128 bit at the cap is carried by FORS, not by WOTS one-time-ness. Pseudorandom leaf reuse is expected and absorbed by the FORS few-time layer (a=24, k=6); a leaf collision is not itself a forgery. See docs/SECURITY-ANALYSIS.md. (review SLH-X-f2cap)
Reading the table:
- vs C7: C13 holds full 128-bit security up to its 2²² cap (vs C7's 2²⁴), but verifies in 105 K vs 127 K (~17 % cheaper) and signs roughly half the hashes. Trade-off: half the signature-count budget per key. Good fit when keys rotate often or the per-key budget is bounded by policy.
- vs C11: Same security at sec_14 (128 bit), but C11 collapses to 86 bit at sec_20. C13 holds 128 bit all the way to sec_20. Cost: ~30× higher signer hash count (C13's a=19 FORS trees vs C11's a=11), but cheapest verify in the C-series.
- vs C12 (plain SPHINCS+ without counter grinding): C13 verifies ~2.6× cheaper for a comparable security envelope, with a sig that's ~44 % smaller. C12 wins decisively on signer cost (it has no counter-grinding step at all), so C12 stays the right pick for tightly-constrained signers (e.g. secure-element keys). C13 is the right pick when verify gas matters more than signer time.
- vs SLH-DSA-SHA2-128-24 (NIST-compliant standalone): C13 is roughly same sig size (-4 %) and ~25 % cheaper to verify, with ~100× lower signer cost. The trade is that SLH-DSA is the FIPS 205 NIST-blessed parameter set; C13 is a research parameter choice in the ePrint 2025/2203 family. C13's ADRS layout now matches FIPS to keep cross-impl porting clean.
- Smallest signature of any variant in the repo. The combination
k=7, a=19with the 4 B count tail and 11-level subtree gives the leanest payload.
The takeaway: C13 is the cheapest verifier in the repo at 128-bit security up to a 2²² sig cap, and the smallest signature. The cost is sign-time, which is ~30× C11 and ~2× C7. For an Ethereum smart account that signs occasionally and is verified by everyone, that asymmetry is the right shape.
C11 and C12 are light enough to run on a hardware wallet, 390s and 47.5s signature times on a ST33K1M5 secure element (Ledger nano S+). C12 has the lowest hardware signer cost of all (36 K hashes - plain SPX with d=5 hypertree skips most tree-hash work) at the price of a 6,512-byte sig. SLH-DSA-SHA2-128-24 is the FIPS-aligned alternative: much larger signer cost even on a desktop-class signer that caches the XMSS tree (~200 M hashes / sig, dominated by FORS, which can't be cached because the leaf-index to FORS-tree-address mapping changes with every message), and ~1.07 B / sig on a zero-memory signer that has to rebuild the 2²²-leaf XMSS for every auth path. 128-bit security across the 2²⁴ usage window is carried by the FORS few-time layer absorbing the expected pseudorandom WOTS-leaf reuse over the 2²² leaf space (‡/§ above; docs/SECURITY-ANALYSIS.md), not by one-time WOTS use. The SHA-2 verifier implements FIPS 205 external SLH-DSA.Verify with an empty context (M wrapped as 0x00‖0x00‖M before H_msg), so it matches published NIST/ACVP external KAT vectors. The Keccak twin trades bit-exact NIST compliance for ~34 % cheaper on-chain verification (but not a very interesting trade-off as it keeps the same signer cost).
The repo now ships only two ADRS layouts in src/, both straight out of FIPS 205: FIPS uncompressed 32 B for the keccak/SHAKE-family hashes (C7, C9, C13) and FIPS ADRSc 22 B for SHA-2 (SLH-DSA-SHA2). The keccak-family verifiers used to all share JARDIN's layout; C7/C9/C13 migrated to FIPS uncompressed, and the verifiers that stayed on JARDIN (C11, C12, and the keccak SLH-DSA twin) were retired to legacy/ rather than migrated. The JARDIN row below is kept for historical reference; those contracts are frozen, not part of the default build.
| Layout | Variants | ADRS bytes | Hash | F/H/T input |
|---|---|---|---|---|
| FIPS uncompressed 32 B | C7, C9, C13 (C13 first) | layer4 ‖ tree12 ‖ type4 ‖ word1·4 ‖ word2·4 ‖ word3·4 |
keccak256 | seed32 ‖ adrs32 ‖ payload |
JARDIN 32 B (retired → legacy/) |
C11, C12, SLH-DSA-Keccak-128-24 | layer4 ‖ tree8 ‖ type4 ‖ kp4 ‖ ci4 ‖ cp4 ‖ ha4 |
keccak256 | seed32 ‖ adrs32 ‖ payload |
| FIPS ADRSc 22 B | SLH-DSA-SHA2-128-24 | layer1 ‖ tree8 ‖ type1 ‖ 12 B type-dependent |
SHA-256 (precompile 0x02) | PK.seed(16) ‖ zeros(48) ‖ ADRSc(22) ‖ payload |
FIPS 205 §4.2 / §11.2.2 uncompressed 32-byte ADRS (the SHAKE-instantiation form):
bytes 0.. 4 layer address (uint32)
bytes 4..16 tree address (96 bits big-endian; top 4 B = 0 in current instances)
bytes 16..20 type (uint32)
bytes 20..24 word1 (type-dependent)
bytes 24..28 word2 (type-dependent)
bytes 28..32 word3 (type-dependent)
| type | name | word1 | word2 | word3 |
|---|---|---|---|---|
| 0 | WOTS_HASH | key_pair_address | chain_address | hash_address |
| 1 | WOTS_PK | key_pair_address | 0 | 0 |
| 2 | TREE | 0 | tree_height | tree_index |
| 3 | FORS_TREE | key_pair_address | tree_height | tree_index |
| 4 | FORS_ROOTS | key_pair_address | 0 | 0 |
JARDIN 32-byte ADRS (retired to legacy/; was used by C11/C12/SLH-DSA-Keccak; C7/C9 migrated off it): same 32-byte width, but with an 8-byte tree field (FIPS gives it 12) and four type-dependent words (FIPS uses three). The freed-up byte budget went to ci (chain_index) being a dedicated WOTS-only slot, while in FIPS chain_address and tree_height share word2 (same bytes, type-dependent meaning). JARDIN's 4th word (ha) is unused for every type in practice; the structural divergence from FIPS is the 8 vs 12 byte tree field.
Why C13 moved to FIPS uncompressed. "Reduce differences between families": FIPS-aligning the ADRS makes the keccak verifier port cleanly from a FIPS reference implementation, and pares the repo's address-layout inventory toward just two layouts (above). The hash stays keccak256; switching to SHA-256 would double on-chain gas (precompile staticcall vs native opcode) and would only be relevant if we needed full SLH-DSA-SHA2 family alignment, which we don't.
SLH-DSA-128-24 family, two wire-level layouts:
- SHA-2 variant: FIPS 205 §11.2.1 hashing, external SLH-DSA.Verify with empty context: ADRSc (22 B), SHA-256 via precompile, message wrapped as
M' = 0x00 ‖ 0x00 ‖ M(empty-ctx envelope), nestedHmsg = MGF1-SHA-256(R ‖ seed ‖ SHA-256(R ‖ seed ‖ root ‖ M'), m=21), big-endian (MSB-first) digest-to-indices (md[t] = BE(digest[3t..3t+3]), the FIPS 205 / current PQClean convention; not the legacy LSB-first SPHINCS+ reference). Matches published NIST/ACVP external KATs; signers prepend the same0x00 0x00. (review SLH-X-f1) - Keccak variant: JARDIN twin: 32-byte JARDIN ADRS (
layer4 ‖ tree8 ‖ type4 ‖ kp4 ‖ ci4 ‖ cp4 ‖ ha4), keccak256 primitive, F / H / T input =seed32 ‖ adrs32 ‖ payload, one-shotHmsg = keccak(seed ‖ root ‖ R ‖ msg ‖ 0xFF..FB)(no MGF1), LSB-first digest-to-indices on the 256-bit keccak output interpreted as a single big-endian integer.
The SPHINCS- verifier is deployed once and shared by all accounts. Follows the ZKnox/Kohaku pattern.
SPHINCs-Asm (deployed once, stateless, pure)
↑ verify(pkSeed, pkRoot, message, sig) → bool
│
├── SphincsAccount (4337) ← keys in storage, rotatable
└── FrameAccount (EIP-8141) ← keys in storage, rotatable
The account stores keys as immutables and passes them to the shared verifier on each UserOp.
EntryPoint.handleOps()
└── SphincsAccount._validateSignature()
├── ECDSA.recover(userOpHash, ecdsaSig) == owner
└── sharedVerifier.verify(pkSeed, pkRoot, userOpHash, sphincsSig) == true
The frame account has keys baked into its bytecode - no storage, no calldata overhead for keys. It receives sigHash + raw_sig, builds the full ABI call to the shared verifier internally, and calls APPROVE on success.
Frame Transaction (type 0x06)
├── Frame 0 (VERIFY): frame account builds verify(pkSeed, pkRoot, sigHash, sig)
│ from embedded keys + calldata → STATICCALLs shared verifier → APPROVE
└── Frame 1 (SENDER): ETH transfer / contract call
No ECDSA - pure post-quantum. Keys are stored in EVM storage (not bytecode) to support future key rotation via rotateKeys() - costs ~4K gas per verify but keeps the same account address across key changes.
BIP-39 mnemonic (12 or 24 words)
│
├──▶ HMAC-SHA512("sphincs-c6-v1", seed) → pkSeed, sk_seed (quantum-safe)
└──▶ BIP-32 m/44'/60'/0'/0/0 → ECDSA address (independent)
SPHINCs- and ECDSA are derived through independent paths - compromising one does not compromise the other.
| Signer | Language | Targets | BIP-39 |
|---|---|---|---|
script/signer.py |
Python | C-series (C7 / C9 / C11) | No |
signer-wasm/ |
Rust/WASM | C-series | Yes |
script/slh_dsa_sha2_128_24_signer.py |
Python (slow; ~hours at NIST params) | SLH-DSA-SHA2-128-24 | No |
script/slh_dsa_keccak_128_24_signer.py |
Python (slow; ~hours at NIST params) | SLH-DSA-Keccak-128-24 | No |
signers/sphincsplus-128-24/ |
C (forked from sphincs/sphincsplus ref) | SLH-DSA-SHA2-128-24 | No, seeds fed in |
signers/jardin-keccak-128-24/ |
C (sphincsplus fork + custom keccak + 32-B ADRS) | SLH-DSA-Keccak-128-24 | No |
# Rust WASM C-series signer
cd signer-wasm && wasm-pack build --release --target web
cargo test --release -- --ignored
# SLH-DSA-128-24 fast C signers (~11 min per NIST-params sign on pure C, no SHA-NI)
(cd signers/sphincsplus-128-24 && make)
(cd signers/jardin-keccak-128-24 && make)
# Python wrapper with disk cache; Forge FFI tests use these:
python3 script/slh_dsa_sha2_128_24_fast_signer.py <master_sk_hex> <message_hex>
python3 script/slh_dsa_keccak_128_24_fast_signer.py <master_sk_hex> <message_hex>EntryPoint v0.9: 0x433709009B8330FDa32311DF1C2AFA402eD8D009 (Sepolia)
New C13 SphincsAccountFactory instances and freshly-deployed accounts (each account funded 0.1 ETH):
| Chain | Contract | Address |
|---|---|---|
| Sepolia | SphincsAccountFactory | 0x8830d3... |
| Sepolia | SphincsAccountFactory (fresh) | 0x79FDD0... |
| Sepolia | SphincsAccount (ERC-4337 hybrid, C13) | 0x012801... |
| ethrex | SphincsAccountFactory | 0x874f5b... |
| ethrex | Frame account (EIP-8141, C13) | 0x253A4d... |
ethrex's
SphincsAccountFactoryis deployed for completeness, but EntryPoint v0.9 has no code on ethrex, so accounts created there are inert for ERC-4337. ethrex's functional PQ path is the EIP-8141 frame account. Full address record:script/.c13_addresses.json.
| Variant | Verifier | Account | Gas | Tx |
|---|---|---|---|---|
| C9 | 0x18F005... |
0xA94111... |
300 K | 0x8366513b... |
| C11 | 0xC25ef5... |
0x3C3b0c... |
308 K | 0x9fba169c... |
| C13 | 0xce176d... |
0xcef985... (factory 0xcaf5d2...) |
293 K | 0xbbf06456... |
C13 on Sepolia uses the FIPS 205 §11.2.2 uncompressed 32-byte ADRS (keccak256 hash). First verifier in the repo on the FIPS address layout. Standalone verify tx-level gas: 188,278. Full hybrid-4337
handleOpsUserOp gas: 292,727 (ECDSA recovery + C13 verify + 0.00001 ETH self-transfer throughSphincsAccount.execute). Seescript/.c13_addresses.jsonfor the canonical address record.
| Variant | Verifier | Deploy tx | Sample verify tx | Verify-tx gas |
|---|---|---|---|---|
| SLH-DSA-SHA2-128-24 | 0x9Fe417... |
0x09be3c59... |
0x00fa6b37... |
225,642 |
| SLH-DSA-Keccak-128-24 | 0x2Ac9Ec... |
0x253aa6dc... |
0x90d785a1... |
177,910 |
Verify-tx gas is the full top-level tx cost including 21 K tx base + ~63 K for the 3,872-B calldata payload; pure assembly execution is ~142 K (SHA-2) / ~94 K (Keccak). Keccak wins by ~21 % tx-level and ~34 % assembly-level because every F / H / T is a single native keccak256 opcode, while the SHA-2 variant pays a staticcall(0x02) dispatch per hash × ~280 hashes.
Older demo devnet at demo.eip-8141.ethrex.xyz (chain 1729): C9 / C10 / C11 frame accounts:
| Variant | Verifier | Frame Account | Gas | Verify | Tx |
|---|---|---|---|---|---|
| C9 | 0xc0F115... |
0xc96304... |
195K | 117K | 0x393588ec... |
| C10 | 0xD0141E... |
0x07882A... |
203K | 122K | 0x0a2571f8... |
| C11 | 0x315575... |
0x5bf5b1... |
202K | 122K | 0x053428f5... |
Current eip-8141.ethrex.xyz devnet (chain 3151908, Osaka fork, frame opcodes enabled from genesis; RPCs rpc1/rpc2/rpc3.eip-8141.ethrex.xyz):
| Variant | Verifier | Frame Account | Frame Gas | Sample Frame Tx |
|---|---|---|---|---|
| C13 | 0x659415... |
0xae3bA3... |
188 K | 0xabf3ce2f... |
EIP-8141 type-0x06 frame tx, two frames:
[VERIFY(frame_account, sigHash‖c13_sig, flags=approve sender+payer), SENDER(0x...dead, value=0.00001 ETH)]. The VERIFY frame's runtime staticcalls the shared C13 verifier andAPPROVE(0,0,3)s on success. Sender by the frame account itself (no protocol-level signature needed). Reproduce withscript/send_frame_tx_c13.py. Note: ethrex's on-chainFrameTransactionRLP layout differs from the draft EIP-8141 markdown by omitting thesignaturesfield: the script handles this; the deviation is documented inline.
forge build
pip install eth-account eth-abi requests pycryptodome
cd signer-wasm && cargo build --release# ── C-series (stateless hybrid + frame accounts) ───────────────────────────
# Deploy shared C-series verifier + SphincsAccountFactory (once):
forge script legacy/script/DeploySepolia.s.sol --rpc-url sepolia --broadcast
# Create account + send hybrid ERC-4337 UserOp (C7 / C11):
python3 legacy/script/send_userop.py create \
--factory <factory> --ecdsa-key $PRIVATE_KEY --variant c7
python3 legacy/script/send_userop.py send \
--account <account> --ecdsa-key $PRIVATE_KEY \
--to <recipient> --value 0.001 --variant c7
# ── SLH-DSA-128-24 (standalone verifiers, no account) ──────────────────────
# Deploy both SLH-DSA verifiers to Sepolia:
forge script script/DeploySlhDsa128_24Sepolia.s.sol --rpc-url sepolia --broadcast
# Build the fast C signer (used by Forge FFI tests, ~11 min per NIST-params sign):
(cd signers/sphincsplus-128-24 && make) # SHA-2 variant
(cd signers/jardin-keccak-128-24 && make) # Keccak variant
# Run the Forge end-to-end verify tests (first run triggers a real sign; later
# runs hit the disk cache at signers/*/\.cache/):
forge test --match-contract SLH_DSA_SHA2_128_24_Test -vv
forge test --match-contract SLH_DSA_Keccak_128_24_Test -vvforge test
cd signer-wasm && cargo test --release -- --ignoredThis repo ships a small Verity workbench under verity/. It models a strict
subset of the live Solidity verifiers and proves that each model refines a
functional spec. Source-to-model fidelity (the transcription of the
handwritten Solidity assembly into Lean) is a review and differential-testing
assumption; it is not itself a Verity obligation.
The Verity workbench currently models only two production verifiers:
src/SPHINCs-C13Asm.sol(keccak; the main production verifier). The model includes the public-key canonicality guard from the Solidity:pkSeedandpkRootmust each equal themselves masked byN_MASK, otherwise the verifier reverts withInvalid public key.src/SLH-DSA-SHA2-128-24verifier.sol(FIPS 205 external SLH-DSA, empty context, SHA-256 precompile).
The other live production verifiers, src/SPHINCs-C7Asm.sol and
src/SPHINCs-C9Asm.sol, are not modeled and not verified. Treat
them as unverified code. Any future Verity coverage would be a separate
change.
The C12 Verity model has been removed: C12 lives in legacy/ and is no
longer a production verifier. The old SphincsC6/, SphincsC6Full/,
SphincsC6V/, and SphincsKernel/ work, the verity/artifacts/ Yul
artifacts, and test/MerkleKernelVerityTest.t.sol have been removed from
this tree. After this change, no Verity artifact is exercised by Foundry;
nothing in verity/ is compiled into a production contract or replayed
in the test suite.
The Verity models in verity/SphincsMinusVerifiers/Model.lean are
hand-transcribed from the Solidity inline assembly. They mirror the
handwritten assembly structure (stacks, memory, and Yul revert fragments)
and use Verity's ABI-aware Bytes parameter locals (sig.length,
sig.offset).
- The models are not compiled into the production contracts.
- The models are not deployed.
- The models are not replayed in the Foundry test suite. There is no EVM-side regression test that takes the Lean model and runs it against the on-chain verifier.
- The proof target is model-to-byte-spec correspondence inside Lean. Correspondence between the model and the deployed code rests on the transcription itself being reviewed against the assembly.
verity/SphincsMinusVerifierSpec/Spec.leandefines the byte-level contract spec (ByteLevel.verifyBytes) and the abstract algorithmic spec (verifyParsed,verifySpec). The byte spec refines the algorithmic spec unconditionally:verifyBytes_eq_verifySpecandbyteVerifier_refines_specare proved with no assumptions beyondpropext.verity/SphincsMinusVerifierSpec/C13Concrete.leanandC13Mirror.lean(plus the matchingAxiomsfiles) provide the hand-codedPrimitivesinstances and concrete FORS / hypertree arithmetic that the algorithmic spec is checked against.verity/SphincsMinusVerifiers/Model.leanholds the hand-transcribed Verity models for the C13 keccak verifier and the SLH-DSA-SHA2-128-24 verifier.verity/SphincsMinusVerifiers/Proofs.leanis the per-verifier refinement surface, withc13_refines_specandslhDsaSha2_128_24_refines_specas the top-level theorems.
c13_refines_specis currently proved in Lean and rests on Lean's logic plus three named residual assembly axioms, all enumerated inverity/SphincsMinusVerifiers/AXIOMS.md. The keccak hashing in the C13 model is concrete (the interpreter's own pure Keccak), so no opaque primitive axiom remains on the C13 side. A follow-up PR is discharging the residual assembly axioms; once it lands,c13_refines_specwill rest on Lean's logic alone.slhDsaSha2_128_24_refines_specis proved in Lean but additionally keeps a named bridge axiom for byte-addressed memory modeling (the SHA-256 precompile path uses overlapping sub-wordmstores that the current word-keyed interpreter does not represent) and an opaque SHA-256 primitives constant.- A hand-held walkthrough of what SPHINCS- is, what a correct verifier must check, and how the proof is structured is at https://lfglabs.dev/research/sphincs-minus-verifier.
The full remaining trust surface (every named bridge axiom, opaque
primitive, and residual assembly axiom) is enumerated in
verity/SphincsMinusVerifiers/AXIOMS.md. Cryptographic security of the
scheme itself (hash collision resistance, EUF-CMA) is an assumption
outside the proofs, not a Lean axiom; the theorems establish
implementation correctness only. The README is worded so it
stays true in both proof states: as of today, and after the residual
assembly obligations are discharged.