[PROPOSAL] RFP-014 — Antumbra Liquidation: Increasing-Discount Collateral Auctions

[edenbd1]

RFP ID

RFP-014 — Liquidation & Auction Engine

Your Project Name

Antumbra Liquidation: Increasing-Discount Collateral Auctions

Team or Organization Name

Antumbra

Primary Contact

Telegram https://t.me/edenbdn or edenbaud1@gmail.com. Either reaches both of us within a day.

Team Members

Eden Baudin — engineer, privacy & ZK

• GitHub: https://github.com/edenbd1
• X: https://x.com/edenbdn
• Telegram: https://t.me/edenbdn
• LinkedIn: https://www.linkedin.com/in/edenbdn/
• Role: LEZ/SPEL program, on-chain integer arithmetic, public/private account
  model, Logos Core module and Basecamp mini-app, CI and reproducible evidence.
• λPrize LP-0005 — Private Balance Attestation: won and merged. A SPEL
  program on LEZ, accepted into this programme's own repository.
• Three further λPrize submissions currently open — LP-0002 Private M-of-N
  Multisig, LP-0003 Private Allowlist / Airdrop Distributor, LP-0008 Autonomous
  AI Module. Four prizes, four programs on the public LEZ testnet.
• 15+ hackathon wins. Shipping a working system against a deadline, which is
  the shape of a milestone.
• Ex-DevRel in privacy, across RWA and DeFi.
• Incubated at the Berkeley Blockchain Xcelerator.
• Former president of a blockchain association.

Nada Ahmadi — engineer, DeFi & AMM

• GitHub: https://github.com/nadaamd
• LinkedIn: https://www.linkedin.com/in/nada-ahmadi/
• Role: AMM pricing and precision-safe integer math, differential backtesting
  against real on-chain data, sale and trading front-end, wallet integration.
• Podium finish, Uniswap track, ETHGlobal Lisbon 2026 — Umbra, an autonomous
  circuit breaker for DeFi positions: it risk-scores a pool and evacuates funds
  through an on-chain Uniswap v3 swap, backtested over 48,000 real swaps.
• Full-stack developer at XRPL Commons.
• Member of DeVinci Blockchain, ESILV.

Project Summary

Requested: $55,000 over 12 weeks, all-in — $43,000 of milestone payouts
to us, paid on acceptance with nothing in advance, and $12,000 which is the
external auditor's own fee rather than ours.

The short version. The auction house this RFP specifies is already running
on the public LEZ testnet: a lot opened, partial fills bought at an escalating
discount, the lot exhausted and closed short, two configurations side by side,
and the instructions the program refused. Driving it is also how we found two
defects in our own engine, which are fixed, and which are still fetchable from
the first build's accounts. The rest of this document is how the other pieces
attach, and what we found in the specification while building the first one.
Every transaction below is listed in
DEPLOYMENTS.md.

This part is deployed, not proposed. The facts, a film of the session, and
the one command that re-checks all of them:

Program	antumbra_auction, live on the public LEZ testnet 0.2
ImageID	38ab5886d20784c8322d1c6a3595cc8a666568946acb63248bac8ecf1149bd57
Deploy transaction	ac43ac1a…9607a75b
Block	20377
Source	edenbd1/antumbra-auction — public, MIT OR Apache-2.0
Demo	the command below, run live against the public testnet — and the two accounts, fetched on camera

$ git clone https://github.com/edenbd1/antumbra-auction && cd antumbra-auction
$ ./scripts/verify-onchain.sh

scripts/verify-onchain.sh is the
whole of it, and CI runs the suite in release —
the profile that sets overflow-checks = true, because a debug run exercises
different arithmetic from the one that ships.

Nothing above needs our cooperation to check. The script talks to the public
sequencer, and it recomputes the deploy hash from the committed binary rather
than reading it from the table — a hash written down beside a file proves only
that someone wrote it down. It counts its own checks rather than printing a
number we typed, and a good few of them are things that must not resolve:
instructions the program refused, a hash never deployed, an address nobody ever
wrote. A check that only ever says yes is not a check.

But a prototype is not the argument, and we will not pretend it is. The
argument is that the platform risk in this RFP is already spent for us. λPrize
LP-0005 was merged into logos-co/lambda-prize after review, and three more
submissions are open. The parts of RFP-014 that are new-platform risk for anyone
starting now — SPEL program layout, the RISC0 guest build, chained-call token
movement, Basecamp module packaging, standalone-sequencer CI — are things we have
already done on this exact stack and had reviewed. The auction on chain is
evidence of that, not a substitute for it.

And the specification's dependency section is wrong in both directions. We
checked each dependency against the live runtime rather than against its prize
tracker, and two of the four are the opposite of what the document says:

