Build it in edda
Embedded
A device that cannot page, cannot grow its heap, and cannot be patched on Tuesday needs its resource ceilings proven before it ships. edda's graded effects put those ceilings on the signature, where the build discharges them.
Bounds the build can prove
There is no garbage collector and no runtime to size. A function whose row says alloc(bytes <= 4096) is held to that number at compile time, and a loop without a termination measure must admit divergence on its signature. The properties embedded reviewers check by hand are the ones the compiler already discharges.
What the language gives a device
Graded allocation
Allocators are parameters with bounds, never globals. A driver handed a 4 KiB budget cannot exceed it, and the proof is part of the build, not a soak test.
Linear peripherals
A handle to a bus or a register block can be linear: the build rejects losing it, double-releasing it, or using it after handoff. Typestate makes invalid device states unrepresentable.
Wire-exact records
Packed layout and alignment attributes pin a record to its hardware or protocol shape, with the unverifiable byte-order claims confined to recorded trust points.