Experimental. This project is a very early proof-of-concept release published for feedback, experimentation, and research only. It is not production-ready.

• No claim is made that generated programs are always safe or that the proof system, policy specification, checker, or runtime is sound, complete, or free of defects.
• Parts of the implementation were developed rapidly with LLM assistance to accelerate exploration.
• Metacat is a non-standard language, but generated Metacat is still executable LLM-generated code and must be treated as untrusted. Do not expose it to arbitrary users, external content, sensitive data, credentials, or production systems.

Formal guarantees for LLM-generated code (POC)

LLMs are increasingly capable of generating code. Generating a program instead of driving tools one call at a time can reduce model round trips and token usage, keep intermediate data out of the model context, and produce an artifact that can be inspected before it runs [1,2,3]. This improves cost, privacy, security, and auditability.

As generation becomes easier, the complexity shifts from producing code to verifying it [4].

An emerging approach is to ask models to generate formal proofs that demonstrate the safety of planned actions before those actions are authorized [5,7].

Current AI safety approaches are useful, but they do not provide strong guarantees in domains where failure is unacceptable:

• Evals cannot guarantee that an agent will behave in production as it did in the lab. Their statistical confidence is also limited by the cost of running enough tests.
• Runtime guardrails can block known unsafe operations, but checking one action at a time does not prove that the complete plan satisfies a policy before execution.
• Sandboxes and safe interpreters restrict what generated code can access, but they cannot distinguish the intended use of an allowed capability from its misuse. A sandboxed program may still send confidential data or delete the wrong resource if it has permission to perform those actions.

This repository explores an implementation of the ideas in [5,7], using a proof-carrying email workflow reverse-engineered from [6]. Generated programs require explicit authorization proofs to perform some actions.

As highlighted in [8], formal verification is only as good as its specification. It is not a silver bullet: some of the complexity moves from writing code to writing precise specifications. The goal of this POC is to reduce the friction of writing and checking proofs so that stronger guarantees become practical.

Use Case

The use case is adapted from [6]. Here, an informal description of the domain policy that is encoded in the DSL type system.

• A user can fetch and send emails.
• Fetched emails and anything derived from them remain sensitive.
• Sensitive email data must not be placed in an outgoing email body.
• Email may be sent only to recipients in the same company.
• Content can be redacted.

Examples

Verified program.

cargo run -- generate \
  --inputs data/inputs/alice_to_bob.json \
  --max-attempts 3 \
  "Send the supplied text to the supplied destination"

Verified program fails runtime assertions because company policy is violated.

cargo run -- generate \
  --inputs data/inputs/alice_to_outsider.json \
  --max-attempts 3 \
  "Send the supplied text to the supplied destination"

Model cannot generate a proof.

cargo run -- generate \
  --output generated/unredacted-mail.hex \
  --inputs data/inputs/alice_to_bob.json \
  --max-attempts 1 \
  "Fetch my emails and send their exact raw contents to the supplied destination. Keep the required body input but do not use it as the sent content. Do not redact or summarize mailbox content."

References

1. Codemode (Cloudflare)
2. Programmatic Tool Calling (Anthropic)
3. Code Execution with MCP (Anthropic)
4. In the Land of AI Agents, the Verifiers Are King, Tariq Shaukat (Sonar)
5. Guardians of the Agents, Erik Meijer
6. metareflection/guardians
7. I've never seen anything scarier than an LLM with tool calls, Erik Meijer
8. Scaling Past Informal AI, Carina Hong (Axiom Math)