pi-aeon

An agent harness where formal verification is part of the agent loop — built on @earendil-works/pi-agent-core, policies as refinement types, proven by Aeon/Z3.

Install

curl -fsSL https://aeon.ucalyptus.me/install.sh | sh

The policy

def do_read (r:Resource) (s:Session) :
    {s2:Session | tainted s2 = (private_r r || tainted s)} := native "None";

def do_publish (s:{s:Session | tainted s = false}) : Unit := native "None";

Read private data → session tainted → publication becomes unprovable, hence impossible. Every tool call is checked by Z3 before it executes; a failed proof obligation is fed back to the model verbatim.

Links