PresenceLock is a small Windows utility: a webcam watches for your face, and when you step away and the machine goes idle, it locks the session. A camera-based take on Windows Dynamic Lock.

Before anything else, what it does with the video. Everything runs locally. Frames are read, checked for a face, and dropped. Nothing is stored and nothing leaves the machine. The decision logic never sees a pixel. The whole observation type it receives is this:

type Observation =
    | FaceSeen
    | NoFace
    | NoFrame
    | DarkFrame

That type is the boundary. Everything this post is about lives on the far side of it.

TL;DR

The decision to lock is a pure F# function of explicit state, config, time, and one event. The C# shell owns the camera, the detector, and the Win32 lock call, and does nothing else. This bought three things. Three times the tool silently stopped locking while its status said it was watching, and each bug was found and fixed as a pure function with no camera involved. The dangerous zero value of the environment sample is unrepresentable, because the type was chosen so that its default is null. And the reachable state space is small enough to close by breadth-first search, so the invariants are checked everywhere, not sampled.

The shape

The decision core (PresenceLock.Core, in F#) makes every call as a pure function: when to lock, when not to, when to ask for a restart. It has no clock of its own and does no I/O. The C# WinForms shell samples the world, calls the core, and executes whatever single action comes back.

let step (config: PolicyConfig, state: State, ctx: StepContext, event: Event)
    : StepResult

StepContext is the world right now: the monotonic clock, the wall clock, and a StepInputs record holding whether the session is locked, whether the user paused the tool, whether a lock inhibitor is active, and how long input has been idle. Event is the reason the call happened: a camera sample, a camera failure, or a plain “the levels changed, re-derive”. The result is a new state and exactly one Action, from a three-case union: nothing, lock, or restart the process.

Two of those inputs need a word. Suppression (paused, or session already locked) freezes sampling at the top of the pipeline, and nothing is decided while it holds. Inhibition lets the whole pipeline run and vetoes only the final lock. The first shell-side inhibitor is “media is playing”. The two words are near-synonyms in English, and in this codebase they name opposite ends of the pipeline.

Three bugs that looked healthy

A lock utility fails in a specific way. Lock when you shouldn’t and it’s annoying. Fail to lock after you’ve walked away and the tool has stopped doing its one job, and the worst version of that is when the tray icon still says “Watching”. All three of these happened.

Burn-in, July 2026. Windows’ FaceDetector produces threshold-flicker false positives on an empty scene, made worse by the auto-framing crop hunting around looking for something to frame. One stray FaceSeen reset the away clock, and the app never locked. The asymmetry was the bug: absence already had to persist for the whole away threshold before it counted, but presence flipped on a single noisy sample. The fix is a pure sibling module, PresenceFilter, that counts presence only after an unbroken run of spatially coherent detections (bounding boxes overlapping from one sample to the next) has spanned a minimum of monotonic time. The bounding box was data the detector had been returning all along and the shell had been throwing away.

Frozen frames. The WinRT frame reader can re-serve the same cached frame forever. A stale frame carrying a stale FaceSeen reset the away clock indefinitely. The tell, a frame timestamp that had stopped advancing, was already being logged by a parallel counter. It just never reached the decision path. The fix is another pure sibling, FrameFreshness, which tracks whether the source’s own timestamp is still moving and, after five seconds frozen, classifies the sample as if no frame had been acquired at all. That needs no new recovery mechanism, because the existing no-signal handling already does the right thing from there.

Folded belief, August 2026. The first design delivered session lock and pause to the core as edge events, and the core folded them into belief flags, with a hand-written truth table over every ordering. The sequence was: pause, then session lock, then session unlock, then resume. At the end of it the core believed the session was still locked while the user sat in an unlocked session, and nothing would ever correct it, because a folded belief has no way to re-synchronize with the truth. This was specified and tested behavior. Every property test derived from that truth table inherited its blind spot. The fix was to stop folding: the session and pause facts are now sampled fresh on every step, and the harness described below exists so the next trap of this shape becomes a failing test instead of an incident.

The first two fixes are time-based rather than count-based, on purpose. A count ties its meaning to the sample interval, and one dropped detection under fast sampling would cost more re-stabilization time than the away clock, measured in real time, gives back. That class of bug had already been fixed once for every other threshold in the codebase.

None of the fixes touched the camera code. All three were written and tested as pure functions, in a container, without Windows. That is the whole argument for the split, in three incidents.

Pick the representation whose default value is invalid

The environment sample, StepInputs, is a plain reference record and deliberately not a struct. The comment on the type says why better than I did the first time.

As a struct, its zero-initialized default reads as “not paused, not locked, no inhibitor, input idle”. That is a plausible state. It is also exactly the state that says the user has gone, lock the screen. And it is reachable through paths no call-site discipline can guard: Array.zeroCreate, a dictionary miss, Unchecked.defaultof, an uninitialized field. As a reference type, every one of those paths yields null and throws on the first field access. A missing sample fails loud instead of quietly deciding you’ve left.

The general rule transfers to any language with zero-initialization: when a type’s default value would be a plausible but dangerous input, pick the representation whose default is invalid. F# makes the choice a one-word difference, [<Struct>] or not.

Time is a parameter, and it’s typed

Every now is passed in. There are two clocks, and they are different types:

[<Struct>] type MonotonicMs = MonotonicMs of int64   // boot-relative, TickCount64
[<Struct>] type WallClockMs = WallClockMs of int64   // Unix epoch, survives reboots

Monotonic time drives the grace and away timers. Wall-clock time drives only the restart cooldowns, which have to stay meaningful across a reboot, because a wedged camera does not get better after one. Passing a WallClockMs where a MonotonicMs is expected is a compile error. They are real struct types rather than [<Measure>] units on purpose. A unit erases to a bare int64 at exactly the C# boundary where the transposition risk lives, and a distinct struct survives it, so the guarantee holds in both languages.

The state is opaque, and truth is sampled

State is a public type, because the shell has to hold one and thread it through, but its representation is internal. The shell can’t construct one, can’t pattern-match it, can’t hand-roll a state that lies. The only window in is snapshot, a read-only projection for logging and tests.

Whether the session is locked or paused is sampled fresh on every step, never accumulated from events. That is the scar from the third bug above. Sampled truth can’t drift, because there is nothing to drift from. The previous sample does live inside the opaque state, for deriving edges, and it lives there rather than in a shell-held pair so that it has exactly one writer.

Which way to fail

For a lock decision, the safe failure is not locking. A bad frame (none, or too dark) resets the away timer exactly as a face does, so a camera hiccup never locks the screen by itself. A camera that stays bad past a threshold surfaces as a distinct no-signal status and, past a longer one, asks the shell for a process restart. The StepInputs guard above exists so that a zero-initialization path can’t silently pick the other direction.

The camera you cannot re-initialize

The restart in that last paragraph is the part of the project I would least like to learn again. Tearing down and re-initializing the capture pipeline inside the process can wedge the camera. In the milder case the process’s own connection to the Windows Camera Frame Server is what breaks, and every init in that process fails with E_HANDLE until a fresh process starts. In the worse case the service itself wedges, machine-wide, and stays that way until it is restarted with elevation. The damage is outside the process and survives the process’s death. A fresh process’s first init is the only reliable re-initialization on the affected hardware.

For a while that was a rule people had to remember. Then it became a rule the code can’t break. The in-process re-init paths were deleted in a single commit, and every remaining path to camera initialization is gated on there being no reader yet, so acquisition is reachable only from process start and from the retry loop before the first success. Recovery is always a clean process restart, decided by the core as an Action.Restart with a reason, executed by the shell, and rate-limited by wall-clock cooldowns that survive the restart. Switching cameras in settings restarts the process too, for the same reason.

The invariant is stated in the architecture doc, but the doc is not what enforces it. Removing the ability to violate it was the fix, because remembering it was not good enough. The full story, including how the restart is kept from looping, is its own post .

Testing a core that can’t touch Windows

There are ordinary xUnit scenario tests and FsCheck property tests over the decision logic. The part worth describing is the model-based harness on top.

An explorer does breadth-first search over the reachable graph of environment levels crossed with an abstraction of the core state, checking the invariants at every node. The search closes on its own: the queue empties at depth 12 with 2,272 nodes reached in about 120 milliseconds, against a depth bound of 16 that exists only as slack. That is the whole space reachable under the harness’s action alphabet at the default config, not a sample of it, which is what lets the harness promise that any future absorbing “silently cannot lock” trap becomes a failing test instead of an incident.

The harness also runs two mutants, and the opacity of State is what makes them meaningful. A mutant cannot reimplement the decision logic, because it has no way to build a State. Every alternate implementation must delegate to the real start and step for the state component. Its only lever is what it feeds them. So a mutant differs from the real thing the way the real bug did: by feeding a correct core the wrong inputs. The first mutant feeds it a folded view of the session and pause flags derived from consecutive samples, which is the pre-RFC architecture, and the explorer finds the incident’s trace. The second freezes the inputs it passes while the environment is suppressed. That is a different mechanism, one the new design could have had, arriving at the same swallowed-edge symptom, and the explorer rejects it too.

If property and exhaustive testing is your thing, it’s the same instinct behind nelli , my Nim testing engine: different language, same conviction that the core should be the easiest part to verify.

Takeaway

None of this is exotic F#. It’s records, unions, a couple of single-case struct types, and functions with no side effects. That kit was enough to make the lock decision the simplest, most-tested code in the project, and to make the two times it silently failed into the two easiest bugs to fix. For a thing whose job is to lock your screen when you leave, that is the only way I wanted it.

Code is at github.com/coreyleavitt/presence-lock (Apache-2.0). The design records are in the repo under docs/rfc/, and the invariant list is in ARCHITECTURE.md.