Dependency	What RFP-014 says	What the chain says today	Effect on this work
LP-0012 events	Listed under "now delivered on LEZ, so they no longer gate this RFP"	getTransactionReceipt, getEvents and getLogs all answer Method not found. Asserted on every run of our verify script	A real blocker moved out of the blocker list. Liquidator discovery must poll account state. We price that, and design for it
LP-0013 token authorities	Listed as a hard blocker — "a token custodian … requires the transfer-authority primitives in LP-0013, currently open"	A program-owned holding account already custodies and pays out on the public testnet without it — antumbra_vesting funds an escrow through a chained call to the native transfer program, and refuses any funding account that program does not own. LP-0013 gates only the case where the payer is neither the signer nor the program	Not a blocker. Custody is designed to the credit-open / debit-owner rule, and swaps to the official primitive when it lands
Price feed (RFP-019 / RFP-020)	"RFP-020 delivers external price feeds; RFP-019 is an alternative once a DEX is live"	RFP-020 is awarded with 0 of 6 milestones delivered. RFP-019 is closed with no milestone issues at all	The one dependency that is genuinely missing. A reference source ships behind the same interface, so the engine works before either lands and swaps in one file after
RFP-001 / RFP-002 authorities	"closed (candidate picked) and the libraries are in development"	2 of 3 milestones delivered each. The only entry in that section that is accurate today	Built behind a thin local adapter matching the published surface; final conformance is a swap, and we say so

The pattern underneath: that section tracks issue status, not runtime
capability, and closed does not mean delivered. It is the reason the
milestone plan below never gates a payment on another team's undelivered work,
and the reason every dependency in it sits behind a trait we can satisfy
ourselves until the official one arrives.

A liquidation engine is an arithmetic problem wearing a protocol. Almost
everything that goes wrong with one goes wrong in a quotient — and the quotient
is the part that can be proven before anyone is paid. So we wrote it first.
edenbd1/antumbra-auction is
public, MIT OR Apache-2.0, 41 tests green, #![forbid(unsafe_code)], no
dependencies at all, and overflow-checks = true on the release profile —
because a debug run exercises different arithmetic from the one that ships.

It also found that this RFP's own named reference cannot be transcribed.
Section 1 below shows why, with the transcription in the repository so the claim
is a test result rather than a paragraph.

Technical Approach

1. The reference this RFP names does not compute on the platform it targets

The RFP points at Reflexer's IncreasingDiscountCollateralAuctionHouse and links
the GEB source. That code is Solidity: every intermediate is a uint256, which
holds 1.16e77. A SPEL program on LEZ computes in u128, which stops at 3.4e38.

Two of the reference's helpers overflow before any auction logic runs.

function rdivide(uint256 x, uint256 y) internal pure returns (uint256 z) {
    z = multiply(x, RAY) / y;          // RAY = 1e27
}

The product is taken first. A collateral price quoted in WAD is about 1e18 for a
unit priced at 1, so x · RAY is about 1e45 — seven orders of magnitude past
u128::MAX. The exact ceiling is u128::MAX / RAY, which is 3.4 × 10¹¹; as
a WAD price that is 0.00000034. Every price from a third of a millionth
upwards is out of reach. This is not an edge case reached by an extreme input.

And rpower, which compounds the discount per second by exponentiation-by-
squaring in ray scale, squares a number near 1e27. The first squaring is 1e54
— sixteen orders past the ceiling, before the exponent is even read.

Both are transcribed in a reference module and exercised by
tests at ordinary values, so this is executable. One test deliberately gives the transcription
numbers small enough to compute and asserts that it does: a transcription that
failed everywhere would prove nothing about the width.

The fix is not a bigger integer. The quotient always fits; only the product
does not. It is taken in 256 bits and divided back in one step with nothing
intermediate stored, reusing the widening multiply and restoring division whose
differential vectors and zkVM cycle counts already run in CI in
edenbd1/antumbra-lez. The discount schedule is linear in the multiplier rather than compounded,
because compounding is what forces rpower. It is monotone, reaches its maximum
at the deadline and stays there, and costs one mul_div instead of a loop whose
length is the age of the auction. A stepwise or exponential curve tabulates into
the same shape; what cannot be done is compounding a 1e27 rate in 128 bits.

2. The direction of that quotient is a withdrawal, not a rounding

collateral_out = bid · WAD / discounted_price

This has to round down. F3 requires partial fills, which hands the bidder
control of how many times the quotient is rounded. Priced at 2000 with no
discount, 2000 base units of coin buy exactly one base unit of collateral:

the same 2000 units, spent differently	collateral received
one bid of 2000	1
2000 bids of 1, rounding down	0
2000 bids of 1, rounding up	2000

Splitting the bid multiplies the collateral by the number of fills. Run to
completion, the bidder takes everything that was seized for one two-thousandth of
its value. R6's invariant — seized collateral equals collateral in auction —
is asserted directly over 600 awkward partial fills against an escalating
discount, and again on chain after every fill.

3. Health is a comparison of two products, and neither of them fits

Deciding a position is undercollateralised compares collateral · price against
debt · liquidation_ratio. A vault holding a million units of a collateral
priced at 2000 wants 2e45 on the left.

