Owl

Runtime verification for Gleam on the BEAM. Owl monitors running actor systems against safety properties using sHML (safety Hennessy-Milner Logic) and the BEAM's native tracing infrastructure.

Requirements

• Gleam >= 1.0
• Erlang/OTP >= 26

Installation

Add Owl as a dependency in gleam.toml:

[dependencies]
owl = { path = "../owl" }

Quick Start

import owl
import owl/markers
import owl/trace/controller

// 1. Define marker functions in your app (zero-cost no-ops)
// File: src/my_app/owl_markers.gleam
pub fn mark_login() { Nil }
pub fn mark_transfer() { Nil }

// 2. Call markers at lifecycle points in your app
// File: src/my_app/bank.gleam
pub fn login(user) {
  let _ = owl_markers.mark_login()
  // ... login logic
}

pub fn transfer(from, to, amount) {
  let _ = owl_markers.mark_transfer()
  // ... transfer logic
}

// 3. Define safety properties
// File: src/my_app/monitors.gleam
fn is_transfer(event: owl.TraceEvent) -> Bool {
  markers.is_marker(event, "my_app@owl_markers", "mark_transfer")
}

fn is_login(event: owl.TraceEvent) -> Bool {
  markers.is_marker(event, "my_app@owl_markers", "mark_login")
}

fn is_other(event: owl.TraceEvent) -> Bool {
  markers.is_any_marker(event, "my_app@owl_markers")
  && !is_transfer(event) && !is_login(event)
}

// Safety: transfer before login -> violation
pub fn no_transfer_before_login() -> owl.SHML {
  owl.nu("X", fn(x) {
    owl.and(
      owl.and(
        owl.box(is_transfer, owl.ff()),   // transfer -> VIOLATION
        owl.box(is_login, owl.tt()),      // login -> safe, stop
      ),
      owl.box(is_other, x),              // other -> keep watching
    )
  })
}

// 4. Start monitoring
pub fn main() {
  let handler = fn(verdict: owl.Verdict) {
    case owl.is_violation(verdict.result) {
      True -> io.println("VIOLATION: " <> verdict.monitor_name)
      False -> io.println("SATISFIED: " <> verdict.monitor_name)
    }
  }

  let specs = [
    #("no_transfer_before_login", no_transfer_before_login(), handler),
  ]

  let assert Ok(runtime) = owl.start(specs, owl.trace_new())

  // Set trace patterns so BEAM watches the marker functions
  let assert Ok(_) = controller.set_trace_pattern(
    "my_app@owl_markers", "mark_login", 0, [],
  )
  let assert Ok(_) = controller.set_trace_pattern(
    "my_app@owl_markers", "mark_transfer", 0, [],
  )

  // ... your app runs ...

  let verdicts = owl.verdicts(runtime)
  let _ = owl.stop(runtime)
}

Core Concepts

sHML (Safety Hennessy-Milner Logic)

Owl uses sHML to express safety properties — things that should never happen.

Constructor	Notation	Meaning
owl.tt()	tt	Always satisfied (terminal)
owl.ff()	ff	Immediate violation (terminal)
owl.box(pred, phi)	[pred]phi	If pred matches, check phi
owl.and(left, right)	left ∧ right	Both must hold
owl.nu("X", fn(x) { ... })	νX. ...	Greatest fixpoint (recursion)

Important: sHML conjunction (∧) absorbs satisfactions. In [good]tt ∧ [bad]ff, if good fires, the tt is consumed but the [bad]ff branch persists. This means monitors are best suited for detecting violations (when ff fires), not confirming satisfactions. Design your formulas so that ff guards events that should genuinely never happen.

Markers

Markers are zero-cost no-op functions placed at key points in your application:

// src/my_app/owl_markers.gleam
pub fn mark_request_start() { Nil }
pub fn mark_authenticated() { Nil }
pub fn mark_request_end() { Nil }

The BEAM tracer watches these functions without modifying your app's behavior. Use the built-in owl/markers module for predicates:

