symkernel


Status	Experimental
Contract stability	Unstable
Recommended for	WasmAgent-ecosystem CEL/wazero/Z3 verification
Not recommended for	Standalone production policy engine

Symbolic verification backend for the WasmAgent ecosystem, written in Go.

Provides a three-tier reasoning service over HTTP, consumed by wasmagent-js, wasmagent-py, and any runtime that speaks the Criterion/ConstraintIR protocol:

Tier	Technology	Use case
Lightweight rules	cel-go	Fast policy evaluation (capability checks, constraint matching)
Hard isolation	wazero (WASM sandbox)	Untrusted code execution with memory + network caps
Formal proofs	Z3 SMT solver	Mathematical satisfiability for invariant and safety properties

Status

🚧 In development. See docs/15-milestones.md.

Milestone	Status
M1 — Foundation & CEL Integration	planned
M2 — wazero Sandbox	planned
M3 — Z3 Formal Verification	planned
M4 — Schema Alignment & Upstream Collaboration	planned
M6 — Policy Composition & Developer Experience	planned
OPA / Cedar compatibility — import Rego/Cedar policies as CEL (`internal/policyimport`)	shipped

Architecture

wasmagent-js / wasmagent-py / bscode
        │  HTTP  (Criterion/ConstraintIR protocol)
        ▼
  symkerneld (Go HTTP server)
   ├── GET  /v1/health           — liveness
   ├── POST /v1/verify/cel        — cel-go expression evaluator
   ├── POST /v1/verify/criterion  — wasmagent-js Criterion adapter
   ├── POST /v1/verify/z3         — Z3 SMT satisfiability (SMTLIB2)
   ├── POST /v1/verify/smt        — SMT solve with variable model
   ├── POST /v1/verify/symbolic   — symbolic execution (Wasm path exploration)
   └── POST /v1/verify/composed   — multi-tier policy composition
        │
        ├── internal/cel          — cel-go wrapper, per-request timeout
        ├── internal/policyimport — OPA Rego / AWS Cedar → CEL import (fail-closed)
        ├── internal/criterion    — Criterion/ConstraintIR adapter (cel_expr method)
        ├── internal/sandbox      — wazero runtime, trap→structured error
        ├── internal/z3           — Z3 via `z3 -in` subprocess (no CGO); backs /v1/verify/z3
        ├── internal/smt          — SMT solver abstraction over the same `z3` subprocess
        ├── internal/composed     — policy composition (ordered cel/smt/wasm stages)
        └── internal/verify       — /v1/verify/z3 + symbolic-execution handlers

Every response carries a decision_id (UUID) and evalMs for traceability, following GENAI_SEMCONV field naming to align with @wasmagent/otel-exporter.

Z3 SMT solver

The POST /v1/verify/z3 and symbolic-verification endpoints rely on the Z3 SMT solver. symkerneld does not link Z3 via CGO: internal/verify/z3.go shells out to the z3 executable in SMTLIB2 interactive mode (z3 -in). This keeps the Go build free of any native libz3 dependency — go build ./... succeeds without libz3-dev installed.

Runtime requirement: the z3 executable (Z3 4.13.x or later) must be on PATH on every host running symkerneld. Install it via your package manager (apt-get install z3 / brew install z3) or from the Z3 releases page, then verify with z3 --version.

Composed Policies

Composed policies chain multiple verification tiers (CEL → wazero → Z3) into a single request, with configurable fallback behaviour. This lets callers express rich policies like "the CEL check passes OR the Wasm sandbox confirms" without client-side orchestration.

`POST /v1/verify/composed`

{
  "tiers": [
    { "type": "cel",    "expr": "input.age >= 18" },
    { "type": "wazero", "module": "<base64-wasm>", "memory_limit_mb": 64 }
  ],
  "mode": "any_pass"
}

Composition modes

