Deterministic state-space exploration for production embedded firmware.
Forkpoint executes real firmware inside a Deterministic Virtual MCU and searches alternate executions — interrupt order, DMA completion, timer fire, peripheral timing, and injected faults — to find bugs that are hard to catch on a bench.
Nondeterminism is modeled as explicit events, so a recorded run can be replayed exactly. Optional application-level properties turn the guarantees you care about into checks the explorer can judge across schedules.
Every raised interrupt was observed by the handler under all seeds.
DMA completions never wrote outside the registered buffer.
Fails on 3 of 128 seeds: a late timer IRQ re-enters init after the first path already claimed the peripheral.
Firmware rarely fails alone. Forkpoint models the peers a board talks to — over the air, on Ethernet, and on wired buses — as deterministic events you can script, fault, and replay.
Run several boards as one system. Bluetooth LE frames pass between linked nodes only through a coordinator, stamped with virtual time. Arrival order is (time, sender, sequence); link loss and RSSI are seeded so the same topology always yields the same air. IEEE 802.15.4 frames can be injected the same way scripted bus traffic is. Captures land in a pcap for Wireshark.
On a board’s Ethernet link, fault plans deliberately misbehave: reorder TCP segments, duplicate ACKs, hold FIN, open gaps, reset connections, ignore DHCP or DNS, flood ARP, and more. Each fault applies to a counted set of matching frames and is kept in the record so replay sees the same network.
An I²C script plays timed external inputs into the run: I²C transfers, GPIO levels, ADC voltages, CAN frames, IEEE 802.15.4 frames, and UDP datagrams from hosts on the link. Fuzz can emit a script that explore replays exactly — same virtual times, same bytes.
Wi‑Fi station/AP stacks are not modeled yet; networked ESP32 examples use the board Ethernet path. BLE multi-node runs use radios such as the nRF52840’s.
Every discovered failure is a deterministic artifact: the firmware hash, the event decisions, and the outcome. Replay it on your desk, minimize it to a short counterexample, and verify the fix under the same conditions.
Baseline execution targets the same firmware artifact you flash to the device — no simulator-specific HAL, no modified RTOS, and no source rewrite required to start. Virtual platforms are described with Device Tree. CPU execution comes from pluggable architecture backends.
Watch the board’s LCD as it commits frames, and drive a touch panel from your viewer — streamed over loopback VNC with no extra host dependencies beyond the standard library.
--display vnc=:N serves the panel on
127.0.0.1, port 5900 + N, for as long as the
run lasts. Nothing appears until the panel commits its first
frame. Add wait so the run pauses there until a
viewer connects; add fps for a host-side frame-rate
readout. The server speaks RFB 3.8 with raw encoding — no
password, loopback only.
On a board with a touch controller, the viewer’s left mouse button
is a finger on the panel: press, drag, and release reach the
firmware as touches over I²C. The keyboard is ignored. Live touch
input is not deterministic, so recording and forking are rejected
together with --display.
fpt explore \
--board esp32-s31-korvo-1 \
--display vnc=:0,wait \
firmware.elf
# viewer → 127.0.0.1:5900
# left mouse = finger on the panelThe SDK is optional. Baseline runs need none of it. When you want application-level properties the machine cannot infer, drop in a few probes — no heap, filesystem, networking, or OS required. Properties report observations without stopping the firmware.
#include <forkpoint.h>
FPT_ALWAYS(
pressure <= MAX_PRESSURE,
"pressure remains within safe range"
);
FPT_SOMETIMES(
retry_count >= 3,
"multiple retries occur"
);
FPT_REACHABLE("recovery mode");
FPT_UNREACHABLE("invalid controller state");use forkpoint::prelude::*;
assert_always!(
pressure <= MAX_PRESSURE,
"pressure remains within safe range"
);
assert_sometimes!(
retry_count >= 3,
"multiple retries occur"
);
assert_reachable!("recovery mode");
assert_unreachable!("invalid controller state");
Probes land in a property catalog in the ELF so Forkpoint can tell a
missing property from one that was never reached. The explorer judges
them across schedules; --properties writes JSONL verdicts.
The exploration core stays independent of ISA, SoC, board, and RTOS. Hardware and environmental nondeterminism enter only as controlled events.
Load production firmware into a Deterministic Virtual MCU with memory, IRQs, DMA, timers, and peripherals under virtual time.
Search alternate event orderings, inject faults, collect coverage, and evaluate properties across the space that matters.
Keep a bit-reproducible recording, shrink it to an understandable counterexample, and confirm the fix under the same seed.
Access and docs are coming soon.