import owl/markers

fn is_auth(event) { markers.is_marker(event, "my_app@owl_markers", "mark_authenticated") }
fn is_any(event) { markers.is_any_marker(event, "my_app@owl_markers") }

// Or use the convenience constructors:
let is_auth = markers.predicate("my_app@owl_markers", "mark_authenticated")
let is_other = markers.except_predicate("my_app@owl_markers", ["mark_authenticated", "mark_request_start"])

Trace Targets

Target	When to use
owl.trace_new()	HTTP servers, actor systems — traces processes spawned after monitoring starts
owl.trace_self()	Benchmarks, tests — traces the calling process and its children
owl.trace_all()	Debugging — traces everything (use with caution)
owl.trace_pid(pid)	Specific process monitoring

Configuration

// Default: monitor fires once, then stops
let assert Ok(rt) = owl.start(specs, owl.trace_new())

// With reset: monitor resets after each verdict (for long-running servers)
let config = owl.default_config() |> owl.with_reset_on_verdict
let assert Ok(rt) = owl.start_with_config(specs, owl.trace_new(), config)

// With debug logging
let config = owl.default_config() |> owl.with_debug

API Reference

Starting and Stopping

Function	Description
owl.start(specs, target)	Start monitoring with default config
owl.start_with_config(specs, target, config)	Start with custom config
owl.stop(runtime)	Stop and clean up
owl.verdicts(runtime)	Get all collected verdicts

Runtime Management

Function	Description
owl.attach(runtime, name, formula, handler)	Add a monitor at runtime
owl.detach(runtime, name)	Remove a monitor

Trace Patterns

import owl/trace/controller

// Tell BEAM to trace calls to a specific function
controller.set_trace_pattern("module_name", "function_name", arity, [])

Built-in Markers (owl/markers)

Function	Description
markers.is_marker(event, module, name)	Check for specific marker
markers.is_any_marker(event, module)	Check for any marker in module
markers.predicate(module, name)	Create a predicate closure
markers.any_predicate(module)	Create an any-marker predicate
markers.except_predicate(module, excluded)	Create an "other" predicate

Common Patterns

1-Phase: Bad Event Never Happens

// νX. ([bad]ff ∧ [·]X)
owl.nu("X", fn(x) {
  owl.and(
    owl.box(is_bad_event, owl.ff()),
    owl.box(is_any_event, x),
  )
})

2-Phase: Bad Event After Trigger

// Phase 1: νX. ([trigger] Phase2 ∧ [other] X)
// Phase 2: νY. ([bad]ff ∧ [reset]tt ∧ [other] Y)
let phase2 = owl.nu("Y", fn(y) {
  owl.and(
    owl.and(
      owl.box(is_bad, owl.ff()),
      owl.box(is_reset, owl.tt()),
    ),
    owl.box(is_other_phase2, y),
  )
})

owl.nu("X", fn(x) {
  owl.and(
    owl.box(is_trigger, phase2),
    owl.box(is_non_trigger, x),
  )
})

3-Phase: Chained Triggers

// Phase 1 → Phase 2 → Phase 3
// IMPORTANT: Only the LAST phase should contain [bad]ff guards.
// ff branches in earlier phases persist into later phases.
let phase3 = owl.nu("Z", fn(z) {
  owl.and(
    owl.and(owl.box(is_bad, owl.ff()), owl.box(is_reset, owl.tt())),
    owl.box(is_other_3, z),
  )
})

let phase2 = owl.nu("Y", fn(y) {
  owl.and(
    owl.box(is_trigger_2, phase3),
    owl.box(is_non_trigger_2, y),
  )
})

owl.nu("X", fn(x) {
  owl.and(
    owl.box(is_trigger_1, phase2),
    owl.box(is_non_trigger_1, x),
  )
})

Warning: Do NOT put [bad]ff in Phase 1 or Phase 2 — those ff branches persist into later phases and cause false violations. See the manual for details.

Building and Testing

gleam build
gleam test

License

MIT