Mode	Behaviour	Use case
`any_pass`	Returns PASS as soon as any tier passes; remaining tiers are skipped. If all tiers fail, returns FAIL.	"Fail-open" policies — one positive signal is enough (e.g. allow if either rule engine or sandbox approves).
`all_pass`	Runs all tiers; returns PASS only if every tier passes. Short-circuits on the first failure.	"Fail-strict" policies — every guard must agree (e.g. CEL check AND Z3 proof).
`short_circuit`	Runs tiers in order; stops on the first definitive result (pass or fail) and returns immediately.	Latency-sensitive paths — fastest tier answers; slower tiers are fallbacks only.

Each tier can carry its own timeout_ms budget so that a slow Z3 call does not block a fast CEL decision.

Trace interpretation

Every composed response includes a trace array showing per-tier evaluation:

{
  "result": { "ok": true },
  "decision_id": "uuid-v4",
  "evalMs": 1.2,
  "trace": [
    { "tier": 0, "type": "cel",    "status": "pass", "evalMs": 0.04, "value": true,     "skipped": false },
    { "tier": 1, "type": "wazero", "status": "skip", "evalMs": 0,    "value": null,     "skipped": true,  "reason": "any_pass: previous tier passed" }
  ]
}

status: pass, fail, error, or skip.
skipped: true when the composition mode caused the tier to be bypassed (e.g. any_pass short-circuits after a pass).
reason: human-readable explanation of why the tier was skipped.
Enable verbose traces with the ?explain=true query parameter on any verification endpoint.

`symk` CLI quickstart

symk is the local development CLI (Milestone 6). It evaluates CEL expressions offline using the embedded evaluator — no running server required.

# Build
go build ./cmd/symk

# Single expression
symk verify cel --expr 'input.age > 18' --context ctx.json

# Without a context file (literal values)
symk verify cel --expr '42 > 0'

# Batch-validate a directory of policy YAML files
symk test-policy --dir policies/

# Check connectivity and auth against a remote symkerneld
symk doctor --addr http://localhost:8080

Example ctx.json:

{ "age": 21, "role": "admin" }

Batch verification (planned)

Planned — not yet implemented. There is no /v1/verify/batch route in cmd/symkerneld/routes.go today; the shape below is the intended design. Until it lands, submit items individually to /v1/verify/cel or /v1/verify/criterion.

The planned POST /v1/verify/batch endpoint would accept up to 1000 verification items in a single payload, executing them in parallel with a configurable concurrency limit (SYMKERNEL_BATCH_CONCURRENCY, default 16).

curl -s -X POST http://localhost:8080/v1/verify/batch \
  -H "Content-Type: application/json" \
  -H "Authorization: Bearer $SYMKERNEL_CLIENT_TOKEN" \
  -d '{
    "items": [
      { "expr": "input.age >= 18", "context": {"age": 21} },
      { "expr": "input.age >= 18", "context": {"age": 15} },
      { "expr": "input.role == \"admin\"", "context": {"role": "viewer"} }
    ]
  }' | jq .

Planned response:

{
  "results": [
    { "index": 0, "ok": true,  "decision_id": "a", "evalMs": 0.03 },
    { "index": 1, "ok": false, "decision_id": "b", "evalMs": 0.02 },
    { "index": 2, "ok": false, "decision_id": "c", "evalMs": 0.03, "hint": "condition false" }
  ],
  "totalMs": 12
}

Items that time out carry "timeout": true. Partial results are returned so the caller can identify and retry only the unfinished items.

Deployment

docker compose up          # local dev
make wasm && make test     # build + test

Designed for Cloudflare Containers (Phase 0/1) with a migration path to self-hosted VPS if Z3 p99 latency exceeds threshold.

Operational Runbook

Production operations documentation for running and maintaining symkerneld.

Guide	Contents
Deployment Checklist	Pre-flight checks, build steps, container build, Cloudflare deploy, schema drift, post-deploy verification, rollback
Environment Variables	`SYMKERNEL_ADDR`, `SYMKERNEL_CLIENT_TOKEN`, `CGO_ENABLED`, and planned M8 variables
Health Checks	Current operational endpoints (audit stats, cache stats, orchestrator stats) and planned `/healthz` hierarchy
Circuit Breaker Recovery	Current Z3 timeout behaviour, manual mitigation steps, planned M8 circuit breaker states
Decision Log Analysis	Audit log schema, export API, `jq` one-liners for pass/fail rates, tier distribution, duplicate detection
Capacity Planning	Resource consumption per tier, memory/CPU sizing, vertical vs horizontal scaling, cache tuning, SLO targets
OPA / Cedar Compatibility	Import existing OPA Rego / AWS Cedar policies as CEL (fail-closed), supported-subset matrix, and a worked Rego/Cedar → CEL → Z3-verified-invariant example

