AIRLOCK Credit
Terms of the AIRLOCK credit pool
As in force on 10 November 2026. 20 clauses.
Each term links to the line that enforces it, the proof or test that covers it, and a transaction that shows it; the limits are terms too.
Parties
These terms bind the pool, the card it funds, the issuer who runs both, the borrower who holds the card, and every lender who deposits. Each contract signs with the hash of the code it runs, read from the chain on 10 November 2026.
- The poolpool.airlock-credit-c1108dSigned 38ECVv72iiyNuNW5FBBu2vDK6do46FZUEiKYskLeMyAY
- The cardcard.airlock-credit-c1108dSigned 6FCZRf51teMBxkLb2V5sc5bpLXDWws9RZgT3ERaUowTg
- The issuerairlock-credit-c1108d
- The borrowerborrower.airlock-credit-c1108d
- The agentagent.airlock-credit-c1108d
Shown code hashes, docs/EVIDENCE.md 350.
1. What the card and the pool do
- 1.1
Money leaves the card for a payee the issuer put in the card's address book, or goes back to the pool.
Enforced airlock-verdict/
src/ lib.rs 218 to 222, rule 9; Enforced airlock-policy/ src/ roles.rs 78 to 109, sweep pays the sponsor; Proved proofs/ Verdict.lean 115, p3_ allowed_ in_ book; Proved proofs/ Verdict.lean 12, allow_ iff; Kani airlock-verdict/ src/ proofs.rs 127, p03_ allowed_ recipient_ in_ book; Shown an injected payee held, transaction BNq34she… (EVIDENCE.md 373) tx; Shown a sweep back to the pool, transaction 25rQep4m… (EVIDENCE.md 378) tx. in force
- 1.2
A hijacked agent cannot choose the payee: a payee picked by outside text is held for a person to decide.
Enforced airlock-verdict/
src/ lib.rs 214 to 217, rule 8; Proved proofs/ Verdict.lean 105, p2_ p15_ allowed_ recipient_ trusted; Kani airlock-verdict/ src/ proofs.rs 117, p02_ p15_ allowed_ recipient_ trust_ set; Shown an injected payee held, transaction BNq34she… (EVIDENCE.md 373) tx. in force
- 1.3
The borrower cannot approve a payment to an account outside the book; the issuer can override it, and either of them can reject it.
Enforced airlock-policy/
src/ roles.rs 42 to 56, require_ settle_ role; Enforced airlock-policy/ src/ escalation.rs 447 to 451, the borrower cannot add payees; Tested airlock-policy/ src/ redteam.rs 519, rt_ con_ borrower_ pays_ himself_ is_ refused; Tested docs/ CLAIMS.md 38, claim C21; Shown the borrower's approve of his own account refused, transaction 12VC9dH5… (EVIDENCE.md 375) tx. in force
- 1.4
An amount read from outside text is never paid on the card; it is held for the owner, because no payee in the card's book has a cap for such amounts.
Enforced airlock-verdict/
src/ lib.rs 227 to 237, rule 11; Enforced airlock-policy/ src/ policy.rs 297, a payee without a cap; Proved proofs/ Verdict.lean 123, p4_ p14_ p23_ untrusted_ amount_ bounded; Kani airlock-verdict/ src/ proofs.rs 137, p04_ p14_ p23_ untrusted_ amount_ inside_ cap_ and_ budget; Measured docs/ BENCH.md 37, strict mode paid 0 of 250 attack runs, default mode 10 of 250; Shown the book without caps set on the card (epoch 2), transaction 3facSJMX… tx. in force
- 1.5
A payment that outside text decided to make is never paid by itself.
Enforced airlock-verdict/
src/ lib.rs 210 to 213, rule 7; Proved proofs/ Verdict.lean 96, p1_ untrusted_ pc_ not_ allowed; Kani airlock-verdict/ src/ proofs.rs 104, p01_ untrusted_ pc_ never_ allowed; Shown a bench run held as UntrustedTrigger, bench/ runs/ recorded/ transcripts/ own-S01.A1.1.json 215. in force
- 1.6
Every payment fits the task the owner signed, and what is left of that task shrinks with each payment.
Enforced airlock-verdict/
src/ lib.rs 202 to 209, rule 6; Proved proofs/ Verdict.lean 192, p21_ allowed_ in_ task_ bound; Kani airlock-verdict/ src/ proofs.rs 355, p21_ allowed_ inside_ task_ bound; Kani airlock-verdict/ src/ ledger.rs 385, l3_ task_ bound_ holds; Shown a payment allowed inside its task, transaction 5TKhYsPc… (EVIDENCE.md 372) tx. in force
- 1.7
A plain transfer to the pool cannot move the share price.
Enforced airlock-credit/
src/ lib.rs 3 to 5, own accounting fields; Enforced airlock-credit/ src/ lib.rs 176 to 179, assets_ at; Tested airlock-credit/ src/ tests.rs 156, a_ plain_ transfer_ to_ the_ contract_ cannot_ move_ the_ share_ price. in force
- 1.8
Deposits and withdrawals price a share the same way, and every rounding goes in the pool's favour.
Enforced airlock-credit/
src/ lib.rs 271, deposit; Enforced airlock-credit/ src/ lib.rs 305 to 307, withdraw; Enforced airlock-credit/ src/ math.rs 54 to 70, share math; Tested airlock-credit/ src/ math.rs 169, withdraw_ rounds_ down_ and_ never_ pays_ more_ than_ pro_ rata; Tested airlock-credit/ src/ math.rs 180, deposit_ then_ withdraw_ never_ gains; Tested airlock-credit/ src/ tests.rs 1011, property_ random_ operations_ keep_ the_ accounting; Shown a lender's 3 NEAR withdrawn as 3.03 NEAR, transaction 5qLww3EW… (EVIDENCE.md 380) tx. in force
- 1.9
An overdue line counts as zero in the share price before anyone calls default, and deposits stay closed while a line is overdue or a loss is unrecovered.
Enforced airlock-credit/
src/ lib.rs 162 to 169, impaired_ at; Enforced airlock-credit/ src/ lib.rs 263 to 270, deposit; Tested airlock-credit/ src/ tests.rs 746, an_ overdue_ line_ is_ impaired_ in_ the_ share_ price_ before_ anyone_ calls_ default; Tested airlock-credit/ src/ tests.rs 407, deposits_ are_ refused_ while_ a_ line_ is_ past_ due_ and_ reopen_ after_ default; Tested airlock-credit/ src/ tests.rs 644, deposits_ stay_ closed_ between_ a_ default_ and_ its_ recovery; Shown a deposit refused while a line was past due, transaction 5n4ZoQW6… (EVIDENCE.md 383) tx; Shown a deposit refused before a loss was recovered, transaction 6Hzfv7Jb… (EVIDENCE.md 385) tx. in force
- 1.10
A lender's shares can be withdrawn by that lender alone, once the hold has passed, from money the pool holds idle.
Enforced airlock-credit/
src/ lib.rs 291 to 314, withdraw; Tested airlock-credit/ src/ tests.rs 172, withdraw_ pays_ the_ pro_ rata_ amount_ down_ to_ idle_ and_ refuses_ beyond; Tested airlock-credit/ src/ tests.rs 701, shares_ are_ held_ for_ min_ hold_ ms_ after_ a_ deposit; Shown a lender withdraws all its shares, transaction 5qLww3EW… (EVIDENCE.md 380) tx. in force
- 1.11
On default the collateral pays the principal before the fee, and what it does not cover is a loss to the lenders.
Enforced airlock-credit/
src/ lib.rs 718 to 754, default; Tested airlock-credit/ src/ tests.rs 502, default_ seizes_ collateral_ principal_ first_ and_ books_ the_ rest_ as_ a_ loss; Tested airlock-credit/ src/ tests.rs 524, default_ with_ collateral_ above_ what_ is_ owed_ returns_ the_ rest; Shown a default: collateral seized, the rest a loss, transaction 6Pk6PR71… (EVIDENCE.md 384) tx. in force
2. Limits
- 2.1
The issuer books the payees, and the issuer can approve a held payment to a payee outside the book. This has not been done on chain.
Enforced airlock-policy/
src/ roles.rs 42 to 56, require_ settle_ role; Enforced airlock-policy/ src/ policy.rs 478, book_ set_ root; Tested airlock-policy/ src/ redteam.rs 519, rt_ con_ borrower_ pays_ himself_ is_ refused. in force
- 2.2
A booked merchant that colludes with the borrower can keep what it is paid. Nothing in the code prevents this.
Enforced nothing in the code.
in force
- 2.3
The pool and the card each hold one full-access key, held by the operator, so the operator can deploy new code to either. The agent holds a full-access key to its own account and a function-call key that can call submit_batch and expire on the card.
Shown the agent's function-call key added on the card, transaction FAyo8RPP… tx.
in force
- 2.4
The fee is charged on what the card kept, so a sweep before the repay lowers it, and a card that returns everything owes no fee.
Enforced airlock-credit/
src/ lib.rs 691 to 694, repay; Tested airlock-credit/ src/ tests.rs 458, repay_ charges_ the_ fee_ on_ what_ the_ card_ kept_ and_ returns_ the_ collateral; Tested airlock-credit/ src/ tests.rs 490, a_ fully_ swept_ line_ owes_ nothing; Shown a repay of 0.5 NEAR kept plus its 10 percent fee, transaction N2344KkG… (EVIDENCE.md 379) tx. in force
- 2.5
The issuer sets the terms of new lines. The collateral ratio of new lines changes at once in either direction, and open lines keep theirs. From the upgrade, a cut of the Passport base applies at once and a raise waits for the hold, 60 seconds on this pool.
Enforced airlock-credit/
src/ lib.rs 757 to 762, set_ collateral_ bps; Tested airlock-credit/ src/ tests.rs 556, the_ collateral_ ratio_ is_ the_ owner_ s_ and_ open_ lines_ keep_ theirs. from the upgrade
- 2.6
Lenders can leave 60 seconds after a deposit on this pool, and then for as much as the pool holds idle; money lent out waits for its repayment. Collateral is 30 percent of a line, and the pool bears any loss beyond it.
Enforced airlock-credit/
src/ lib.rs 309 to 313, withdraw; Enforced airlock-credit/ src/ lib.rs 22 to 23, collateral ratio; Measured docs/ EVIDENCE.md 390, the pool's hold, read from the chain. in force
- 2.7
All of this runs on NEAR's test network with test money. The issuer, the borrower, the merchant and the agent are the team's own accounts, and so are the two lenders of the recorded run.
Measured docs/
EVIDENCE.md 350, the accounts of the run. in force
- 2.8
The pool's terms rest on tests, not proofs. The Lean theorems and the Kani harnesses cover the payment gate of the card, the verdict function, and not the credit pool: terms 1.7 to 1.11 and limits 2.4 to 2.6 cite tests.
Tested airlock-credit/
src/ tests.rs 1011, the pool's property test. in force
- 2.9
An hourly loop borrows 0.09 NEAR from the pool, pays the booked merchant and repays with a 10 percent fee. Its borrower and merchant are the team's accounts, so the fee the lenders earn from it is the team's own money.
Enforced runtime/
src/ economy/ facts.ts 1 to 3, the loop's accounts; Enforced runtime/ src/ economy/ facts.ts 24 to 26, 0.09 NEAR at 10 percent; Shown the loop's repay with its fee, transaction C3ZKyFda… tx. in force
Schedule of cited files
Line numbers refer to the repository as of 10 November 2026. The check, scripts/terms-check.ts, fails when a cited line no longer holds what it names.
- bench/
runs/ recorded/ transcripts/ own-S01.A1.1.json - 215
- contracts/
airlock-credit/ src/ lib.rs - 3 to 5, 22 to 23, 162 to 169, 176 to 179, 263 to 270, 271, 291 to 314, 305 to 307, 309 to 313, 691 to 694, 718 to 754, 757 to 762
- contracts/
airlock-credit/ src/ math.rs - 54 to 70, 169, 180
- contracts/
airlock-credit/ src/ tests.rs - 156, 172, 407, 458, 490, 502, 524, 556, 644, 701, 746, 1011
- contracts/
airlock-policy/ src/ escalation.rs - 447 to 451
- contracts/
airlock-policy/ src/ policy.rs - 297, 478
- contracts/
airlock-policy/ src/ redteam.rs - 519
- contracts/
airlock-policy/ src/ roles.rs - 42 to 56, 78 to 109
- contracts/
airlock-verdict/ src/ ledger.rs - 385
- contracts/
airlock-verdict/ src/ lib.rs - 202 to 209, 210 to 213, 214 to 217, 218 to 222, 227 to 237
- contracts/
airlock-verdict/ src/ proofs.rs - 104, 117, 127, 137, 355
- docs/
BENCH.md - 37
- docs/
CLAIMS.md - 38
- docs/
EVIDENCE.md - 350, 372, 373, 375, 378, 379, 380, 383, 384, 385, 390
- proofs/
Verdict.lean - 12, 96, 105, 115, 123, 192
- runtime/
src/ economy/ facts.ts - 1 to 3, 24 to 26