MVL Playground
Run
⌘+Enter
Stop
Validate
▾
check
ready
prove
ready
solve
ready
test
ready
test --coverage
waiting
mcdc
ready
assurance
ready
Examples
▾
Hello, world!
Simplest MVL program — Console effect (Req 7).
Auth handler
All 11 requirements — ADTs, ownership, Option, Result, IFC.
Safe division
Refinement types, IFC labels, effects, totality (Req 5, 7, 10, 11).
Shapes
ADTs, enum match dispatch, function composition (Req 1).
Calculator
Total functions, if/else expressions (Req 8).
Actor ping-pong
Two actors exchanging messages — capability-based concurrency (Req 9).
Flight fuel planning
Aviation dispatch kernel — refinements, IFC, MC/DC (DO-178C).
ETCS movement authority
Rail supervision kernel — refinement + IFC (EN 50128 SIL 4).
PCI payment
PCI-DSS payment processing — user-defined IFC labels.
Medical triage
Emergency-department triage — compound boolean decisions, MC/DC.
Grid protection
Electric grid protection — IFC on taint, sensor trust boundary.
Reset
Files
+
Runtime
Compile Output
Download JSON
Press Run (⌘+Enter) or pick a validator from Validate ▾.