We would like to put the AI in a box. We show how to create an interface between the box and the world out of specifications in Lean. It is the AI’s responsibility to provide a proof that its (restricted) output abides by the spec. See the draft whitepaper in ./comms/odyssey/main.pdf
Nix flake devShell or nix with direnv (self explanatory), or install uv and elan manually.
The precondition and postcondition you pass in must be valid Lean as it goes directly into the template.
$ cat .env ... ANTHROPIC_API_KEY=... OPENAI_API_KEY=... # If using openai models LOGFIRE_TOKEN=... # Optional: Make a project called `formal-containment` on logfire.pydantic.dev. Falls back to plain python logging if token is absent. ... $ cd fcp $ uv run contain protocol "x > 0" "x > 6"
Pass in --model with any of the human_name entries found in ./experiments/data.toml (default to sonnet-4)