This is the worst of the three, because it fails quietly: with overflow checks
off the product wraps and a healthy position is declared liquidatable.
Neither product is needed — only the comparison. It is decided in 256 bits
without materialising either side, and the test checks it against real
multiplication everywhere a real multiplication exists, across the range either
side of 2⁶⁴.

Staleness is a state, not an error. R2 pauses liquidation for a collateral
type whose feed is stale and R4 says only that type pauses, so health returns
Paused rather than failing. An engine that treated a stale feed as an error
would take the whole system down for one bad oracle, which is what R5 forbids.
The age is a saturating subtraction, so a feed timestamped in the future does not
wrap into a very large age and pause everything.

4. A three percent minimum improvement is zero percent below thirty-four units

F4 and F5 want a debt auction and a surplus auction, and both guard
themselves with a percentage: a challenger must beat the standing value by beg.
Written in integers that guard evaporates as the numbers shrink. On the surplus
side 1 · 1.03 floors to 1 and 33 · 1.03 floors to 33 — the unchanged bid
clears its own threshold. A bidder re-posts the standing value, the expiry
resets, and the auction stays open for free while the system carries the bad debt
it exists to clear.

The fix is not a larger percentage. The improvement must move by at least one
base unit whatever the percentage works out to, and the threshold must round
against the challenger — ceiling on the growing side, floor on the shrinking one.
Two lines, and a test over every size from 1 to 200 that fails without either.

The spec licenses a stand-in for the token these auctions trade against —
"fully implemented and tested (using a mock token), but parameterized by a
configurable token address" — so the token is an address they never dereference,
and everything in them is real arithmetic over real state.

5. What is on chain today, and what it demonstrates

Two programs, because a program's id is its code and the second one is not the
first one. A 2% discount at open growing to 20% over an hour; ten base units of
collateral, priced at 2000, raising 20000.

	transaction	shows
start_auction	53004d4c…bde1fa8e	the lot opened
buy_collateral at t=0	66fe3871…639fec60	a partial fill, F3
buy_collateral at t=1800	559ef1a1…27df8a74	10.11% more collateral for the same bid, F2
a bid of 16000 on a lot worth 12569.59	3a5941a2…35190b9d	the price re-struck, the lot exhausted, and a shortfall booked
a second config, a second auction	0871332b…835d147f	F7 and R3

The auction account afterwards, read from the sequencer by anyone, and matching
what the library computes digit for digit:

collateral_seized     10000000000000000000
collateral_sold       10000000000000000000
collateral_left                          0     sold + left == seized, which is R6
raised            16569594129786746160000
to_raise          20000000000000000000000
settled                                  1

R6 is checkable without us. The invariant is not an assertion you have to
trust; it is two counters in a public account that a reader can add up.

And the auction closed 3430.41 short of its target, and said so. That is the
input F4's debt auction exists to consume, and it is the thing the next section
is about.

What it refused, which is what the successes mean anything against. A bid
dated before a fill already honoured; a settle on an auction neither sold out nor
funded; a settle on one already settled; a bid on an auction that does not exist;
a hash that was never deployed; and an account address nobody ever wrote. All
absent, each recorded by hash, with the auction account byte-identical after
each.

6. The two defects we found in our own engine, and where to fetch them

This is the part a prototype buys that a design document cannot. Both came out
of reading a live account rather than out of a review, and the first build is
left deployed on purpose so the evidence stays fetchable rather than described.

A bid larger than the lot was charged in full. quote clamped the collateral
handed out to what the lot still held, and went on charging a bid that had been
priced against a larger lot. The bidder overpaid — and worse, the auction
recorded raised == to_raise and reported itself fully raised while the
collateral it had actually sold was worth much less. A shortfall that is never
booked is one F4's debt auction never hears about, and F4 is a hard requirement
of this RFP.

We submitted that bid deliberately, so the defect has a public address:

Transaction	e46fb1ac…77555ae2, block 20376
Account	9xMhmHEsJXX18f4rBSwFkRKA9kwE2tQBEnKSCXpdK2yB
What it reads today	raised = to_raise = 5000·10¹⁸ — fully raised
What the config beside it allows	the schedule never sells above 95% of market
So the whole lot was worth at most	4750, at any moment of its life

Two public reads, no cooperation from us, and the account is internally
inconsistent. The fix re-strikes the price when it is the lot that ran out
rather than the target: the bidder pays for the collateral they receive, rounded
towards the auction, capped at the bid it replaces. Two named tests fail without
it.

And the on-chain R6 assertion was a tautology. The first build checked
left + (seized - left) != seized in
the guest program.
That is an identity: it holds for every value
of every field, including the ones a leak would produce, and it was never once
going to fire. An invariant needs two quantities that are maintained separately
or there is nothing to compare, so AuctionState now carries collateral_sold,
moved independently of collateral_left. That is also what makes R6 checkable
from the account rather than only inside our proof.

Neither of these is in the RFP's own list of things to watch for, and neither is
findable by reading a specification. They are findable by deploying, driving, and
then reading back what the chain actually holds — which is what our milestone
gates ask for, and why they ask for it.

