It is
@leolarav but I know that
@leonardoalt also have done or is doing some FV. I take the confusion as a compliment.
If you need an really executable and usable Lean4 SSZ look into us, it is free software and we are very collaborative. Built by a humble volunteer team of already 5 people. (like
@IvanAnishchuk)
We have not completed the formal verification of our implementation (although I would say it is 90%), because in
@invisiblgarden philosophy we are using it as a learning tool. Ethereum Protocol Fellows and IG fellows are adding them.
However, it is very fast, we implemented "toggleable caching" for the merkle tree intermediate hashes, like remarketable, using implied type classes and meta programming.
The result, disabling the cache makes the code simple and easy to create proofs for it. Enabling the cache makes it very fast.
Soon we will publish benchmarks.
Thanks to metaprograming, it is trivial to use it, just derive SSZRepr in your struct. Zero builerplate: you get de/ser, Markle Root (with C or Lean hash), and cache that you can disable for simple proofs.
Also, it works with a C implementation of sha256, or with a Lean implementation.
github.com/etheorem/etheorem…