PQTS2026-06-24_011
PQ Transaction Signatures #011
2026-06-24 1 decision 323 transcript lines
Transcript
- Gustavo Frederico
Can we access the video of a previous meeting?
- Antonio Sanso
Sure is in the ethereum YouTube channel
- Antonio Sanso
Let me find the link
- Antonio Sanso
- Gustavo Frederico
Reacted to "https://www.youtube...." with ✅
- Antonio Sanso
Reacted to "https://www.youtube...." with ✅
Call summary
Decisions
- •Priority: proving security assumptions (ground truth strength) ranked higher than completing Yul→bytecode verification gap - 00:51:07
Highlights
- Formal Verification Progress:
- ·Ricardo (EPFL student) formally verified Riva Labs' FORS+ verifier contract in Lean4 via EVMYulLean (Nethermind tool), proving correct address recovery for all possible inputs - 00:18:39
- ·Proof runs on optimized Yul IR, not EVM bytecode — Solidity compiler backend (Yul→bytecode) remains trusted but unverified - 00:21:39
- ·AI used to write Lean4 proofs and reference model; correctness relies on Lean kernel, not AI output. Riva Labs' reference Lean model also AI-assisted from Solidity + FORS+ context - 00:26:46
- ·Verity team reportedly achieved full formal refinement of SPHINCS+; separate effort to formally verify SLH-DSA wallet integration is in progress - 00:44:55
- Verification Scope And Limitations:
- ·Contract proves which address signed — validity check (recovered address == expected address) must be done by the calling contract; unforgeability not claimed - 00:20:09
- ·keccak assumed correct (long-standing EVM primitive); not formally verified in this work - 00:34:00
- ·Ground truth risk: Lean reference model derived from Solidity+AI; manual review needed to confirm it matches NIST/FIPS specification intent - 00:35:09
- ·Yoichi: security proof anchoring recover function to hash pre-image hardness would strengthen confidence in Lean spec independent of PDF comparison - 00:46:19
- ·Benedikt: CryptHOL framework (Lean4) enables formalizing asymptotic and concrete security proofs for hash-based signatures; security definition itself still needs human review - 00:47:21
Action Items
- •Ricardo Perello / Riva Labs - Extend verification to cover EVM bytecode (not just optimized Yul), and add security reduction proof (breaking FORS+ implies breaking keccak pre-image) - 00:50:24
Key decisions
Priority: proving security assumptions (ground truth strength) ranked higher than completing Yul→bytecode verification gap
Prioritizing proving security assumptions over completing Yul→bytecode verification gap