zkDaily - 2026-03-28

零知识证明 zkDaily

ZKP Frontier Tracker 🎯

Sat

03.28

2026

CatCrypt: From Rust to Cryptographic Security in Lean

Paper

https://eprint.iacr.org/2026/604

Bas Spitters Lean Rust AI

Bas Spitters proposed the CatCrypt library in their paper, offering an end-to-end pipeline from Rust reference implementations to security proofs in Lean's computational model, covering 172 cryptographic protocols with AI-accelerated development.

Notes

Offers machine-checked security proofs, covering 172 protocols with 110 having full Rust-to-Lean pipelines.
Uses Hax tool for Rust-to-Lean translation, ensuring consistency between implementation and proofs.
All bounds systematically cross-referenced against sources like IETF RFCs, NIST standards, and academic papers.
Some proofs ported from SSProve and EasyCrypt; most are independent formalizations without prior machine-checking.
Developed in two months vs. traditional months of expert effort, accelerated by GenAI assistance.
Addresses AI hacking, AI-generated software, and post-quantum security challenges via formal methods.

Collected by @icerdesign

零知识证明 zkDaily

Q&A Deep Dive 💬

Sat

03.28

2026

Why is translating from Rust to Lean important?

Rust is used for implementation, while Lean is used for formal proofs. Translating ensures that the implementation matches the proof, avoiding mismatches between code and security guarantees.

How does CatCrypt achieve end-to-end verification?

It uses the Hax tool to translate Rust code into Lean, then proves security in the computational model. This allows verification of real implementations rather than abstract models.

What is the key role of AI in CatCrypt’s methodology?

AI accelerates proof generation and translation, drastically reducing development time. However, it introduces risks, so cross-referencing and validation against standards are used to ensure correctness.

Prompted by @icerdesign