OCaml 5 will not tell you which effects a library requires you to handle. This works it out from the compiler's own typed trees.
Thomas Leonard, the author of Eio, reviewed this work and asked for a feature. He told us the crash case matters less than we thought, since the runtime reports it immediately, and described the one a runtime check cannot see: Lwt code performing an Eio effect that is handled and still deadlocks. That request is
E005, it is built, andmodels/schedulers.confcites him rather than guessing.The full exchange: discuss.ocaml.org
The manual is explicit about the gap:
Unlike languages such as Eff and Koka, effect handlers in OCaml do not provide effect safety; the compiler does not statically ensure that all the effects performed by the program are handled.
So there is no declaration to read, no signature to check, and no way to know
what a library asks of you short of reading its source. unhandled contract
derives it:
$ unhandled contract picos/_build
module Picos
Picos.Trigger.await may perform {Picos.Trigger.Await}
Picos.Fiber.current may perform {Picos.Fiber.Current}
Picos.Fiber.spawn may perform {Picos.Fiber.Spawn}
Picos.Fiber.yield may perform {Picos.Fiber.Yield}
Picos.Fiber.Maybe.current_and_check_if may perform {Picos.Fiber.Current, ...unknown}
module Picos_std_structured__Run
Picos_std_structured__Run.spawn may perform {Picos.Fiber.Spawn, ...unknown}
...unknown means the contract is incomplete at that function because it
calls into code with no .cmt available. It is printed rather than rounded
away: a contract that quietly stops short is worth less than one that says
where it stops.
docs/ECOSYSTEM-CONTRACTS.md is that output for
16 libraries and 458 functions, regenerated by one command. Nothing else in
the ecosystem produces this document, and no hand-written version would stay
true.
A printed contract is a report. A recorded one is a guarantee:
$ unhandled contract . --baseline effects.txt
recorded 84 function(s) in effects.txt
$ unhandled contract . --baseline effects.txt
contract unchanged: 84 function(s)
Commit effects.txt. If a pull request changes what your library asks of its
callers, the build goes red and the diff names the function and the effect.
The same analysis run the other way: every perform that can reach a program
entry point with no handler above it.
type _ Effect.t += Emit : string -> unit Effect.t
let log msg = Effect.perform (Emit msg)
let process xs = List.iter log xs
let () = process (load_batch ())$ unhandled check .
esc_simple.ml:4:9: error[E001] effect Esc_simple.Emit escapes unhandled
entry Esc_simple (module initialisation)
via esc_simple.ml:4:9 calls Esc_simple.process
then esc_simple.ml:3:27 calls Esc_simple.log
then esc_simple.ml:2:17 performs Emit
1 error(s), 0 warning(s)
Zero false negatives over 1000 generated programs with the runtime as oracle,
and swept across 48 analysed repositories and 4,735 modules of real ecosystem
code. Where it is imprecise it is imprecise in one direction only: it
over-approximates rather than staying quiet. The known limits, and the full
account of what the ecosystem sweep produced, are in
docs/LIMITATIONS.md and
bench/NEGATIVE-RESULT.md.
No forked compiler, no annotations, no code changes: it reads the .cmt files
your build already produces.
dune build && make demo
Six sections, each executed rather than asserted: the ten-line program that compiles clean and crashes, the finding, a witness that is generated and run, a finaliser whose effect no handler can catch, an Eio call with no runtime, and the two measured numbers. Nothing in it is a screenshot.
OCaml 5.3 or newer. Texp_match and Texp_try only gained their
effect-case lists in 5.3, so earlier compilers cannot represent the construct
this tool analyses; match ... with effect did not exist before 5.3 either.
5.4 is supported through a small compatibility shim (lib/compat_5*.ml,
selected by dune on %{ocaml_version}), which covers three changes: the move
of constructor and label descriptions from Types to Data_types, the extra
field on Tpat_alias, and the labels that labelled tuples added to
Types.Ttuple. See docs/TYPEDTREE-NOTES.md section 10.
dune build
dune exec bin/unhandled.exe -- check _build/default
test/run_tests.sh is a three-way differential test: for every corpus program
it compares the declared expectation, the analyser's prediction, and what the
program actually does when executed.
$ bash test/run_tests.sh
PROGRAM EXPECTED ANALYSER RUNTIME RESULT
------------------------------------------------------------------------------
esc_simple crash Emit crash Emit crash ? PASS
lambda_iter crash Emit crash Emit crash ? PASS
local_helper crash Ping crash Ping crash ? PASS
nested_forward clean clean clean PASS
nested_partial crash B crash B crash B PASS
ok_deep clean clean clean PASS
ok_handled clean clean clean PASS
recursion crash Tick crash Tick crash ? PASS
try_effect clean clean clean PASS
wildcard_trap crash B crash B crash B PASS
------------------------------------------------------------------------------
10 passed, 0 failed
unhandled witness turns each finding into a program, compiles it, runs it,
and reports what actually happened. A witness does not parse the crash message
(the runtime only prints the effect payload sometimes); it installs a handler
for the exact effect under suspicion and reports a positive confirmation when
that effect arrives:
$ unhandled witness test/xmodule
w01 Svc.Ping Svc.run_all confirmed
1/1 findings confirmed by execution
(* Generated by unhandled. Proves that Svc.Ping escapes Svc.run_all unhandled. *)
let () =
match ignore (Svc.run_all ["witness"]) with
| () -> print_endline "NOT_CONFIRMED"
| effect (Svc.Ping _), _ -> print_endline "CONFIRMED"Arguments are synthesised from the callee's type, and deliberately non-trivial:
an empty list would make List.iter f [] perform nothing and the witness would
prove nothing. When no witness can be built, the tool says so rather than
guessing:
w06 Lambda_iter.Emit - not constructible: no named function in the blame path
A confirmed finding is a true positive by construction. That is how this tool measures its own precision.
test/fuzz generates random effectful programs and checks the analyser against
reality. It does not compute an expected answer: the runtime is the oracle.
Generate a program, ask whether any effect escapes, then run it and see whether
it actually crashes. Any disagreement is a genuine bug.
| Mode | Programs | False positives | False negatives | Agreement |
|---|---|---|---|---|
| branch-free | 600 | 0 | 0 | 100% |
| branching | 400 | 21 (5.3%) | 0 | 94.8% |
Zero false negatives across 1000 generated programs. The imprecision is one-sided: the analyser over-approximates, and never stays silent about a crash that actually happens.
The branching false positives are join over-approximation, and we checked that
rather than assuming it. In test/fuzz/failures/fp_seed122.ml the flagged
perform E3 sits in an else branch that never executes; the analyser joins
both arms of every conditional, so it reports an effect the run never performs.
Branch-free and branching results are reported separately for exactly this
reason: folding them together would hide real defects behind known,
explainable imprecision.
Generated programs nest syntactic and Deep.try_with handlers, forward through
| _ -> None wildcards, call across functions, and pass effectful closures
through List.iter.
$ START=1 COUNT=600 bash test/fuzz/run_fuzz.sh
seeds 1..600 mode branch-free analysed 600 skipped 0
agree 600
false positives 0
false negatives 0
agreement 100%
$ MODE=branch START=1 COUNT=400 bash test/fuzz/run_fuzz.sh
agree 379
false positives 21
false negatives 0
agreement 94.8%
The runner refuses to start unless the analyser flags a known-bad probe first. Without that guard a broken build reads as "predicted clean" on every seed and the run reports a wall of false negatives that are really a missing binary.
Summaries are cached per module, keyed by the digest of the .cmt file. The
expensive part of a run is reading typed trees and building summaries; the
fixpoint itself is cheap, so an unchanged project re-checks in near-zero work.
$ bash bench/perf.sh
modules: 200
consistency: cached and uncached output identical
cold: 0.18s
warm: 0.06s
warm: 0.05s
The consistency line matters more than the timings: a cache that changes the
answer is worse than no cache, so perf.sh compares cached against
--no-cache output byte for byte before reporting any number. --no-cache
also exists so a suspected cache bug can be ruled in or out in one run.
Honest caveat on the benchmark: those 200 modules are small and synthetic. The shape of the result (reading trees dominates, caching removes it) holds on real projects, but the ratio on a large codebase has not been measured.
One subtlety the cache has to respect: alias registration is a side effect of building, so a cached entry carries the aliases its module contributed and replays them on a hit. Without that, a second run would resolve fewer names than the first and quietly report different findings.
A library that performs effects is not buggy: its handler lives in the application. Analysing libraries as if they were programs is how an effect checker drowns in false positives. So the same code gets two readings.
$ unhandled contract test/xmodule # library mode: what callers must handle
module Svc
Svc.service may perform {Svc.Ping}
Svc.run_all may perform {Svc.Ping}
$ unhandled check test/xmodule # executable mode: who forgot to handle it
app.ml:2:9: error[E001] effect Svc.Ping escapes unhandled
entry App (module initialisation)
via app.ml:2:9 calls Svc.run_all
The manual is explicit that an effect performed from a signal handler,
finaliser, GC alarm, memprof callback, or across a C caml_callback frame
always raises Effect.Unhandled. No handler anywhere in the program can
rescue it, which makes these findings unconditional.
let () = Gc.finalise (fun _ -> Effect.perform Log) (ref 0)
let () =
match Gc.full_major () with (* a handler that cannot help *)
| () -> print_endline "no crash"
| effect Log, k -> Effect.Deep.continue k ()fin_leak.ml:3:9: error[E004] effect Fin_leak.Log can be performed from a
finaliser, where no handler can ever catch it
Running that program confirms it: Fatal error: exception Stdlib.Effect.Unhandled(Fin_leak.Log), despite the enclosing handler.
OCaml's concurrency libraries are mutually incompatible effect schedulers. Performing one library's effect under another's runtime is a guaranteed crash, and it is not a missing handler: a handler is installed, it just belongs to the wrong library. That gets its own diagnostic.
let () = Sched_b.run (fun () -> Sched_a.yield ())mix.ml:2:9: error[E003] effect Sched_a.Yield belongs to the mock_a scheduler
but is performed under the mock_b runtime
Handlers for Eio, Riot, Moonpool and Miou live inside compiled dependencies we
often have no .cmt for, so they are supplied as data in
models/schedulers.conf rather than discovered by analysis.
Every diagnostic above ends in a crash, which means a runtime test could have
found it too. E005 is the one that could not.
We announced this work on discuss.ocaml.org and asked to be criticised. Thomas Leonard, who wrote Eio, replied that the crash case is worth less than we thought, since "a runtime error is reported immediately, so there's no benefit to static analysis here". Then he described the case that is worth catching:
when running Eio and Lwt code together, I'd like to be sure that the Lwt code doesn't perform an Eio effect, even though it will be handled. This can result in deadlock because Lwt assumes that all code returns immediately.
The effect is performed. A handler catches it. Nothing crashes. And work that should have interleaved runs in sequence instead. There is no exception for a runtime check to observe, which makes this the first case in the project where being static is an advantage rather than a consolation.
Lwt_eio.run_lwt opens a region where performing is forbidden and
Lwt_eio.run_eio closes it again, so the fatal-context machinery behind E004
needed only that escape hatch:
lwt_ctx.ml:12:18: error[E005] effect Eio__core.Suspend.Suspend is performed in
Lwt context, where Lwt expects the callback to
return immediately
entry Lwt_ctx (module initialisation)
via lwt_ctx.ml:12:18 enters Lwt_eio.run_lwt
then lwt_ctx.ml:13:6 performs Suspend
bash bench/lwt_demo.sh runs it against the real lwt_eio, where it fires on
his reproduction directly and inside Eio.Fiber.both. Wrapper depth is covered
in docs/LIMITATIONS.md.
Building it also paid off somewhere unrelated. Printing the term the analysis
had already computed (UNHANDLED_EXPLAIN=1) exposed a real defect: a lambda
handed to a callee with no .cmt was assumed never to be called. That is
unsound, and it had been swallowing effects in every
with_resource (fun r -> ...) in the corpus, a pattern with nothing to do with
Lwt. The fix outlives the feature that prompted it.
unhandled-lsp speaks LSP over stdin/stdout and re-checks on open and save.
Diagnostics carry the blame path as relatedInformation, which editors render
as a clickable chain. The finding is the path, not the line.
diagnostic: effect Metrics.Emit escapes unhandled (E001)
- calls Metrics.process
- calls Metrics.log
- performs Emit
It reacts to save rather than to every keystroke, on purpose: effects are a
whole-program property and the analysis reads .cmt files, so there is nothing
useful to say about a buffer that has not been compiled. The summary cache is
what makes re-checking on every save cheap enough to do.
VS Code, Neovim or any LSP client can launch it directly; it needs no
configuration beyond the binary path and a project with a dune-project and a
_build directory.
docs/TYPEDTREE-NOTES.md: empirical notes on the OCaml 5.3 typed tree. Read this before touchinglib/effect_syntax.ml.docs/DESIGN.md: the analysis, and why it is shaped this way.docs/LIMITATIONS.md: where it is unsound, stated plainly.docs/ECOSYSTEM-CONTRACTS.md: the derived contracts for 16 libraries.bench/NEGATIVE-RESULT.md: the sweep that found nothing, and what it taught.paper/ABSTRACT.mdandpaper/PITCH.md: the SegFault 2026 submission.
MIT.