Undetectable counterfeiting is the bug Zcash is trying to prove impossible, by formally verifying Ironwood's shielded pool.

zkGolf is a competition for building the cheapest zero-knowledge circuits, with correctness proved in Lean 4.

IETF TLS last-call thread on ML-KEM in TLS, with the usual calls for actual attacks and less hand-waving.

Need Yul semantics in Lean? This repo gives big-step semantics, an executable interpreter, and a verified Fibonacci demo.

zk.golf turns circuit golf into a competition, with Lean proofs and a Clean-based submission pipeline.

Blockstream's Simplicity site relaunch, with Liquid mainnet status, proof-before-deployment notes, and contract examples.

Paper on Hema, a formally verified mutual attestation protocol for same or mixed TEEs, since one attestation stack was not enough.

Lean's ArkLib post, formal verification for SNARKs and arguments of knowledge, for people who enjoy proving proofs.

DV Club Zurich 2026 talks and slides on verifying RISC-V, SoCs, crypto extensions, and connected devices, because silicon loves bugs.

Tweet on Ironwood circuit verification and Zcash upgrade timing, with the usual reminder that consensus waits for nobody.

CFP for CT-RSA 2027's Cryptographers' Track, a grab bag of crypto/ZK topics and SoK papers, as conference season does.

Long essay on Hilbert's axioms, then somehow hashes, TLA+, Circom, OPA, SHAP, and SBOMs end up in the same security sermon.

So Cryspen spun out CE Labs for cryptographic engineering, and kept the formal-verification plumbing in-house?

Semantic Non-Assembly says exposed components can stay useless if no sub-threshold coalition can assemble the predicate.

Sound bounds on AI-agent policy violations under probabilistic transitions, via DRO, because independence was too optimistic.

The annoying bit was an implicit carry bound, and they proved a Plonky2 U32AddManyGate in Lean after exporting Rust constraints.

Auto-generates Tamarin models from a DSL and ties them back to code, because hand-writing protocol proofs was still too pleasant.

The cheapest audit quote is usually the wrong one, this guide shows how to vet crypto, ZK, and smart-contract auditors.

Vitalik’s take on formal verification, with Lean examples and a sober look at where end-to-end proofs still blow up.

ePrint on faulting the forward NTT in ML-KEM/ML-DSA, with exact rank/kernel leakage bounds and a Lean 4 proof.

ProVerif says standalone ML-KEM is one brittle point of failure; hybrid TLS 1.3 keeps working if either half survives.