I believe it works like this: - You write (or at least own verification of) LAWS.bend and don't give the AI you're going to writing the rest of the .bend code

I believe it works like this: - You write (or at least own verification of) LAWS.bend and don't give the AI you're going to writing the rest of the .bend code control of that file at any point - You ask your AI agent to write the rest of the .bend code for whatever you want it to do - The AI is free to write any other .bend code it'd like - The bend compiler takes all .bend files, including LAWS.bend - If the other .bend files don't act as a proof the rules in LAWS.bend are valid, it's a compilation error with where in the code the proof failed. - If the proof checks out, the program is built So the AI can write as much as it'd like but the only ways it'll result in anything but a compiler error back to the AI are: 1. You gave control of LAWS.bend to the AI and it took that permission to change the laws 2. The AI found a bug in the proof checker 3. The actual output generated by the compiler was bugged/sidechannel attackable/didn't match what the proof checker 4. What the AI wrote was compatible with the laws 1 is removing the guardrail itself. 2 & 3 are similar to how there can be a bug in the LEAN compiler or Rust type checker or etc. 4 is the intended usage+outcome. My main concern would be writing a LAWS.md for a complicated project which actually aligns with your intent is likely an astronomical task and would be so detailed it'd require proofs so complex even a valid program would take a long time to validate (if it ever did). Once you get past that step though you don't really have to worry about the rest.