A Cap Makes Brute Force Win
We aimed our own IC3/PDR model checker at the split-brain proof expecting it to beat explicit-state enumeration. It lost — because the lease guard caps one quantity, and that collapses the space brute force has to search.
warp-types¶
Intervals Collapse to Points
What happens to formal verification when the hardware is deterministic.
The Bug That Wasn't There
A one-line soundness hole that zero tests caught and zero users triggered.
What the Type Erases To
A type system that compiles to nothing is not overhead you tolerate — it is proof the compiler can verify and then discard.