Issues

• Idea: using co-induction to describe matrices

  formal-land/garden#83 · Filter by author clarus opened on Sep 26, 2025

• Terminate Keccak verification

  formal-land/garden#81 · Filter by author clarus opened on Sep 14, 2025
  

• Full translation of OpenVM's sha256

  OpenVM
  formal-land/garden#76 · Filter by author clarus opened on Aug 29, 2025

• Blake3: determinism for eval

  formal-land/garden#66 · Filter by author clarus opened on Aug 13, 2025

• Blake3: determinism for verify_round

  formal-land/garden#65 · Filter by author clarus opened on Aug 13, 2025

• Blake3: determinism for full_round_to_diagonal_quarter_round

  formal-land/garden#64 · Filter by author clarus opened on Aug 13, 2025

• Blake3: determinism for full_round_to_column_quarter_round

  formal-land/garden#63 · Filter by author clarus opened on Aug 13, 2025

• Blake3: determinism for quarter_round_function

  formal-land/garden#62 · Filter by author clarus opened on Aug 13, 2025
  

• Plonky3: Plans on Verifying Soundness

  formal-land/garden#47 · Filter by author YunkaiZhang233 opened on Jul 15, 2025
  3

• Linea: verify a first example

  formal-land/garden#41 · Filter by author clarus opened on Jun 16, 2025
  1

• Note: Ideas for Formalization

  formal-land/garden#33 · Filter by author InfiniteEchoes opened on Jun 12, 2025

• Keccak: verify the verifier: no over-constraints

  formal-land/garden#29 · Filter by author clarus opened on May 27, 2025
  

• The roles of constraints vs circuits, and relationship between prover and verifier in Rocq proofs.

  formal-land/garden#22 · Filter by author YunkaiZhang233 opened on Apr 28, 2025
  1

• Blake3: Formally Specify and Verify the Blake3 Hashing Algorithm

  formal-land/garden#17 · Filter by author YunkaiZhang233 opened on Apr 18, 2025

• Circom: more primitive operations to read/write variables

  circom
  formal-land/garden#15 · Filter by author clarus opened on Jan 26, 2025
  

• O1: verify the theta operation

  o1
  formal-land/garden#5 · Filter by author clarus opened on Dec 24, 2024
  

• O1: specify the theta iteration

  o1
  formal-land/garden#4 · Filter by author clarus opened on Dec 24, 2024