Introducing Frml

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 one. Frml is aimed at experienced programmers: you should understand basic Boolean logic (and, or, not, implication) and already know what a lexer, parser, and abstract syntax tree (AST) are, but you need no prior background in formal verification. The big picture Frml’s lexer and parser turn program text into an AST, and the typechecker rejects programs with type errors. The prover then turns the AST…