Search results

Idea: using co-induction to describe matrices

Status: Open.

#83 In formal-land/garden;

· clarus opened on Sep 26, 2025

Terminate Keccak verification

Status: Open.

#81 In formal-land/garden;

· clarus opened on Sep 14, 2025

Full translation of OpenVM's sha256

OpenVM

Status: Open.

#76 In formal-land/garden;

· clarus opened on Aug 29, 2025

Blake3: determinism for eval

Status: Open.

#66 In formal-land/garden;

· clarus opened on Aug 13, 2025

Blake3: determinism for verify_round

Status: Open.

#65 In formal-land/garden;

· clarus opened on Aug 13, 2025

Blake3: determinism for full_round_to_diagonal_quarter_round

Status: Open.

#64 In formal-land/garden;

· clarus opened on Aug 13, 2025

Blake3: determinism for full_round_to_column_quarter_round

Status: Open.

#63 In formal-land/garden;

· clarus opened on Aug 13, 2025

Blake3: determinism for quarter_round_function

Status: Open.

#62 In formal-land/garden;

· clarus opened on Aug 13, 2025

Plonky3: Plans on Verifying Soundness

Status: Open.

#47 In formal-land/garden;

· YunkaiZhang233 opened on Jul 15, 2025

Linea: verify a first example

Status: Open.

#41 In formal-land/garden;

· clarus opened on Jun 16, 2025

Note: Ideas for Formalization

Status: Open.

#33 In formal-land/garden;

· InfiniteEchoes opened on Jun 12, 2025

Keccak: verify the verifier: no over-constraints

Status: Open.

#29 In formal-land/garden;

· clarus opened on May 27, 2025