EIPsInsight

Loading Experience

Preparing your insights...

Loading0%
EIPsInsightEIPsInsight
Sign in
All protocol calls
Previous
PQTS2026-06-24_011

PQ Transaction Signatures #011

2026-06-24 1 decision 323 transcript lines

Transcript

Ask about this call

Answered from this call's summary and transcript only.

AI-generated — verify against the recording.

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

Meeting chat6

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

Links