The paper describes the design and philosophy of a mask verification language (MVL) and its compiler. Mask verification tools have to be programmable, because of the large software investment they require, and the speed at which fabrication technology changes. The language described here allows a designer to specify the topological structure of a device (the device description), and to attach to it a procedure to be executed when that device is recognised (the device procedure). The device procedure allows certain geometric qualifications to be placed on the structure. (The device description and procedure, taken together, form a device declaration.) In general, an MVL program will contain several device declarations: one for each realisable type of device of a technology. The description part of a declaration is asynchronous, and the procedural part, which is internally sequential, is executed once for each instance of the device description located on the mask set. Careful choice of the primitives provided allows extensive optimisation of the leaf operations involved, which is extremely important, given the usual size of the mask data-sets.