Verification is runtime

[Erhannis]

The docs say all over that verification happens at compile time, but when I try e.g. the following, derived from the example in the docs:

import std::io

public export method main():
    Microwave m = {
        heatOn: false,
        doorOpen: false,
        timer: 0
    }
    closeDoor(m)
    io::println("Hello World")

type nat is (int x) where x >= 0

// First, define the state of the microwave.
type Microwave is ({
    bool heatOn, // if true, the oven is cooking
    bool doorOpen, // if true, the door is open
    nat timer // timer setting (in seconds)
} m) where !m.doorOpen || !m.heatOn

function closeDoor(Microwave m) -> Microwave
requires m.doorOpen:
    m.doorOpen = false
    return m

// A door opened event is triggered when the sensor detects that the door is opened.
function openDoor(Microwave m) -> Microwave
requires !m.doorOpen:
    m.doorOpen = true
    m.heatOn = false
    return m

// Signals that the "start cooking" button has been pressed.
function startCooking(Microwave m) -> Microwave
requires !m.doorOpen:
    m.heatOn = true
    return m

wy build completes with no errors, but wy run throws a runtime exception on closeDoor(m). Why?

The docs also occasionally say "when verification is enabled", so maybe it's an opt-in feature, but I have yet to find anywhere that explains how to enable verification. Given that, quote, "an important feature of Whiley is verification", I'd expect that to be more up-front. If the problem is that it's disabled, how does one enable verification?