diff --git a/README.md b/README.md
index 583f611..d0706c1 100644
--- a/README.md
+++ b/README.md
@@ -8,7 +8,7 @@ real OpenBSD `pfctl` over the `/dev/pf` ioctl ABI. (A second module for the
 
 **Status:** the filter core, stateful filtering, tables, anchors, NAT
 (`nat-to`/`rdr-to`), `divert` and `pflog` are **verified in a real libvirt
-lab** (9/9 gates green).  The remaining features (binat-to, route-to/dup-to,
+lab** (10/10 gates green).  The remaining features (route-to/dup-to,
 scrub e2e, ALTQ/pfq, af-to) are still pending — honest per-feature status:
 [`docs/en/feature-matrix.md`](docs/en/feature-matrix.md).
 Demo (asciinema): [`docs/en/demo.md`](docs/en/demo.md).
@@ -22,7 +22,7 @@ Design: [`docs/superpowers/specs/2026-11-11-pf-linux-port-design.md`](docs/super
 | M0 | repo, scripts, kernel build, VM boots the custom kernel | done |
 | M1 | compat layer, `pf.ko` loads, `/dev/pf`, `pfctl -f` / `-s info` | done |
 | M2 | filter core: rules/states/tables/anchors, VM gates 01–04 | **done** — gates 01/02/03/04 green |
-| M3 | NAT (`nat-to`/`rdr-to`/`binat-to`), scrub e2e | **partial** — `nat-to` (gate 05) and `rdr-to` incl. 2 MB integrity (gate 06) verified; `binat-to` and scrub e2e pending |
+| M3 | NAT (`nat-to`/`rdr-to`/`binat-to`), scrub e2e | **partial** — NAT verified (gate 05), redirect incl. 2 MB integrity (gate 06), `binat-to` (gate 07); scrub e2e pending |
 | M4 | route-to/dup-to/fail-to, divert e2e, pflog | **partial** — divert e2e (gate 11) and pflog (gate 12) verified; route-to/dup-to pending |
 | M5 | queues: HFSC/FQ-CoDel back ends + `pfq` qdisc | pending |
 | M6 | docs complete, patchset tidy, full suite green, tagged release | in progress (docs done, suite 7/7 green) |
diff --git a/docs/en/feature-matrix.md b/docs/en/feature-matrix.md
index 2a98ce3..1bd0878 100644
--- a/docs/en/feature-matrix.md
+++ b/docs/en/feature-matrix.md
@@ -50,7 +50,7 @@ As of 2026-11-11; source of per-row evidence: `out/test-logs/`,
 |---|---|---|---|
 | `nat-to` (port pools, sticky-port, static-port) | `pass out … nat-to (eth1:0)` | M3 | **VERIFIED in lab** — source NAT works end to end: the packet leaves with the pool address (tcpdump proof), the reply is de-NATed and re-routed to the client, and the state shows both tuples (`10.0.2.1:59335 (10.0.1.10:4380) -> 10.0.2.20:8`). Gate: `tests/vm/05-nat.sh`. |
 | `rdr-to` | `pass in … to <fw> port 8080 rdr-to <srv> port 80 keep state` | M3 | **VERIFIED in lab** — port redirect works end to end (gate `06-rdr.sh`): the client talks to the firewall's address, pf rewrites the destination, re-routes the packet, and the reply is un-redirected. The gate also pulls 2 MB through the redirect and checks byte-for-byte integrity (GSO/TSO regression guard). |
-| `binat-to` | `binat-to <net>` (no direction) | M3 | PENDING-M3 — parser accepts the 8.0 form (`binat-to` is a rule option, not a standalone rule); VM gate not written yet. |
+| `binat-to` | `pass quick proto icmp from 10.0.2.20 to 10.0.1.10 binat-to 10.0.2.50 keep state` | M3 | **VERIFIED in lab** — gate `07-binat.sh`. pfctl expands one `binat-to` rule into the documented pair (`pass out … nat-to <mapped> static-port` + `pass in … rdr-to <real>`), and both halves work: the peer sees the mapped address, the original never leaks, and the reply is translated back. |
 | Scrub/normalize: reassembly, `fragment drop-overlap`, `min-ttl`, `max-mss`, `df`/`no-df`, `random-id`, `set reassemble yes` | `match on all scrub (max-mss 1380 …)` | M3 | COMPILES-untested (`pf_norm.c` compiled into pf.ko and reached from `pf_test`; scapy gate 08 pending) |
 | OS fingerprinting in states | `pass … set os A` + `/etc/pf.os` | bonus | COMPILES-untested (`pf_osfp.c` compiled; no fingerprint packaging yet — missing `/etc/pf.os` is tolerated) |
 
diff --git a/docs/en/pf-guide.md b/docs/en/pf-guide.md
index 3099ecd..1380295 100644
--- a/docs/en/pf-guide.md
+++ b/docs/en/pf-guide.md
@@ -60,7 +60,7 @@ treat them as load-and-pray until the matrix moves them.
 
 | Syntax | Until | What happens today |
 |---|---|---|
-| `nat-to`, `rdr-to` (`binat-to` pending) | — | **Verified in the lab** (gates `05-nat`, `06-rdr`, the latter pulls 2 MB through a redirect and compares it byte for byte). `nat-to (egress)` expands the OpenBSD interface *group*; on a multi-NIC host prefer the explicit `nat-to (<iface>)` form. |
+| `nat-to`, `rdr-to`, `binat-to` | — | **Verified in the lab** (gates `05-nat`, `06-rdr`, the latter pulls 2 MB through a redirect and compares it byte for byte). `nat-to (egress)` expands the OpenBSD interface *group*; on a multi-NIC host prefer the explicit `nat-to (<iface>)` form. `binat-to` is expanded by pfctl into a `nat-to … static-port` + `rdr-to` pair (gate `07-binat`). |
 | `scrub (…)`, `set reassemble` | M3 | `pf_norm.c` runs inside `pf_test` (compiled) — crafted-fragment behavior is untested; treat results as unvalidated. |
 | `divert-to`, `divert` tag | — | **Verified in the lab** (gate `11-divert`): the packet is delivered to an `AF_DIVERT` socket (`PF_DIVERT=32`) served by `tools/pdivert`; with no listener it is dropped, exactly like BSD's `divs_noport`. |
 | `route-to`, `dup-to`, `fail-to`, `reply-to` | M4 | Not implemented as Linux routing glue yet; rules may load but the behavior is undefined — avoid. |
diff --git a/docs/pt-BR/feature-matrix.md b/docs/pt-BR/feature-matrix.md
index e2dffac..824ef3f 100644
--- a/docs/pt-BR/feature-matrix.md
+++ b/docs/pt-BR/feature-matrix.md
@@ -50,7 +50,7 @@ Estado em 2026-11-11; evidência por linha: `out/test-logs/`,
 |---|---|---|---|
 | `nat-to` (pools de portas, sticky-port, static-port) | `pass out … nat-to (eth1:0)` | M3 | **VERIFICADO em lab** — NAT de origem funciona ponta a ponta: o pacote sai com o endereço do pool (prova via tcpdump), a resposta é des-NATeada e roteada de novo para o cliente, e o estado mostra as duas tuplas (`10.0.2.1:59335 (10.0.1.10:4380) -> 10.0.2.20:8`). Gate: `tests/vm/05-nat.sh`. |
 | `rdr-to` | `pass in … to <fw> port 8080 rdr-to <srv> port 80 keep state` | M3 | **VERIFICADO em lab** — o redirect de portas funciona ponta a ponta (gate `06-rdr.sh`): o cliente fala com o endereço do firewall, o pf reescreve o destino, re-rotea o pacote e a resposta é des-redirectuada. O gate também baixa 2 MB pelo redirect e confere a integridade byte a byte (guarda de regressão GSO/TSO). |
-| `binat-to` | `binat-to <rede>` (sem direção) | M3 | PENDING-M3 — o parser aceita a forma 8.0 (`binat-to` é opção de regra, não regra própria); gate em VM ainda não escrito. |
+| `binat-to` | `pass quick proto icmp from 10.0.2.20 to 10.0.1.10 binat-to 10.0.2.50 keep state` | M3 | **VERIFICADO em lab** — gate `07-binat.sh`. O pfctl expande uma regra `binat-to` no par documentado (`pass out … nat-to <mapeado> static-port` + `pass in … rdr-to <real>`), e as duas metades funcionam: o peer vê o endereço mapeado, o original não vaza, e a resposta é traduzida de volta. |
 | Scrub/normalize: remontagem, `fragment drop-overlap`, `min-ttl`, `max-mss`, `df`/`no-df`, `random-id`, `set reassemble yes` | `match on all scrub (max-mss 1380 …)` | M3 | COMPILES-untested (`pf_norm.c` compilado no pf.ko e alcançado pelo `pf_test`; gate scapy 08 pendente) |
 | Fingerprint de SO em estados | `pass … set os A` + `/etc/pf.os` | bônus | COMPILES-untested (`pf_osfp.c` compilado; sem empacotamento de fingerprints ainda — ausência de `/etc/pf.os` é tolerada) |
 
diff --git a/docs/pt-BR/pf-guide.md b/docs/pt-BR/pf-guide.md
index fa3abe8..6132dbe 100644
--- a/docs/pt-BR/pf-guide.md
+++ b/docs/pt-BR/pf-guide.md
@@ -63,7 +63,7 @@ matriz mudar.
 
 | Sintaxe | Até | O que acontece hoje |
 |---|---|---|
-| `nat-to`, `rdr-to` | — | **Verificado em lab** (gates `05-nat`, `06-rdr`; este último baixa 2 MB por um redirect e compara byte a byte). `nat-to (egress)` expande o *grupo* de interfaces do OpenBSD; num host multi-NIC prefira a forma explícita `nat-to (<iface>)`. `binat-to` ainda sem gate. |
+| `nat-to`, `rdr-to` | — | **Verificado em lab** (gates `05-nat`, `06-rdr`; este último baixa 2 MB por um redirect e compara byte a byte). `nat-to (egress)` expande o *grupo* de interfaces do OpenBSD; num host multi-NIC prefira a forma explícita `nat-to (<iface>)`. O `binat-to` é expandido pelo pfctl num par `nat-to … static-port` + `rdr-to` (gate `07-binat`). |
 | `scrub (…)`, `set reassemble` | M3 | O `pf_norm.c` roda dentro do `pf_test` (compilado) — o comportamento com fragmentos forjados não foi testado; trate o resultado como não validado. |
 | `divert-to`, tag `divert` | — | **Verificado em lab** (gate `11-divert`): o pacote é entregue a um socket `AF_DIVERT` (`PF_DIVERT=32`) atendido pelo `tools/pdivert`; sem listener é descartado, exatamente como o `divs_noport` do BSD. |
 | `route-to`, `dup-to`, `fail-to`, `reply-to` | M4 | Ainda não implementados como glue de roteamento Linux; as regras podem carregar, mas o comportamento é indefinido — evite. |
diff --git a/tests/vm/07-binat.sh b/tests/vm/07-binat.sh
new file mode 100755
index 0000000..50c94e0
--- /dev/null
+++ b/tests/vm/07-binat.sh
@@ -0,0 +1,48 @@
+#!/usr/bin/env bash
+# M3 gate: binat-to — bidirectional (static 1:1) NAT.
+#
+# Lab: the server (10.0.2.20) pings the client (10.0.1.10) through pf0.  The
+# binat rule rewrites the source to 10.0.2.50; the client's reply goes back to
+# 10.0.2.50, which pf0 owns in the mapping, and is translated to the server.
+#
+# Proves: outbound source rewrite + inbound destination rewrite with one rule,
+# and that the reply survives the state/translation path.
+set -uo pipefail; cd "$(dirname "$0")"; . ./lib.sh
+
+BINAT=10.0.2.50
+
+pf0 'insmod /opt/pf/pf.ko 2>/dev/null || insmod /tmp/pf.ko; true'
+pf0 '/opt/pf/pfctl -e; /opt/pf/pfctl -f /dev/null' >/dev/null
+
+cat > /tmp/g07.conf <<C
+pass quick proto icmp from $SRV_IP to $CLI_IP binat-to $BINAT keep state
+pass in quick proto icmp keep state
+pass out quick proto icmp keep state
+C
+pfload /tmp/g07.conf || { bad "binat rule load"; finish; }
+# pfctl expands one binat-to rule into the documented pair:
+#   pass out ... nat-to <mapped> static-port   (outbound half)
+#   pass in  ... rdr-to <real>                 (inbound half)
+RULES=$(pf0 '/opt/pf/pfctl -sr')
+echo "$RULES" | grep -q "nat-to $BINAT static-port" && ok "binat outbound half installed" || bad "outbound half missing"
+echo "$RULES" | grep -q "rdr-to $SRV_IP" && ok "binat inbound half installed" || bad "inbound half missing"
+
+# capture on the client side (resolve its transit interface, like pf0's)
+CLI_DEV=$(cli "ip route get $SRV_IP | grep -o 'dev [a-z0-9]*' | cut -d' ' -f2")
+[ -n "$CLI_DEV" ] || CLI_DEV=eth1
+cli "(tcpdump -ni $CLI_DEV -c 4 -e icmp > /tmp/bi.td 2>&1 &)" 2>/dev/null
+sleep 1
+srv "ping -c2 -W2 $CLI_IP >/dev/null 2>&1" && ok "ping srv->cli through binat" || bad "binat round trip"
+sleep 2
+
+TD=$(cli 'cat /tmp/bi.td' 2>/dev/null)
+if echo "$TD" | grep -q "$BINAT"; then
+	ok "request arrived from the mapped address $BINAT"
+else
+	bad "mapped address not seen on the client: $(echo "$TD" | head -2)"
+fi
+echo "$TD" | grep -q "$SRV_IP" && bad "original address $SRV_IP leaked" || ok "original source not leaked"
+
+pf0 '/opt/pf/pfctl -ss' | grep -q "$BINAT" && ok "state shows the mapping" || bad "no binat state"
+pf0 '/opt/pf/pfctl -d' >/dev/null
+finish