Security hardening for solver execution

[hyperpolymath]

Design sandboxed solver execution, resource limits, and safe temp handling.\n\nRefs: docs/wiki/Safety-Critical.md

[hyperpolymath]

Fixed in commits d3ec22b (verified-container-spec) and 0fa0c44 (Axiom.jl).

Implemented comprehensive containerization for SMT solver execution using svalinn/vordr + cerro-torre pattern.

Container Spec (verified-container-spec repo):

• Containerfile using cerro-torre base
• Guix channels for reproducible SMT solver builds (z3, cvc5, yices, mathsat)
• solver-runner.sh entrypoint with security checks
• svalinn-policy.json with comprehensive security rules
• Full documentation in README.adoc

Axiom.jl Integration:

• Rust FFI detects AXIOM_SMT_RUNNER=container
• Spawns containers via podman/svalinn/docker
• Backward compatible with direct execution modes

Security Features:
✓ Process isolation (PID, network, mount, IPC, UTS namespaces)
✓ Resource limits (2GB RAM, 2 CPU cores)
✓ Seccomp filter (syscall allowlist)
✓ No network access
✓ Read-only root filesystem
✓ Non-root execution (UID 1000)
✓ Capabilities dropped: ALL
✓ Reproducible builds via Guix
✓ Supply chain verification

Usage:

export AXIOM_SMT_RUNNER=container
export AXIOM_CONTAINER_RUNTIME=podman

@prove ∀x. x > 0 ⟹ (x + 1) > 0  # Runs in container

Pattern established for reuse in other Julia repos requiring external process isolation.