Posts tagged #formal-verification
-
Zero-Sorry Discipline: What a Lean 4 Appendix Actually Costs
Two theorems in this paper — MoEGauge and JensenFloor — had to reach zero sorries before the paper shipped. What that process looks like, why sorry is dangerous, and what JensenFloor actually says.
-
A Survey as a Living Document
What it means to maintain a formal proof corpus that stays in sync with its own coverage badge, and what happened when RWKV was added as a new architectural family without invalidating existing theorems.
-
Lean 4 as a Soundness Oracle for Security Properties
Type stubs catch misuse at type-check time. But can we prove they are sound — that a well-typed program cannot trigger the dangerous code path? Enter Lean 4.