We are developing a framework for cryptographic proofs in Lean.
At this point, the project is still in development and quite undocumented.
In case of questions, do not hesitate to contact us (Dominique Unruh, Denis Firsov).
The project is named after the crypt of Gaudí’s Church of Colònia Güell, known for its leaning pillars.