7. Two measurements that change the design, not the marketing

A refused instruction costs a full proof: 430 s, against 62 s for a fill.
Measured, both. On this runtime a refusal leaves no receipt and no reason — only
"Transaction not found in preconfigured amount of blocks" — so a liquidator bot
cannot probe by trying. Seven minutes and a proof per rejected attempt, with no
diagnostic. It must read account state before submitting, which is precisely what
the RFP believed LP-0012's events had made unnecessary. That is a design
constraint. It is measured in M0 and paid for in M5, rather than discovered in
month three.

That is the explorer's own page, not ours. The Program ID on it is
38ab5886… — the ImageID at the top of this proposal, base58-encoded. Decode it
and the two agree, which is what ties the picture to the claim rather than
merely illustrating it.

A program's id is its code. The ProgramId is the ImageID of the guest, so
two deployers of byte-identical code get the same program id. F7's "Each product
deploys its own configured instance of the program" therefore cannot mean a
separate deployment unless the code differs — it means a distinct config account
under one shared program. That is also the better outcome: it is what makes the
RFP's own rationale, shared audits and shared liquidator tooling, true rather
than aspirational. Two configurations are live under one program today.

8. Every missing dependency sits behind a trait with a working default

The rule is uniform and it is what keeps this proposal's schedule ours: nothing
here waits on another award.

• Price — a PriceSource returning a value and an observation time. A
  reference implementation ships in-repo: an on-chain observation buffer with a
  time-weighted read, which is the consumer side RFP-014 actually owns. RFP-020's
  adaptor or RFP-019's TWAP substitutes at the trait boundary with no consumer
  change. Staleness and per-collateral pause are ours either way.
• Host CDP — a CollateralSource with seize and cancel_debt. A minimal
  reference host in-repo implements it and is documented as the conformance
  target. A stand-in written against a published interface is a conformance test
  of that interface; it is not a claim that the eventual counterparty behaves as
  assumed, and the README says so.
• Protocol token — a configurable address, exactly as F4 and F5 direct.
• Admin and freeze — a thin adapter matching RFP-001's and RFP-002's
  published surface, which are at 2 of 3 milestones. Final conformance is a swap
  once their third lands, disclosed as such rather than assumed away.
• Events — there is no shim for a capability the runtime does not have.
  Discovery polls account state, the cost of that is published, and if
  getEvents ever answers, our verify script fails loudly and we adopt it.

9. Time is an argument, so it is guarded

now is supplied by the caller. A caller who can rewind it re-prices a fill at an
earlier, shallower discount, so every instruction that reads the clock refuses a
now below one already honoured. The refusal is on chain above. Where the
runtime's clock accounts become ergonomically reachable, the same guard reads
block time instead, and the argument becomes a cross-check rather than the
source.

10. Soft requirements

Three are listed, and one of them is the invariant this proposal has already
spent a section on. All three are in scope.

Multi-oracle redundancy with a stale fallback — in scope, in M2. The
PriceSource trait already returns a value and an observation time, so a
redundant source is a second implementation behind the same boundary plus a
policy that chooses between them: the primary while it is fresh, the secondary
when it is not, Paused when neither is. That is a small amount of code on top
of what R2 and R4 already oblige us to write, and it is the difference between
one bad oracle pausing a collateral type and one bad oracle being routed around.

Formal verification of the auction invariants — in scope, in M6, and we have
already found the version of it that does not work. The RFP names exactly the
property this engine was built around: collateral seized equals collateral in
auction, and debt shortfalls are correctly propagated to the debt auction
house. Our first build asserted the first of those as
left + (seized - left) != seized, which is an identity — true of every number
there is, incapable of ever firing. The current build carries two counters moved
independently, and their sum is checkable from a public account by anyone.
Formal verification is the next step up from that rather than a new direction:
the properties are already written as executable assertions, and M6 discharges
them under a model checker instead of only over test vectors. We will report
which properties are proven and which are merely tested, because a proposal
that says "formally verified" without saying of what is the same tautology
written in prose.

A liquidator bot SDK with monitoring and automated triggers — in scope, in
M5. This is where the 430-second refusal stops being trivia. A bot that probes
by trying pays seven minutes and a full proof per rejected attempt and learns
nothing from it, so the SDK's monitor reads account state and submits only what
the arithmetic says will be accepted. The reference liquidator in M4 is that
loop, and its polling cost at a realistic position count is one of the two
numbers M0 exists to measure.

And what we are not proposing. The RFP's Out of Scope list — flash-loan
liquidations, batching aggregators, insurance funds, multi-collateral atomic
liquidations — is absent from this plan on purpose. Nothing in the design
forecloses them and none of them is billed here.

11. Requirement traceability

Every numbered hard requirement, what meets it, and how you can check.

