Show HN: CSL-Core – Formally Verified Neuro-Symbolic Safety Engine for AI (github.com)
We built this because we realized that "prompt engineering" isn't enough for critical AI systems (like in finance or governance). You can't just ask an LLM nicely not to delete a database—you need a runtime guarantee.
CSL-Core is a policy language designed to bring "Policy-as-Code" to AI agents.
Instead of relying on the model's probabilistic nature, CSL enforces constraints that are:
1. Formally Verified: Policies are compiled into Z3 constraints to mathematically prove they have no logical conflicts or loopholes.
2. Deterministic: The checks happen in a separate runtime engine, independent of the LLM's context window.
3. Model Agnostic: It acts as a firewall between the LLM and your tools/API.
It's currently in Alpha (v0.2). Currently working on TLA+ specifications for the dual formal verification engine and governance architecture because we believe AI safety needs mathematical rigor.
I'd appreciate any feedback on the DSL syntax and our verification approach.
3 comments
[ 3.4 ms ] story [ 14.5 ms ] threadIt allows you to verify policies using the CLI without writing any Python code. I'd really appreciate any feedback on the DSL syntax or the verification approach. Thanks!
1. How does CSL handle the gap between what an LLM intends to do (based on its reasoning) and what constraints allow? For example, if a policy forbids "database modifications" but an agent legitimately needs to write logs—does the DSL let you express intent-aware exceptions, or do you end up with overly broad rules?
2. Z3 constraint solving can be slow at scale. What's your performance profile when policies are deeply nested or involve many symbolic variables? Have you profiled latency on, say, 100+ concurrent agent requests?
The formal verification angle is solid, but I'd be curious whether you've stress-tested the actual bottleneck: not the policy logic itself, but the interaction between agent reasoning and constraint checking when policies need to be permissive enough to be useful.
Should a (formally verified) policy engine run within the same WASM runtime, or should it be enforced by the WASM runtime, or by the VM or Container that the WASM runtime runs within?
"Show HN: Amla Sandbox – WASM bash shell sandbox for AI agents" (2026) https://news.ycombinator.com/item?id=46825026 re: eWASM and costed opcodes for agent efficiency
How do these userspace policies compare to MAC and DAC implementations like SELinux AVC, AppArmor, Systemd SyscallFilter, and seccomp with containers for example?