Pacing logic proved safe in Z3 before a pulse can reach cardiac tissue. Blocks R-on-T induction at the hardware execution gate and clamps the upper tracking rate regardless of software state.
After the ventricle depolarises it repolarises, and during that recovery the tissue is vulnerable: a pacing spike delivered into the T wave can induce ventricular fibrillation. The interval is the ventricular refractory period, and the safety property is simple to state and lethal to get wrong — no spike may fall inside it.
PacePulse does not implement that as a software timer that interrupts might delay. It is a hardware-gated formal invariant, proved over every transition of the DDD and VVI pacing state machines against an electrophysiology specification, so the guarantee holds regardless of what the software is doing.
Medical device software is usually argued safe by testing: hardware in the loop, coverage metrics, clinical evidence. That establishes confidence. It does not establish a bound, and a buffer overflow in C firmware is not a statistical event.
| Characteristic | Traditional medical firmware | PacePulse verified kernel |
|---|---|---|
| safety verification | hardware-in-the-loop manual testing | exhaustive mathematical SMT proofs |
| memory safety | buffer overflow risk in C firmware | pure #![no_std] Rust, zero pointer aliasing |
| refractory guard | software timer interrupts, race-prone | hardware-gated formal invariant |
| transparency | proprietary closed binary | open source, verifiable toolchain |
git clone https://github.com/KELLERBABG/PacePulse.git cd PacePulse && cargo test cargo run --bin pace-sim -- --mode DDD --bpm 72
Scope. This is a research toolchain: a simulator and a formal proof suite, not an implanted device. Nothing here has been through regulatory submission.