#	Requirement (abridged)	How it is met	Evidence	Milestone
F1	Anyone can trigger liquidation on any undercollateralized position. No whi…	Permissionless liquidate: no whitelist, incentive paid from the seized lot	Three unrelated signers each triggering one, on testnet	M2
F2	Seized collateral is sold via auctions where the discount to market price …	Increasing discount, schedule per config, early termination on target or empty lot	Done on chain: the same bid bought 10.11% more 30 min later; the lot exhausted and the auction closed itself	M1
F3	Auctions support buying partial collateral lots, preventing large position…	Partial fills, clamped to what is left to raise and left to sell	Done on chain, including the fill where the lot ran out before the target and the price had to be re-struck	M1
F4	When collateral auctions don't raise enough to cover debt plus penalty, th…	Debt auction over a configurable token address; buffer absorbs first, freeze beyond it	Both branches e2e, the token-unset branch as the default configuration	M3
F5	When the protocol accumulates excess stablecoin above a threshold, surplus…	Surplus auction with burn, same configurable address; accrual is real penalties	Threshold crossing and burn e2e; accrual-only branch shown as default	M3
F6	Auctions follow strict state transitions with no reversals. All state chan…	Strict transitions; settled is terminal	Done on chain: settle-twice and settle-early both refused, account byte-identical after each	M1
F7	The system integrates with its host CDP protocol via a well-defined interf…	One program, one config account per product. A program's id is its code, so a separate deployment is not available	Done on chain: two configs, two concurrent auctions, isolated	M1
U1	Build the program using the SPEL framework, which generates the IDL and cl…	SPEL program; IDL and CLI generated from it	Done: idl/antumbra_auction.idl.json is committed and drives the CLI	M1
U2	Provide a Logos mini-app GUI with local build instructions, downloadable a…	Basecamp module loaded from a git repo, reading live auction state	Load verified against Basecamp's own Qt, with a deliberate failing control	M5
U3	Provide a CLI that covers core functionality of the program. The CLI may h…	CLI covering every instruction	Transcript of each against the public testnet	M5
U4	Tools display undercollateralized positions with estimated liquidator ince…	Position list with estimated incentive and a trigger; discovery polls state, because the runtime has no events	e2e against the reference host; polling cost published	M5
U5	Active auctions display collateral type, amount, current discount, raised …	Collateral, amount, current discount, raised against target, time remaining; preview is the same mul_div the program runs	Preview and fill diffed and asserted equal	M5
U6	Provide an SDK that can be used to build Logos modules for interacting wit…	SDK with the deshield-interact-reshield path	Driven twice already on antumbra-lez, with distinct ephemerals	M5
R1	Auction operations are non-reentrant. State transitions are ordered to pre…	One instruction, one pre-state, one post-state; transitions ordered	Re-entrant chained call attempted and refused; every transition pair enumerated	M1
R2	Liquidation uses time-weighted or confidence-adjusted prices, not raw spot…	Time-weighted read over an observation buffer; stale pauses that type	A mock feed allowed to go stale on chain while the clock advances	M2
R3	Multiple liquidations and auctions can occur simultaneously without interf…	Each auction is its own PDA; concurrency is isolation, not a lock	Done on chain: a fill on one auction left the other byte-identical	M1
R4	If a price feed fails for one collateral type, only that type's liquidatio…	Feeds map to collateral configs, so a failure is scoped to one	Two feeds, two types: stale one refuses, other succeeds	M2
R5	Other collateral types and non-liquidation operations continue unaffected.	Non-liquidation operations are not gated on any feed	Bidding and settlement continue on an open auction of the stale type	M2
R6	Critical invariants: seized collateral equals collateral in auction; debt …	Seized equals sold plus left, from two counters moved separately, asserted after every fill and readable off the account	Checkable on chain by anyone, and over 600 partial fills off it	M1
P1	Liquidation transactions complete within one block.	One instruction, no multi-transaction choreography	Inclusion block against submission block, measured	M2
P2	The system supports many concurrent auctions without exceeding compute lim…	Cost flat in the number of live auctions: each is its own account	Measured: a whole bid is 27,753 cycles, 0.083% of the session budget, and CI fails if that figure drifts	M4
P3	Bid transactions complete within one block.	One instruction per bid	Measured: a fill proves in 62 s and lands in the next block	M1
S1	The program is deployed and tested on LEZ devnet/testnet.	Deployed and driven on the public testnet	Done: ImageID 38ab5886…, deploy ac43ac1a…, block 20377	M1
S2	End-to-end integration tests run against a LEZ sequencer (standalone mode)…	e2e against a standalone sequencer with RISC0_DEV_MODE=0, in CI	The job runs; a skipped step counts as not run and fails the build	M6
S3	CI must be green on the default branch.	Green on the default branch	Green today on the auction crate; badge in the README	M6
S4	Every hard requirement in Functionality, Usability, Reliability, and Perfo…	One named test per hard requirement, in a coverage matrix	The matrix, with rows marked where a stand-in is the counterparty	M6
S5	A README documents end-to-end usage: deployment steps, program addresses, …	README with deployment steps, addresses and CLI walkthrough	Partly done: DEPLOYMENTS.md already carries addresses and the recipe	M6
Pr1	The mini-app and SDK must support both direct public account interaction a…	The operation handle can only be consumed by reshielding	A test asserting the refusal to drop it unreshielded	M5
Pr2	When using the private account path, the SDK must validate that the target…	Target validated as shielded before submission, explicit typed error	Public target rejected, private control passing in the same run	M5
Pr3	The ephemeral public account created during the deshield step must never b…	A fresh ephemeral per operation, published	Done twice already: two distinct ephemerals, no prior history, never reused	M5

