我不审查AI的算术：定理证明器来做

New Story I Don't Review My AI's Arithmetic: A Theorem Prover Does by Alexander Kalankhodzhaev September 8th, 2026 TLDR Your browser does not support the audio element. byAlexander Kalankhodzhaev@kalaninja byAlexander Kalankhodzhaev|@kalaninja Core Engineer Lead at Raiku Story's Credibility Parts 1 and 2 solved two problems I don’t want an AI to be able to hide. The first was the environment. Toolchains are pinned, builds are hermetic, and the agent works through one reproducible command surface. The second was the data layer. Wrong account type? Parse failure. Wrong PDA? Validation failure. Silent layout change? Compile failure. That still leaves the part that worries me most. The logic. Can sold ever exceed capacity? Can a payment multiplication overflow? Can an error path mutate state halfway through an instruction? Can a refactor change a field it was never supposed to touch? Tests help. But tests only cover cases somebody thought to write. When an AI writes most of the implementation, I want something stronger than my ability to imagine its mistakes. So, the final layer of this repository is a verification boundary: thin trusted shells that talk to Solana, and pure verified cores whose contracts are proved with Creusot. The AI can write the arithmetic. A theorem prover gets the final word. 1. Tests check what you thought of The companion program sells tickets to events: create an event with a fixed capacity and price, buy tickets, then close sales. Twenty-two Mollusk integration tests exercise the real compiled program through the paths I could think of: normal purchases, sold-out events, impostor organizers, replayed transactions, failed closes. That phrase — the paths I could think of — is the limitation. The questions I actually care about are universal. Can sold ever exceed capacity, for any valid state and any sequence of calls? Can quantity * price ever overflow? If a purchase returns an error, is the event unchanged on every error path? A test suite samples that state space. A proof quantifies over it. Rust has a tool for doing exactly that. 2. Trusted shells, verified cores Creusot cannot meaningfully verify Solana syscalls, CPIs, account borrows, or the runtime itself. I don’t want it to. Instead, the crate is split at exactly that boundary: mod domain; mod flows; #[cfg_attr(creusot, trusted)] mod instructions; There are three layers. instructions/ contains the imperative shells. They parse accounts, create PDAs, read the clock, transfer lamports, and persist the result. Anything that touches the Solana runtime lives here. Creusot treats this module as #[trusted]. That means the prover assumes it. So humans review it. And because humans have to review it, I keep it intentionally small and boring. flows/ contains one verified decision core per instruction. These are pure functions over wire-level values. No accounts. No CPIs. No I/O. They receive state, make a decision, and return what the shell should persist. This is also where domain operations are called, which matters because their preconditions become real proof obligations instead of documentation. domain/ contains the vocabulary: state predicates, constructors, mutators with contracts, and a few small trusted wrappers for foreign types Creusot doesn’t model directly. Everything verification-specific is behind cfg(creusot). The SBF program ships the same implementation with none of the specification machinery in the binary. The proof layer disappears at compile time. 3. Specs you can actually read. Creusot contracts are written in Pearlite, its Rust-shaped specification language. A few pieces of syntax go a long way: x@ lifts a machine integer into an unbounded mathematical integer. *self means the value before a mutable borrow. ^self means the value after it. #[logic] functions define predicates the prover can reason about. For each state type I use three concepts: invariant: what must always be true. is_initial: what a constructor establishes. is_legal_transition_from: what one valid state is allowed to change into. For an Event, the core invariant is small: fn invariant(self) -> bool { pearlite! { self.organizer.is_set() && self.sold@ (*self).is_status_sales_open() && actual.int() == int_min( requested.int(), (*self).capacity.int() - (*self).sold@, ) && actual.int() * (*self).price_lamports.int() !(*self).is_status_sales_open() || (*self).sold@ == (*self).capacity.int(), }))] #[cfg_attr(creusot, ensures(match result { Ok(_) => (^self) == Event { sold: (^self).sold, ..*self }, Err(_) => (^self) == *self, }))] fn record_sale( &mut self, requested: NonZeroU64, ) -> Result { There are four guarantees hiding in there. First, the invariant survives every exit. Not only Ok. Every exit. If the function returns an error, the resulting event still has to be valid. Second, the clamp is exact. If ten tickets are requested and only three remain, the result is not merely required to be “ bool { pearlite! { self.header == prev.header && self.created_slot == prev.created_slot && self.organizer == prev.organizer && self.capacity == prev.capacity && self.price_lamports == prev.price_lamports && self.name == prev.name && self.bump == prev.bump && self._reserved == prev._reserved && self.sold@ >= prev.sold@ && is_legal_event_status_transition(prev.status, self.status) } } This is the account’s constitutional law. Headers do not change. The organizer does not change. Capacity and price do not change. The ticket counter cannot move backward. Status can only follow the legal state machine. Every verified flow that mutates an event then proves: ensures((^event).is_legal_transition_from(*event)) That contract is independent of record_sale’s frame. Now widen the frame and rewrite the price. The mutator may still prove against its own contract. But the flow above it doesn’t. I tested this by breaking the implementation on purpose. I allowed the price write in the mutator’s frame and the mutator stayed green. purchase went red. That’s exactly what I wanted. The two specifications are deliberately redundant. Under correct code, the operation-specific frame already implies the account-level transition rule. The redundancy matters only when one of them is wrong. Two locks written at different levels. 6. Make forgetting impossible too. There is still one embarrassingly mundane failure mode. Someone could add a new mutable flow and simply forget the transition clause. No theorem prover can verify a contract that does not exist. So scripts/check-ticketing-transitions.sh scans every flow that accepts an account by &mut and fails if the transition guarantee is missing. It runs before every Creusot verification and replay. Yes, the guardrail in front of the theorem prover is a shell script with grep. I like that. Formal methods don’t make simple checks obsolete. They make it clearer where simple checks are enough. 7. One contract, written once. Creusot prefers contracts on extension traits. I don’t want the AI maintaining one copy of a precondition on a trait and another on the implementation. Duplicated specifications are exactly the kind of thing that drift. So domain operations are written once as an inherent impl: #[creusot_extension(trait EventOps)] impl Event { // ... } A small procedural macro generates the extension trait Creusot expects and copies the requires clauses to the necessary locations. The important detail is what the macro is not. It is not trusted. It expands into normal Rust before Creusot sees the crate, and Creusot verifies the generated result like everything else. If the macro generates something inconsistent with the proof, verification fails. The macro removes boilerplate without enlarging the trusted computing base. 8. Who proves the precondition? There is an important trap in deductive verification. Suppose record_sale says: requires((*self).invariant()) Creusot checks that requirement at the call site. But instructions/ is trusted. A call from trusted code can assume the precondition instead of proving it. Do that carelessly, and you end up with a beautiful proof of “if the account was valid, then everything works” while nobody ever proves that the account was valid in the first place. The fix is architectural. Trusted shells never call domain mutators directly. They call verified flows. So the chain looks like this: Solana runtime ↓ trusted instruction shell ↓ verified flow ↓ verified domain operation Every constructor and mutator therefore executes below the verification boundary. When create_event calls Event::new, Creusot proves the constructor’s preconditions. When purchase calls record_sale, Creusot proves the event invariant first. The shell still has to establish the flow’s inputs. That part depends on the runtime and the data layer from Part 2. Program state enters through ownership checks, PDA validation, checked parsing, and one controlled mutable-account path. Solana contributes something unusually useful here: a program-owned account can only be written by that program. So if creation establishes the invariant, and every verified mutation proves that it preserves the invariant, then every future state written by the program is valid. Creation is the base case; verified mutation is the induction step. That is why the verified core does not need to re-check the same semantic invariant on every read. The chain enforces who is allowed to write, so once every writer is proved, every reader inherits the result. 9. The trusted computing base. “Formally verified” sounds absolute, but it isn’t. Every proof rests on assumptions, and the engineering job is to make those assumptions small enough to read. In this repository, the trusted computing base has three parts. The first is the instruction shells. They are marked #[trusted], exercised by twenty-two Mollusk tests, and reviewed manually. But manual review now has a much narrower definition. For each shell, I need to check: Did it load state through the validated path? Did it establish the verified core’s preconditions? Did it pass signer-checked addresses? Did it persist exactly what the core returned? That’s much easier than reviewing the arithmetic inside the decision logic as well. The second part is a small set of trusted axioms for foreign types Creusot doesn’t fully model. For example: #[cfg_attr(creusot, trusted)] #[cfg_attr( creusot, ensures((result == None) == (self.int() * other.int() > u64::MAX@)) )] #[cfg_attr( creusot, ensures( forall result == Some(r) ==> r.int() == self.int() * other.int() ) )] fn ax_checked_mul( self, other: NonZeroU64, ) -> Option { self.checked_mul(other) } The implementation is one line. The assumption says what that one line means mathematically. There are five wrappers around NonZeroU64, two around Address, and two around wire constructors. Auditing all of them is roughly forty lines. The third part of the trusted computing base is Creusot, Why3, and the SMT solvers themselves. Everything above that boundary is checked. 10. Running it should be boring. The verification toolchain lives in its own pinned Docker image from Part 1: Rust nightly, Creusot, Why3, and the solver portfolio. There are two commands I use: verify: check-transitions tooling::build-creusot MISE_ENV=creusot ./scripts/docker/run-tooling.sh \ {{ creusot_tooling_image }} cargo creusot replay: check-transitions tooling::build-creusot MISE_ENV=creusot ./scripts/docker/run-tooling.sh \ {{ creusot_tooling_image }} cargo creusot --replay verify translates the program into Why3 verification conditions and asks the solver portfolio to discharge them. Each solved condition produces a small proof.json under verif/. Those files are committed next to the code. So the proof state is versioned too. The tree looks roughly like this: verif/ticketing_program_rlib/ ├── domain/address/... ├── domain/event/... ├── domain/nonzero/... ├── domain/ticket/... └── flows/ ├── event_create/... ├── ticket_buy/... └── event_close/... replay checks the recorded sessions again without searching for a new proof. That is what the pre-push hook and CI run. Change a contract or an implementation and either the recorded proof still holds, or the push fails. That’s the workflow. Not “remember to run formal verification before release.” Push. Fail. Fix. 11. Formal verification without the heroic-project price tag. Formal verification has a reputation for being impractical for normal software, and that reputation did not appear from nowhere. The famous reference points are projects like seL4: years of specialist effort, proof artifacts many times larger than the implementation, interactive theorem proving, and a language where mutable aliasing makes reasoning expensive. That is not what I’m doing here. I verify a small pure core, not the entire Solana runtime. Rust’s ownership model eliminates much of the aliasing problem before the prover starts, most contracts discharge automatically through SMT solvers, and the proof sessions replay mechanically in CI. AI also changes the economics of this workflow. It is quite good at the repetitive part: writing Pearlite, reading failed verification conditions, adjusting the implementation, and trying again. The part I keep for myself is smaller and more important: I review the contract. For this program, the verified surface currently produces: 23 proof files. 112 solver goals. Of those, 96 discharge with Alt-Ergo, 13 with Z3, and 3 with cvc5. From warm caches, a full verification run stays well under a minute. Replay takes seconds. For a program this size, the proof tax is smaller than the cost of wondering whether an arithmetic edge case survived an AI refactor. 12. What changes when the author is an AI. This is the workflow the first two parts were building toward. When I add an instruction now, the order is simple: spec first, code second, proof as review. I define — or carefully review — the contract first: what must stay invariant, what may change, what must never change, what success means exactly, and which error conditions are allowed. Then the agent writes the implementation, shell, and tests, and Creusot checks whether the code actually satisfies those claims. If it doesn’t, the failed verification condition tells us exactly where the contract and implementation disagree, and the agent iterates against that. This changes code review in a useful way. I read the trusted shells carefully and the specifications even more carefully, but I spend less time manually simulating arithmetic inside verified bodies. Not because I trust the AI, but because I don’t have to: the theorem prover has already checked the part humans are especially bad at checking exhaustively. There is one caveat I don’t want to hide. A verified program is not necessarily a correct program; it is a program that matches its specification. Write the wrong specification and the prover will prove the wrong behavior with extraordinary rigor. That is why the specification is where human judgment lives. Fortunately, specs are much smaller than implementations. They are declarative, easy to diff, and describe exactly what I actually care about: what the program is allowed to do. That asymmetry is the whole point — the human owns the contract, the AI writes the implementation, and the prover sits between them. 13. The Whole Picture The repository now has three independent rails. The environment, from Part 1, gives me pinned toolchains, hermetic builds, one command surface, an explicit agent contract, and versioned knowledge. The interface, from Part 2, validates bytes in place, locks layouts at compile time, checks canonical PDAs during account loading, and generates clients from one source of truth. The logic, in this part, keeps the trusted shell small and puts the decision core behind contracts that are replayed on every push. None of those systems depends on the AI being careful. That is the point. Wrong bytes fail parsing, wrong layouts fail compilation, wrong client schemas fail parity tests, and wrong arithmetic fails a proof. If a change crosses the small boundary the prover cannot see, it lands in code I have deliberately kept short enough for a human to review. I don’t think safe AI-assisted development means asking an AI to write less code. It means building a system that does not particularly care who wrote it. For software controlling money on a public chain, that is the standard I want. The complete companion repository, including the formally verified ticketing program used throughout this series: https://github.com/kalaninja/pinocchio-workshop Part 1: The Environment. Part 2: Data Bugs Are the Bugs. ← Previous The Safest Solana Parser Is the One That Refuses Bad Bytes About Author byAlexander Kalankhodzhaev|@kalaninja Core Engineer Lead at Raiku Read my storiesAbout @kalaninja TOPICS ai-and-ml #solana#rust#ai#smart-contracts#security#creusot#verification#ai-solana