Lean 4.29.0 released with 453 changes.

Highlights: reduced startup time through static initialization of closed terms, simpler 𝚗𝚘𝚗𝚌𝚘𝚖𝚙𝚞𝚝𝚊𝚋𝚕𝚎 semantics improving predictability, higher-order Miller pattern support in 𝚐𝚛𝚒𝚗𝚍's e-matching engine, and a significant overhaul to instance and reducibility handling.

Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.29.0/

#LeanLang #LeanProver #FormalMethods

If your security depends on someone reacting in time,
you don’t have a guarantee. You have coordination.

Wrote about a real failure mode that keeps showing up.
https://app.daily.dev/posts/yqybiiFvJ

#blockchain #smartcontracts #security #formalmethods #web3 #cryptography #defi #ethereum #protocoldesign

fly51fly (@fly51fly)

대규모 언어모델을 활용한 형식적 반례 생성 연구 'Learning to Disprove: Formal Counterexample Generation with Large Language Models'가 소개되었다. 정리·검증이 필요한 수학/논리 문제에서 LLM을 반례 생성 도구로 쓰는 새로운 연구 방향을 제시한다.

https://x.com/fly51fly/status/2036199167882830168

#llm #research #formalmethods #counterexample #arxiv

TLA+ mental models

https://fed.brid.gy/r/http://muratbuffalo.blogspot.com/2026/03/tla-mental-models.html