Checking it yourself

Fortell's pitch is that its rules are checkable rather than promised. This page is where that has to be made good.

Nothing here requires trusting a Fortell service. Everything it describes is a public Solana account you can look up in any block explorer, and everything Fortell's own transparency page shows is these same reads, done for you.

There is nothing on mainnet to check yet. Re-verified 2026-08-07 by asking mainnet for each of the four program addresses below: all four come back empty. What follows is correct for whichever network a program is deployed to, and today that is a private test fork.

#Start here: what is checkable and what is not

The most useful thing this page can do is be clear about the boundary, because a page that implies everything is verifiable is doing the opposite of its job.

The rest of this page is the "yes" rows.

#The addresses

Four programs. Each address is declared in its own source file, so the mapping from published source to deployed program is something you can confirm by building it and comparing.

Checked 2026-08-07 on mainnet, devnet and the fork:

That is one lookup per cell. Re-run it rather than believing the table.

#The five checks worth running

#1. Is a feature actually in the deployed program?

You do not need to rebuild anything to answer "is this feature in what is running". Every error message a Fortell program can produce is stored as plain text inside the deployed program, so the error strings work as a coarse but reliable version stamp. Fetch the program's data and search it for the message.

Search for the message text, not the internal name of the error. The internal name is not in the deployed bytes at all, and searching for one is how a feature that is present reads as absent. That has already happened once on this page.

#2. Is the first-loss buffer real?

This is the check Fortell's own review process requires be run rather than quoted, because a document asserting the answer has already been wrong once.

Read two numbers off the pool account, the recorded buffer and the part of it that live seats have reserved, then read the actual cash balance of the pool's own token account.

recorded buffer  <=  cash in the account
reserved         <=  recorded buffer
recorded buffer  >   0

The first is the one that makes absorption a movement of money rather than a bookkeeping entry. If the recorded buffer exceeds the cash, the first-loss guarantee is not backed and nothing else is worth computing. The third looks trivial and is not: every proved property about the buffer is true when there is no buffer.

#3. Is every live seat protected?

Every funded seat has a matching record in the pool saying how much capital it holds and how much cover was reserved against it. List them, and for each one confirm that its reserve equals the seat's own size multiplied by the seat's own drawdown limit. Then confirm that all those reserves sum to exactly the total the pool says is reserved, and that the total does not exceed the buffer.

The first equality is what the program enforces when it funds a seat, so a mismatch means either the account is not what it claims to be or the program has been replaced.

#4. Is a seat's risk engine armed?

Run this before believing any table anywhere, including the tier tables on this site. The answer is a property of one seat on one day. It is not a property of a tier and it must never be inferred from one.

Read the seat account and check five things:

• Its drawdown high-water mark and its daily reference are both above zero. A zero in either means that floor is inert.

• Its drawdown limit and daily loss limit are non-zero and no more than 100%.

• Its per-round cap and open-exposure cap are non-zero. This is the one that catches people: zero means the limit is switched off, not that no size is allowed. A seat with a zero open-exposure cap has no open-exposure limit at all.

• Its settlement destination is the pool you expect. A seat pointed at the wrong pool cannot return its capital to yours.

Why this matters rather than being pedantry: a seat is created with its size caps at zero, and they are set by a separate step immediately afterwards. For a period, every seat on the test fork read zero in all three size fields, so per-round sizing, total exposure and the minimum hold were enforced on none of them. The drawdown and daily floors still bound them, so they could not exceed their reserved cover, but the size limits were simply not on.

Two things have closed that since, and neither makes the limits a property of the tier. The step that provisions a seat now sets them without a human involved, and the program refuses to move capital into a seat whose size caps read zero. But the limits can still be changed on a funded seat afterwards. Read the seat.

And reading a field is not the same as knowing the limit fires. A non-zero value only means it is not switched off. To see one actually refuse, you need it to refuse a real trade, and Fortell tests them that way: on one railed $500 seat every limit was made to reject a live transaction on chain, each with its own error, and the same seat then traded and claimed successfully.

