Quint spec review: verify invariants map to implementation behavior

[abienkowski]

Problem

The Quint formal specification (spec/docker_socket_policy.qnt) is the source of truth for security invariants, but it has not been formally reviewed against the actual guard/mutator behavior in the Go, Rust, and TypeScript implementations.

Solution

Perform a formal review of each invariant and confirm it maps to real code paths in all three implementations:

Invariant	Go	Rust	TypeScript
noPrivilegedAccess (privileged=false enforced)	ContainerConfigMutator	?	?
alwaysHostNetwork (network_mode=host)	ContainerConfigMutator	?	?
imagesAlwaysAllowed (allowed_image_prefix)	RegistryGate	?	?
validImagesOnly (invalid refs rejected)	createContainer guard	?	?
envOnlyFromFile (no inline env when env_file set)	EnvFileGate	?	?
proxyLives	error recovery	?	?
volumesInWhitelist	MountSourceGate	?	?
flagsInAllowlist	CmdGate	?	?
routingTableComplete	Router default-deny	?	?

Also verify:

• All endpoints in the routing table match the specs endpointsTable
• Exec is denied (execContainer unconditionally returns false) in all three languages
• Spec README invariants count (currently says 7, CHANGELOG says 9) is corrected to match reality

Which implementation(s) would this affect?

• Go
• Rust
• TypeScript
• Quint specification

Additional context

• Spec: spec/docker_socket_policy.qnt (P0 + P1 invariants, allInvariants)
• Verification: make verify / make typecheck / CI quint job
• Tracked by epic First release prep: Quint spec review, test parity, and release pipeline validation #4