That is all 30 numbered hard requirements.

Milestones, Payout and Timeline

Sequential and gated. No upfront payment on any milestone, including M0:
each is invoiced once it meets its stated gate, and Logos never pays ahead of
delivered work. Durations are calendar weeks for the two of us working
together, and they sum to the 12 the RFP asks for.

#	Deliverable	Effort	Payout
M0	Cost baseline and the two spikes that could change the design	1 wk	$3,500
M1	The auction house, hardened	2 wk	$7,000
M2	Liquidation, prices, and failure isolation	2 wk	$7,000
M3	Debt and surplus auctions, and the buffer	1.5 wk	$5,000
M4	The host interface, and a reference host	1 wk	$3,500
M5	SDK, CLI, mini-app, and the privacy path	1.5 wk	$5,500
M6	CI, tests, docs, and the testnet bundle	1 wk	$3,500
M7	External audit coordination and remediation	2 wk	$8,000
	Eight milestones, paid on acceptance		$43,000

M0 — Cost baseline and the two spikes that could change the design. 1 week,
$3,500. Measure the zkVM cycle cost of a fill, a liquidation and a settle
under the executor, tagged to the testnet version they were taken against,
because the per-transaction budget moves between releases. Two go/no-go spikes:
whether a chained call can seize from a host and initialise auction state in one
transaction, and what a liquidator's polling loop costs at a realistic position
count now that events do not exist. The external audit slot is also booked in
this week — firms are scheduled months out, and an audit milestone that starts
looking for a firm in week 11 is an audit milestone that slips. Gate: cost
numbers delivered and reviewed with Logos; both spikes answered in writing,
including if the answer is unwelcome; audit engagement confirmed in writing.
M0 shapes how we build; it does not decide whether the engine ships.

M1 — The auction house, hardened. 2 weeks, $7,000. What is on chain
today plus the missing lifecycle: reserve price, minimum bid, deadline handling,
and the re-entrancy and transition-pair tests in full. Gate: every F2, F3, F6,
F7, R1, R3 and R6 test green, and the lifecycle re-driven on testnet with each
refusal recorded by hash — which on this runtime is the only trace one leaves.

M2 — Liquidation, prices, and failure isolation. 2 weeks, $7,000. The
permissionless trigger and its incentive; the PriceSource trait with an
in-repo time-weighted reference; staleness pausing one collateral type while the
rest continues. Gate: three unrelated signers each liquidate on testnet; a feed
allowed to go stale on chain pauses its type only, with an open auction of that
type still accepting bids in the same run.

M3 — Debt and surplus auctions, and the buffer. 1.5 weeks, $5,000. Both
houses over a configurable token address, the surplus buffer, and the freeze
fallback when bad debt exceeds it. Gate: the shortfall path e2e against a mock
token; the token-unset branch demonstrated as the default configuration; the
minimum-improvement rule tested at the sizes where a percentage rounds to
nothing.

M4 — The host interface, and a reference host. 1 week, $3,500. The
CollateralSource interface, a minimal in-repo host implementing it as the
conformance target, and the published cycle table. Gate: seizure driven through
the interface on testnet; cycle costs published and shown flat in the number of
live auctions rather than asserted to be.

M5 — SDK, CLI, mini-app, and the privacy path. 1.5 weeks, $5,500. The
SDK with a non-skippable reshield and shielded-target validation; the CLI; the
Basecamp module reading live state; the position list and the bid preview.
Gate: the module loads in Basecamp with a deliberately failing control beside
it; a public reshield target rejected by name with a private control passing in
the same run; preview and fill diffed equal.

M6 — CI, tests, docs, and the testnet bundle. 1 week, $3,500. e2e
against a standalone sequencer at RISC0_DEV_MODE=0 in CI, the coverage matrix
with one named test per hard requirement, and a README a reviewer can follow
without us. Gate: CI green on the default branch with the e2e job actually
running — a skipped step counts as not run — and the published addresses aged
past the explorer's indexing lag before we call it done.

M7 — External audit coordination and remediation. 2 weeks, $8,000. The
firm booked in M0 reviews the frozen tree. This figure is our work: scoping
the review, coordinating the firm, remediating what it finds and re-verifying
afterwards. The auditor's own fee is a separate itemised line, to be scoped
with Logos. A review by a firm of the standard an engine holding seized
collateral needs costs an order of magnitude more than any milestone in this
plan; folding it into one of them would put a number in this proposal that could
not survive being checked, which is the opposite of what the rest of it is for.
Priced at the same weekly rate as the other milestones here. The engine
custodies seized collateral, and the proposal template asks for an audit
milestone where a project handles funds. Gate: report delivered, every finding
remediated or accepted in writing with the reason, re-verification passed.