That test ran on the private test fork. No public explorer reaches it, so there is no identifier here for you to resolve, and this page quotes none. It is Fortell's account of a test rather than a check you have run, and it belongs in the "no" column above until there is a seat on a public network to repeat it against. The five checks on this page are the ones that do not require taking Fortell's word for it.

One quirk worth knowing when you read such a refusal. The size and loss limits are checked after the trade has run, against the money that actually moved, and the whole transaction is then discarded. So a refusal is a transaction in which the trade happened and was undone, which looks odd in an explorer and is the correct behaviour. The minimum hold is checked before, and does not.

#5. Does entry-fee revenue cover what it has committed?

The treasury records how much cover all outstanding challenge purchases may still require. Compare it against the treasury's actual balance.

More committed than held is legal and expected, especially early: a $75 sale commits $125 of cover. What is not legal is a withdrawal that creates a shortfall, and the program enforces that at the moment of withdrawal rather than when it is queued.

To check the withdrawal timelock is real, look for a queued-withdrawal record before every executed one and confirm the gap is at least the treasury's stated delay. Read that delay rather than assuming it is non-zero; a zero is currently representable.

#What formal verification does and does not mean

Fortell runs machine-checked property tests against models of its programs, and reports the results. This section is about what that is worth, because "formally verified" is a phrase that does more work in marketing than it deserves.

What it is. Four specifications describing what the programs must always be true of, compiled into randomised tests that hammer the model with tens of thousands of generated sequences. The load-bearing one states that backer capital is never eroded, and it is checked across every operation the pool can perform. It is not vacuous in the direction that matters: remove the guard that forces the buffer to fully cover a loss, and the tests produce a counterexample immediately.

What it is not. These are property tests over a hand-maintained model of the programs, with hand-applied patches to the generated test harness. They are strong protection against a future change quietly weakening a guarantee, and they are a genuine bug-finding tool. They are not a proof that the deployed program has the property.

Two documented cases where a green run meant nothing, both in this repository, both worth knowing before you take any pass count as evidence:

• One property was written to say that backer value does not fall across a settlement. The test backend silently dropped the part that referred to the previous state, so it compiled to "x is at least x". It would have passed forever while checking nothing. It was deleted rather than fixed, because a tautological property is worse than no property.

• Another property was added and passed, and was checking nothing at all: its precondition was satisfiable in principle and essentially never produced by random generation, so every case was rejected. A green run over zero executed cases looks exactly like a green run over ten thousand. What caught it was not the pass count. It was deleting the code the property was supposed to protect and noticing the tests stayed green.

Verification also found two places where the model was weaker than the real program, which is the more common shape of this failure and the more insidious one. A green run against a model that is weaker than the code proves something true about a system that is not the one deployed. A count of properties passing says nothing about whether they are the right properties.

Every buffer property is trivially true when the buffer is empty. A pool with no buffer satisfies all of them while offering backers nothing. Fortell's own rule is that the first-loss claim may only appear in user-facing copy once the properties pass and the pool actually holds a buffer, and the site enforces that in software rather than by remembering: the wording is derived from a live read, and a build gate refuses to ship a strong claim beside an unfunded buffer.

The practical instruction. A pass count is not evidence. Ask what fraction of generated cases actually ran rather than being thrown away, and ask whether anyone has deliberately broken the code to confirm the tests notice.

Also worth knowing: the on-chain programs have had one internal adversarial review, and it predates the entire first-loss buffer and the treasury program. Those surfaces have property tests and have not had a security pass. There has been no third-party audit.

#What you cannot check from the chain

Stated plainly, because the value of everything above depends on being clear about this.

• Whether a trader deserved their seat. Grading happens in a database. See who decides. What you can check is that a funded seat is inside the risk engine and that its cover is reserved.

• Whether the amount reported as returned when a seat closes matches the cash that actually arrived. The program does not reconcile those two. You can check it from outside by comparing the account's balance change in the same transaction against the reported figure.

• Seat history. Nothing indexes it. Current state only.

• What a pool share is worth at the exact moment you deposit. Share pricing uses the capital deployed into seats at its original size, which does not move until a seat closes, so a deposit or a withdrawal prices against that rather than against what the seats are currently worth. That gap runs in both directions and is not closed.