squitter

A no_std, allocation-free parser and encoder for 1090ES (1090 MHz Extended Squitter, the ADS-B link layer carried in Mode S DF17 frames), commonly represented as raw hex (e.g. dump1090's *8D4840D6202CC371C32CE0576098; format).

• Four message families, decode and encode: aircraft identification, surface position, airborne position, and airborne velocity. Every test fixture is a real captured hex frame, cross-checked against pyModeS's own test suite, not synthetic round trips. tests/real_world_corpus.rs additionally cross-checks against an independent bulk decode (via pyModeS itself) of over a thousand unique real captured frames.
• Fuzz-tested with proptest: message decode/encode never panics on arbitrary bytes, and reaches a fixed point after one encode/decode pass, over the full space of raw ME payloads (not just the handful of fixed fixtures above).
• CPR position decoding, including the harder surface-CPR case (which needs a nearby reference position to disambiguate its 90° latitude zone), verified against real airborne and surface position pairs.
• no_std, no alloc: works on bare-metal targets with no allocator. core has no floor/sqrt/acos without a libm dependency, so the CPR math and ground-speed magnitude use a hardcoded latitude-zone table and a hand-rolled Newton-Raphson sqrt instead of pulling one in.
• Zero mandatory dependencies. The bit-level codec is hand-rolled, same as the CPR/velocity math above.
• #![forbid(unsafe_code)].
• Formal verification of the bit engine with Kani, not just tests.

Crates

Quick start

let msg = squitter::decode_line("8D4840D6202CC371C32CE0576098")?;

let squitter::AdsbMessage::Identification(id) = msg else {
    panic!("expected an identification message");
};

println!("callsign={}", id.callsign);

Encoding mirrors decoding, given the transmitting aircraft's ICAO address and transponder capability level:

let frame = squitter::encode_frame(&msg, 0x4840D6, 5)?;
let mut buf = [0u8; 28];
let hex = frame.write_hex(&mut buf);

Add it to a project with:

cargo add squitter

Message type coverage

A few things are deliberately left undecoded/deferred rather than approximated, and documented as such in the source: the legacy Gillham/gray-code altitude encoding (rare in modern traffic), single-frame CPR position decode against a known reference (only the even/odd-pair global decode is implemented), and a ground-track-angle accessor for airborne velocity (needs atan2, which doesn't have the same clean small-table shortcut NL(lat) does).

See crates/squitter/src/lib.rs for the crate's module layout and crates/squitter/src/message for each message type, each with its own real-fixture tests.

Building

This project is built and checked with Nix:

nix develop        # dev shell: toolchain, rust-analyzer
nix flake check -L # fmt, clippy (pedantic), tests, no_std/no_alloc cross-compile
nix build           # squitter-cli (default package)
nix build .#squitter

CI runs the identical nix flake check -L, so there is one source of truth for what "passing" means, locally and in GitHub Actions.

Without Nix, a standard cargo build / cargo test from the workspace root also works with a recent stable Rust toolchain (edition 2024, MSRV tracked in Cargo.toml).

Formal verification

The bit-level codec (src/bits/) is proven, not just tested, using Kani, a bounded model checker for Rust. Where the test suite samples inputs, these harnesses (gated behind #[cfg(kani)], so they add nothing to normal builds) prove properties over every input in a bounded space:

• BitReader/BitWriter never panic, for any input, including malformed nbits/buffer combinations a caller isn't supposed to pass.
• Writing a value and reading it back recovers the original value exactly, for every bit width 1..=64.

Kani requires its own toolchain download (a pinned nightly + CBMC), which needs network access and isn't run inside the hermetic Nix sandbox, so it's a manual step rather than part of nix flake check:

cargo install --locked kani-verifier
cargo kani setup
cargo kani -p squitter

License

MIT. See LICENSE.