On the number. $55,000 all-in: $43,000 of milestone payouts to us,
plus the external auditor's own fee of $12,000 — money that goes to the
firm and never reaches us, itemised here so the figure is a budget and not a
starting position. We propose Trail of Bits, Zellic, NCC Group or another firm
with a Rust and zkVM practice, mutually agreed with Logos; the scope is the
arithmetic core, the escrow path and the guest program, and a broader engagement
is a separate decision with a separate number rather than a surprise. It is not
under-scoping. The auction arithmetic, the SPEL program and the deploy-and-drive
path are already built and already paid for by us, which is what an experience
dividend looks like from the buyer's side. Between us we have shipped four
programs on this stack, one of them merged into this programme's own repository,
so the ramp-up another team prices into month one is not in this plan.

On the schedule. The RFP estimates 10–12 weeks. The durations above are
effort, not calendar; run strictly sequentially they sum to 12 weeks, and
that is the number we commit to — the top of the range rather than the middle,
because each milestone here is gated on evidence produced by the one before it
rather than on a hand-off. The critical path is M0 → M1 → M2 → M3 → M6 → M7,
which is 9.5 weeks. M4's host interface and M5's SDK, CLI and mini-app sit on
the second track from the end of M1 — the role split declared above rather than
a scheduling convenience — and they are inside the twelve only because we would
rather gate their payment behind the engine being right than run them early for
the calendar. M7's audit is a third party's diary, not ours, which is why the
firm is booked in M0. We flag rather than hide the one dependency we do not
control: M2's price work and M4's host work are built against in-repo
references, so neither slips if RFP-019, RFP-020 or a CDP host lands late — but
the conformance swap to whichever Logos selects is post-delivery work, and it
sits in the Post-Delivery Plan rather than being smuggled into a gate here.

Total Requested Budget (USD)

$55,000

Relevant Experience

We have already shipped on this exact stack, in this programme, and it is
public and checkable.

λPrize LP-0005 — Private Token Balance Attestation. Won, and merged into
logos-co/lambda-prize.

• Submission PR: Solution: LP-0005 — Private Balance Attestation lambda-prize#64 (merged)

• Code: https://github.com/edenbd1/lp-0005-private-token-balance-attestation

  A SPEL program on LEZ with RISC0 threshold proofs over shielded accounts,
  verifiable both on-chain and off-chain over Logos Messaging. It went through
  this programme's own review and was accepted.

Three further λPrize submissions are open right now, all on the public LEZ
testnet, all four programs written by the same two people:

• LP-0002 Private M-of-N Multisig —
  Solution: LP-0002 Private M-of-N Multisig lambda-prize#125 ·
  https://github.com/edenbd1/lp-0002-private-multisig

• LP-0003 Private Allowlist / Airdrop Distributor —
  Solution: LP-0003 Private Allowlist / Airdrop Distributor lambda-prize#126 ·
  https://github.com/edenbd1/lp-0003-private-airdrop-distributor

• LP-0008 Autonomous Agent Module —
  Solution: LP-0008 — Autonomous AI Module with Wallet, Storage, and Messaging lambda-prize#129 ·
  https://github.com/edenbd1/lp-0008-autonomous-agent-module

  Between them these cover the surface this RFP asks for: SPEL programs and
  IDLs, PDAs and account models, the shielded/public account boundary,
  on-chain proof verification, Logos Core C++ modules and Basecamp mini-apps
  loaded from a git repo, CLIs, and CI that runs end-to-end against a real LEZ
  sequencer in standalone mode.

The math for this RFP is already written, public, and running in CI.
https://github.com/edenbd1/antumbra-lez — MIT OR Apache-2.0, 50 tests green.

The CI is worth thirty seconds of your time, because it checks the claims and
not only the tests:

• the suite runs in release, since that profile sets
  overflow-checks = true — a debug run exercises different arithmetic from the
  one that ships, which is how a wrapping bug reaches production past a green
  build;
• the committed differential vectors are regenerated and diffed against
  their Python generators, because a committed oracle's real failure mode is
  not being wrong, it is being edited to make a failing test pass;
• and the zkVM cycle table is re-measured on GitHub's own runners under the
  RISC0 executor and compared against the published document, so a figure we
  quote here and a figure a reader reproduces cannot disagree.

That last job is the one to look at:
https://github.com/edenbd1/antumbra-lez/actions/workflows/ci.yml — green,
including the executor run, which means every cycle count in this proposal is
reproducible by someone who has never spoken to us.

