Protocol Security Specification & Invariant Audit
A formal cryptographic specification of the Solana instruction introspection mechanism, milestone commitment integrity, anti-replay state machines, and sandboxed test isolation properties.
3SBmcsZq...ebtM•Execution Time: 0.57s•Suite: tests/test_all_security_invariants.pyTHREAT MODEL & PROTOCOL ASSUMPTIONS
TrancheLock assumes that the autonomous coding agent is an untrusted entity with access to public API specifications and language models. The sponsor is assumed to be an adversarial economic agent seeking to minimize capital expenditure. The verifier oracle is an authorized Ed25519 signer operating under isolated execution.
- Funds deposited into a vault PDA cannot be withdrawn by anyone until either (a) an authentic oracle proof releases the current tranche to the agent, or (b) the expiration timestamp is reached.
- Once a tranche is released to an agent, that capital is permanently inviolable. Clawback can only touch unreleased funds.
- A signature generated for milestone
Ncannot unlock milestoneN+1, nor can it be reused to claim milestoneNa second time.
ED25519 INSTRUCTION INTROSPECTION
Rather than searching transaction instructions for any valid Ed25519 signature, TrancheLock requires that the verification instruction occur immediately before release_tranche.
// 1. Current instruction index
let current_index = load_current_index_checked(instructions_sysvar)?;
// 2. Ed25519 MUST occur at current_index - 1
require!(current_index > 0, TrancheError::MissingEd25519Instruction);
let ed25519_index = (current_index - 1) as usize;
let ed25519_ix = load_instruction_at_checked(ed25519_index, instructions_sysvar)?;
// 3. Program ID check
require_keys_eq!(ed25519_ix.program_id, ED25519_PROGRAM_ID, TrancheError::InvalidEd25519ProgramId);
// 4. Single signature enforcement
let num_signatures = data[0];
require!(num_signatures == 1, TrancheError::MultipleSignaturesNotAllowed);
// 5. Exact 153-byte payload verification
require_eq!(message_data_size, 153, TrancheError::WrongMessageLength);
require!(pubkey_bytes == expected_pubkey, TrancheError::WrongOraclePublicKey);
require!(message_bytes == expected_message, TrancheError::InvalidMessageBytes);
FORMAL VERIFICATION AUDIT LEDGER
The complete 22-test invariant suite runs against the onchain state machine and introspection engine. All assertions pass deterministically:
Vault PDA initializes with exact multi-tranche allocations and bumps.
Valid Ed25519 signature immediately releases tranche funds to agent.
Forged or tampered oracle signature rejected by precompile.
Signature generated for Vault A cannot unlock Vault B.
Signature for Agent A cannot release funds to Agent B.
Proof for Milestone 1 cannot release Milestone 0.
Proof tampering with tranche amount fails byte check.
Proof with mismatched milestone spec hash rejected.
Re-submitting previously accepted proof fails with sequence error.
Transactions attempting release after vault completion rejected.
Sponsor cannot claw back capital before expires_at timestamp.
Sponsor can recover unreleased escrow strictly after expiration.
Released funds belong unconditionally to agent; cannot be refunded.
Non-sponsor signers cannot execute clawback refunds.
Signatures signed by unlisted keypairs fail pubkey match.
Payload serialization is strictly 153 bytes byte-for-byte.
Rejects Ed25519 instructions positioned anywhere other than ix[current - 1].
Rejects Ed25519 instruction data if message length != 153.
Rejects instruction offsets not pointing to exact precompile index.
Introspection verifies extracted public key bytes match vault oracle.
Rejects release if milestone spec hash does not match vault committed hash.
Replaying an identical signature transaction fails on current_tranche state increment.
SANDBOX ISOLATION & PRIVATE TEST CUSTODY
The verifier never claims "zero network leakage" without OS-level container enforcement. Development runs are tagged LOCAL_DEV (Network isolation NOT OS-enforced), while production harnesses enforce docker run --network none or E2B hardware microVMs.
Private test suites are never communicated to the agent. The verifier verifies SHA-256(test_suite) == vault.milestone_spec_hashes[idx] before execution. Mismatched suites trigger an instant verification abort with zero signatures generated.