Agent Approvals - formally verified
Differential publishes an Approval Contract on the NEAR blockchain as a building block for agent trust systems, along with formal proofs of its behavior.
Should your agent build out the new product line? Sign this contract? Disburse a grant?
Key control points like these need approval from an accountable party. As much as we would like to do everything, businesses rest on making choices about what to do and not do. Frameworks like ISO 27000 and SOC are designed to verify the business controls around these choices.
The higher the stakes the more the control needs to resist subversion, log the decision, and resist log tampering. An agent (or system of 1000s of agents) that can re-write control policy files or work around them is likely to eventually do so.
Fortunately distributed cryptographic ledgers provide solutions to this problem and are widely available. For day to day cases like Pull Request approvals you may use ledger features of your company or team’s database. For interactions with vendors and partners you may use a private blockchain like the ones JP Morgan uses for settlement or Intel uses for chip verification. For interactions with customers, public proofs, or simply the highest stakes decisions, a public blockchain provides the capabilities we need.
As part of our research on Boundary Enforcement, Differential is publishing an Approval Contract that works on the NEAR blockchain. NEAR is a high performance, low-cost public blockchain that supports smart contracts, thus is well suited to this application. The approval contract is a minimal building block for trust systems. It uses the distributed execution, immutable logs, and signing keys that NEAR provides.
Other systems can then use deterministic code to read and verify those approvals before triggering the approved action: beginning the project, signing the contract, releasing the funds.
Ok, but does it work? How reliable is it? This is where the real work (for us) begins. Formal verification allows us to mathematically prove the behavior of the approval contract. We use a multi-layer strategy to prove low-level design, the limits of the implemented code, system behavior, and consistency of requirements.
Does the contract behave how it says it does? Read the mathematical proofs.
Want to see it in action? In this video we approve each line of the specification, 'what the approval contract should do'. That specification is what is being formally proved. And where do we write these approvals? To the approval contract of course!