Kontrol Formal Verification for SecurityCouncilAzorius

[lisandrasilva]

This PR adds a formal verification specification for the SecurityCouncilAzorius contract using Kontrol, the symbolic execution tool developed by Runtime Verification.

Background

This specification was developed by Runtime Verification based on the existing Certora CVL specification. The two tools are complementary and the Kontrol spec extends coverage to properties that CVL cannot handle due to dynamic array limitations.

What is Kontrol?

Unlike Foundry fuzz tests, which sample a finite number of random inputs, Kontrol performs exhaustive symbolic execution using the K Framework and KEVM. This means:

All possible initial states are covered at once — kevm.symbolicStorage makes every storage slot symbolic, so proofs hold for any reachable state of the contract, not just the state produced by the constructor.
All possible inputs are covered simultaneously — symbolic inputs represent every value a type can take, not a random sample.
Proofs are mathematical guarantees — if a proof passes, the property holds for every execution path, with no counterexamples missed.

Group	Tests
vetoProposal	post-condition integrity, isProposalVetoed consistency, access control
unvetoProposal	post-condition integrity, isProposalVetoed consistency, access control
vetoTx	post-condition integrity, revert on duplicate veto, access control
unvetoTx	post-condition integrity, revert when not vetoed, access control
multicall	invariant preservation, access control
checkTransaction	reverts iff txHash is vetoed, no storage modification
checkAfterExecution	never reverts, no storage modification
renounceOwnership	always reverts
transferOwnership	reverts on zero address, post-condition integrity, access control
supportsInterface	ERC-165 compliance for IGuard, IERC165, and rejection of 0xffffffff

In addition to per-function properties, four global invariants are checked after every state-changing call:

• I-1 ownerIsNotZero — owner is never the zero address
• I-2 azoriusIsNotZero — azorius is never the zero address
• I-3 ownerPreservation — only transferOwnership can change the owner
• I-4 azoriusIsImmutable — azorius address never changes
• I-5 storagePreservation — each function modifies only the expected storage slots

Additional coverage beyond Certora

Two properties that the Certora spec could not cover due to dynamic array limitations are fully verified here:

• I-18/I-19 vetoProposal/unvetoProposal integrity over symbolic txHash arrays — handled via MockAzorius.setSymbolicProposal, which uses KEVM cheatcodes to build unbounded symbolic txHash arrays directly in storage.
• I-26/I-27 isProposalVetoed consistency after veto/unveto — same technique.

In progress

T-13 test_multiCall is incomplete. calls: bytes[] is treated as symbolic raw bytes by KEVM, which cannot dispatch into the individual delegated functions. Full storage isolation and per-call effect verification require constructing calls as a symbolic array of properly ABI-encoded calls to known functions with symbolic arguments.