It might not be super clear for people who don't know about formal verification with Lean or about arithmetic circuits, but this project let's you optimize code in a secure way: if you have code that's faster, not only you have a proof that it is indeed faster, but you also have a proof that it is correct and secure by construction!

It's important that the circuits implement the logic "securely" because arithmetic circuits are used in cryptography (in ZKP, MPC, FHE, for example) to implement programs with additions and multiplications (instead of NAND gates for example)

Show HN: https://news.ycombinator.com/item?id=48763246