Post Quantum transaction signature #11

Protocol Calls & happenings
1

Agenda

  • FORS contract formal verification - Ricardo Perello

Meeting Time: Wednesday, June 24, 2026 at 13:00 UTC (60 minutes)

GitHub Issue

2

Meeting Summary:

This was the 11th occurrence of a post-quantum cryptographic meeting focused on formal verification, where Ricardo presented his successful attempt to formally verify the first contract developed by Riva Labs using the Forest+Sea verifier. Ricardo demonstrated how he verified that the contract’s recover function correctly identifies signers for every possible input by comparing the Yul implementation with a Lean reference model using EVM Yulen tools. The discussion revealed that while the current proof shows the assembly code is correctly implemented, there are concerns about the ground truth of the reference implementation, which was partially AI-generated, and participants suggested expanding the verification to include security proofs for the signature scheme. Yoichi and Benedikt provided insights on formal verification approaches and security definition frameworks that could strengthen the foundation of the verification work.

Click to expand detailed summary

The meeting was the 11th occurrence of a post-quantum cryptography discussion series held every two weeks. The main focus was on formal verification, with Yoichi, a world expert in the field, attending as a leading expert. Ricardo was scheduled to present his work on formally verifying the first contract by Riva Labs, though the presentation portion had not yet begun when the transcript ended.

Ricardo presented his work on formally verifying the Forest Plus Sea verifier contract developed by Riva Labs. He explained that the verification focused on proving the contract correctly recovers signatures for every possible input, using EVM Yulen tool from Nethermind to compare the Yul implementation with a clean model in Lean. The proof assumes the Solidity compiler’s backend is trusted and covers the assembly reconstruction of the signature, but does not claim unforgeability of the signature itself. Next steps include proving that the on-chain bytecode matches expectations and exploring whether an efficient contract can be derived from the Lean model.

The team discussed the purpose of address recovery operations in their smart contract wallet system, with Matteo explaining that it verifies the public address used for signing transactions matches what is stored in the wallet. Yoichi inquired about the need for both recovery and valid signature operations, leading to a discussion about formal verification efforts using Sphinx to prove the entire signature scheme. Ricardoperello mentioned that there is ongoing work to prove the signature scheme with Sphinx, with integration into the wallet being a future step.

The team discussed the complexity of code analysis and verification processes. Yoichi inquired about the nature of case analysis in the code and the number of proofs generated by AI. Ricardoperello confirmed he assumed k-check was working correctly, though Antonio noted it had been in the EVM for years and wasn’t entirely bug-free. Antonio raised a question about whether the comparison method used by Ricardoperello was appropriate, particularly given his experience with formal verification.

The discussion focused on how RivaLabs implemented their Solidity contracts and Lean verification. Alessandro explained that their main implementation was written directly in Solidity, with some AI-assisted Lean implementation done experimentally, but not extensively. The team aimed to create a simplified Solidity version that would match the bytecode verified by Lean, though they acknowledged this goal was not fully achieved yet due to various technical complexities.

Ricardo discussed different approaches to proving CVM bytecode, determining that directly proving EVM bytecode inside the EVM Yulin is the simplest option rather than formally verifying the compilation process. Matteo agreed with this approach and mentioned that Verity provides a clean CDSL sub-language for deploying bytecode. Antonio noted that the full verification of strings has already been accomplished by the Verity team, though the details were incomplete in the transcript.

The team discussed progress on formal verification work, with Antonio expressing satisfaction while emphasizing the need for a reliable ground truth. Yoichi suggested using Lean specifications to verify the recover function rather than reading URL code or bytecode, and proposed adding security proofs to strengthen confidence in the ground truth. Benedikt mentioned a new VCVIO paper that provides a framework for formalizing security definitions and proofs of signature schemes in Lean. The group agreed to focus on proving security assumptions about the Keccak hash function rather than just verifying EVM bytecode, with plans to reconvene in two weeks.

Next Steps:

  • ricardoperello: Investigate and attempt to prove security assumptions about the signature scheme in Lean, specifically showing that breaking the scheme implies breaking Keccak.
  • ricardoperello: Explore proving that the EVM bytecode (not just the optimized YUL) matches the expected implementation, using EVM Yulinen tools.
  • Antonio: Follow up with ricardoperello to discuss further collaboration on the project, focusing on the security assumptions proof.

Recording Access:

3

YouTube recording available: https://youtu.be/2NpQMjtVFuo