wirespec 0.4.1

Type-safe protocol description language — compiler, verifier, and LSP
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131

# wirespec

**Type-safe protocol description language for network binary formats.**

Declaratively describe your binary protocol and get safe, zero-allocation C and Rust parsers/serializers — no hand-written byte manipulation, no buffer overreads, no endianness bugs. State machines are verified with TLA+ model checking.

## Quick Example

```
@endian big
module net.udp

packet UdpDatagram {
    src_port: u16,
    dst_port: u16,
    length: u16,
    checksum: u16,
    require length >= 8,
    data: bytes[length: length - 8],
}
```

```bash
wirespec compile udp.wspec -t c -o build/    # generates .h + .c
wirespec compile udp.wspec -t rust -o build/  # generates .rs
```

## Install

```bash
cargo install wirespec
```

Or build from source:

```bash
git clone https://github.com/wirespec-lang/wirespec
cd wirespec
cargo build --release
# Binary: target/release/wirespec
```

## Usage

```bash
wirespec compile <input.wspec> -t <c|rust> -o <dir>  # compile to C or Rust
wirespec check <input.wspec>                          # type-check only
wirespec verify <input.wspec> -o <dir>                # generate TLA+ spec
wirespec verify <input.wspec> --run-tlc               # run TLC model checker
```

Options: `-I <dir>` (include path), `--recursive` (emit dependencies), `--fuzz` (libFuzzer harness, C only), `--bound N` (TLA+ model checking bound).

## State Machine Verification

Define state machines with guards, actions, and delegates. wirespec statically verifies them and generates TLA+ specs for model checking.

```
@verify(bound = 3)
state machine PathState {
    state Init       { path_id: u8 }
    state Active     { path_id: u8, rtt: u8 = 0 }
    state Closed [terminal]
    initial Init

    transition Init -> Active {
        on activate(id: u8)
        action { dst.path_id = src.path_id; }
    }
    transition Active -> Closed { on close }
    transition * -> Closed { on abort }

    verify NoDeadlock
    verify AllReachClosed
    verify property AbandonIsFinal:
        in_state(Closing) -> [] not in_state(Active)
}
```

```bash
wirespec verify path.wspec --run-tlc
# PASS: All properties verified for PathState (bound = 3)
```

**Static analysis (compile-time):** terminal state irreversibility, delegate acyclicity, structural reachability, exhaustive transitions, wildcard priority.

**Model checking (TLA+):** deadlock freedom, liveness (all paths reach terminal), user-defined safety/liveness properties, guard mutual exclusivity.

## ASN.1 Integration

wirespec can embed ASN.1-encoded fields in binary protocol descriptions. With the `asn1` feature, `.asn1` files are automatically compiled via [rasn](https://github.com/librasn/rasn).

```
extern asn1 "etsi_its_cdd.asn1" { CAM }

packet ItsCamPacket {
    version: u8,
    length: u16,
    cam: asn1(CAM, encoding: uper, length: length),
}
```

```bash
cargo run --features asn1 -- compile its.wspec -t rust -o build/
# Outputs: build/etsi_its_cdd.rs (rasn types) + build/its.rs (wirespec codec)
```

Supported encodings: UPER, BER, DER, APER, OER, COER. C backend transparently treats ASN.1 fields as raw bytes.

## Protocol Examples

QUIC, TLS 1.3, MQTT, BLE, IPv4, TCP, Ethernet, V2X (ASN.1/UPER) — all defined and tested in `examples/`.

## Editor Support

VS Code extension with syntax highlighting, completion, hover, and diagnostics: [wirespec-language-tools](https://github.com/wirespec-lang/wirespec-language-tools)

## Roadmap

| Version | Feature |
|---------|---------|
| ~~v0.1.0~~ | Wire formats, state machines, C/Rust codegen |
| ~~v0.2.0~~ | ASN.1 / rasn integration |
| ~~v0.3.0~~ | TLA+ bounded verification |
| v0.4.0 | Delegate SM TLA+ support, crates.io publish |

## License

Apache-2.0

Copyright (c) 2026 mp0rta