Multi-Tenancy

symkernel supports multi-tenant deployments via the tenant resolver middleware (internal/tenant). Tenant IDs are extracted from the JWT sub claim or the X-Tenant-ID header and validated against SYMKERNEL_ALLOWED_TENANTS.

An example configuration for three tenants with different quotas and memory limits is provided in deploy/tenant-config.yaml:

Tenant	Cache TTL	QPS / Burst	Memory	Use case
org-a	300 s	100 / 200	512 Mi	Production
org-b	600 s	50 / 100	256 Mi	Staging
org-c	disabled	20 / 40	128 Mi	Development

Key environment variables:

Variable	Description
`SYMKERNEL_ALLOWED_TENANTS`	Comma-separated allowlist of tenant IDs (`internal/tenant`)
`SYMKERNEL_CLIENT_TOKEN`	Auth token for the `internal/auth` middleware
`SYMKERNEL_ADMIN_TOKEN`	Admin token for `/v1/tenant/usage` and other admin endpoints (M9)
`SYMKERNEL_CACHE_TTL`	Redis-backed cache TTL in seconds; 0 disables caching (M9)
`SYMKERNEL_TENANT_QUOTA_DEFAULT`	Default per-tenant rate limit (requests/s) when not overridden (M9)
`SYMKERNEL_TENANT_QUOTA_OVERRIDES`	JSON map of `tenant_id → requests/s` for per-tenant quota (M9)
`SYMKERNEL_TENANT_MEMORY_LIMITS`	JSON map of `tenant_id → MiB` for wazero sandbox memory caps (M9)
`SYMKERNEL_RATE_LIMIT_QPS`	Token-bucket QPS (M8 milestone)
`SYMKERNEL_RATE_LIMIT_BURST`	Token-bucket burst capacity (M8 milestone)

Schema alignment

schemas/ holds constraint-ir.schema.json and constraint-violation.schema.json pinned from wasmagent-js. make sync-schemas refreshes them; CI fails on drift.

Part of the WasmAgent ecosystem.

Name		Name	Last commit message	Last commit date
.claude-bot		.claude-bot
.github/workflows		.github/workflows
api		api
bench		bench
cmd		cmd
deploy		deploy
docs		docs
internal		internal
schemas		schemas
wasmagent/symbolic-fixtures		wasmagent/symbolic-fixtures
.gitignore		.gitignore
.golangci.yml		.golangci.yml
BOT_STATE.md		BOT_STATE.md
CLAUDE.md		CLAUDE.md
Dockerfile		Dockerfile
LICENSE		LICENSE
Makefile		Makefile
README.md		README.md
docker-compose.yml		docker-compose.yml
go.mod		go.mod
go.sum		go.sum

Navigation Menu

Uh oh!

Repository files navigation

symkernel

Status

Architecture

Z3 SMT solver

Composed Policies

`POST /v1/verify/composed`

Composition modes

Trace interpretation

`symk` CLI quickstart

Batch verification (planned)

Deployment

Operational Runbook

Multi-Tenancy

Schema alignment

About

Releases

Packages

Contributors

Languages

Uh oh!

Latest commit

History

Folders and files

Repository files navigation

symkernel

Status

Architecture

Z3 SMT solver

Composed Policies

POST /v1/verify/composed

Composition modes

Trace interpretation

symk CLI quickstart

Batch verification (planned)

Deployment

Operational Runbook

Multi-Tenancy

Schema alignment

About

Resources

Stars

Watchers

Forks

Releases

Packages

Contributors

Languages

`POST /v1/verify/composed`

`symk` CLI quickstart