A few months ago I set out to learn how program verification works. I tried Lean and Dafny, but kept wondering how verification actually worked. To find out, DeepSeek and I built Frml, which is a very simple imperative language with its own verifier. This post walks through the Frml verification engine, explaining how a Frml program becomes Boolean logic that the Z3 solver can check, and what Z3 does with that logic. The language and its verifier are layered: the scalar level handles straight-line and branching code with no functions or loops, while successive levels add features one by...