Eden Baudin — privacy and RWA engineer, ex-DevRel in privacy computing
across RWA and DeFi: the side of the table that finds out which document is
wrong and which SDK breaks under a real integration. 15+ hackathon wins, which
is the same shape as a milestone: a working system against a fixed date.
Incubated at the Berkeley Blockchain Xcelerator.

Nada Ahmadi — DeFi and AMM engineer. Podium finish on the Uniswap track at
ETHGlobal Lisbon 2026 with Umbra (https://github.com/nadaamd/umbra), an
autonomous circuit breaker that risk-scores a pool and evacuates a position
through an on-chain Uniswap v3 swap, backtested over 48,000 real swaps —
directly the AMM-pricing and differential-backtesting work this RFP needs.
Full-stack developer at XRPL Commons. Member of DeVinci Blockchain, ESILV.

How this maps to the recommended team profile. The RFP lists six
competencies. Here is where each already exists rather than being promised.

The RFP asks for	Where it is, and how you can check
DeFi protocol design (liquidation systems, auction mechanisms)	The auction house above, deployed and driven — plus the finding that the RFP's own named reference cannot be transcribed on this platform
Solana or SVM program development	LEZ's account model is SVM-shaped — PDAs, ATAs, IDLs, program-owned state — and SPEL is its Anchor. Five programs written against it, one merged after review
Auction theory and mechanism design	src/lib.rs and src/settlement.rs — the discount schedule, the partial-fill rounding proof, and the minimum-improvement rule that stops working at small sizes
Oracle integration and price feed security	src/liquidation.rs — staleness as a state rather than an error, isolated per collateral type, with the age measured so a future timestamp cannot pause everything
Writing and running on-chain tests	41 tests green with no dependencies, plus an on-chain check script whose controls are refused instructions, a hash never deployed, and an address nobody wrote — it counts them itself rather than quoting a number here
Front-end development for DeFi applications	Nada Ahmadi — Umbra, a Uniswap-track podium at ETHGlobal Lisbon 2026, and full-stack work at XRPL Commons

Post-Delivery Plan

Six months of support, included, with no ongoing cut. No revenue share, no
protocol-fee percentage, no retainer. Logos gets a maintained primitive rather
than a commercial dependency.

The three swaps we have designed for, and will perform. Each is a trait
boundary today, so each is a small change rather than a rewrite: the price source
to whichever of RFP-019 or RFP-020 Logos selects; the admin and freeze adapters
to RFP-001's and RFP-002's libraries when their third milestones land; and
custody to LP-0013's transfer authorities if a deployment ever needs a payer that
is neither the signer nor the program. We will do these within the support
window at no additional cost.

If the runtime gains events, we adopt them. Our verify script asserts today
that getTransactionReceipt, getEvents and getLogs answer Method not found. The day that assertion fails, it fails loudly and we replace the polling
discovery path with a subscription — which is a better liquidator bot and a
cheaper one.

Version churn is ours. LEZ is pre-mainnet and its runtime will move. Cycle
figures are published tagged to the testnet version they were measured against,
and keeping the engine current across upgrades during the support window is part
of this commitment rather than a change request.

Beyond six months, we are glad to keep maintaining it; if Logos wants a
longer operating commitment with an SLA, we will scope and price one separately
rather than promise a response time we have not staffed.

Permissions and Consent

• I/We confirm Logos may contact me using the primary contact information provided above for follow-ups and next steps.
• I/We consent to Logos using information from this proposal publicly such as blogs case studies social posts or analytical reporting. Redactions can be requested at any time.

Program Requirements

• I/We have read and agree to the Logos RFP Terms and Conditions and I understand that no Grant is awarded and no right to payment arises unless a Grant Agreement is executed.
• I/We understand that RFP specifications are proposals rather than instructions, that Logos makes no representations as to their legal or regulatory treatment, and that we are responsible for assessing what we build, deploy or operate and for complying with the laws that apply to us.
• I/We understand this project must be open-sourced under the MIT and Apache 2.0 Licenses unless explicitly approved otherwise.
• I/We are prepared to deliver milestone-based outcomes.

[edenbd1]

Demo, recorded against the public LEZ testnet

antumbra-014-liquidation-auction.mp4

Nothing here is mocked or replayed from a file: every command is really executed
in the session you see, and every figure on screen is derived from account data
fetched during it rather than from numbers we already knew. Every check the film
performs re-runs from a clean clone with one command:

git clone https://github.com/edenbd1/antumbra-auction && cd antumbra-auction
./scripts/verify-onchain.sh

The middle of the film is the part worth the two minutes. It fetches two
accounts on the same public chain: the first build of this engine, which reports
itself fully raised on a lot its own configuration could never have sold for
that much, and the build that fixes it, which closes short and books the
shortfall. Two public reads, no cooperation from us.

Program	antumbra_auction
ImageID	38ab5886d20784c8322d1c6a3595cc8a666568946acb63248bac8ecf1149bd57
Deploy transaction	ac43ac1a…07a75b
Source	https://github.com/edenbd1/antumbra-auction

Subtitles are burned into the picture, so the film is followable with the sound
off.