Formal Verification
On this page
Formal verification here means a machine-checked proof that a property holds for every input in a stated domain, not for a sample of inputs. Three methods are used, each suited to a different kind of property. Every claim on this page is marked as a fact (a result recorded in the repository) or an estimate.
fact The raw outputs of the runs described below are committed under audit/static-analysis/ with dated file names (halmos-2026-10-01.txt, integer-proofs-2026-10-01.txt, smtchecker-2026-10-01.txt) and the harnesses live under contracts/test/formal/ and contracts/test/halmos/. The sources verified are the version 1.0 review sources deployed as testnet deployment 12.
Methods
| Method | What it proves | Where it applies |
|---|---|---|
| Symbolic execution of Foundry harnesses | A check_ function with symbolic arguments cannot reach a failing assert on any path, under its vm.assume preconditions, against the real compiled contracts | State-machine gates, access control, parameter bounds, conservation under transfers, oracle round selection |
| Compiler model checker | Each assert in a pure-maths harness is proved safe by the compiler's built-in model checker (constrained Horn clauses) | Rounding, bounds and monotonicity of the arithmetic libraries |
| Integer proofs | The same arithmetic statements over the unbounded integers, with division modelled by its Euclidean witness; each property is checked to be non-vacuous before its negation is shown unsatisfiable | Credit arithmetic (LegWrap, LegOracle), FixedPointMath, WeekMath |
The symbolic engine executes EVM bytecode, so a proof covers the deployed logic including compiler behaviour. Its limit is non-linear 256-bit arithmetic: a property whose path condition contains a multiplication or division by a symbolic operand often exhausts the solver budget without a verdict. Such a property is reported as “not proved within budget”, never as proved; where it is a pure arithmetic statement, the integer route carries the universal claim instead.
Results: Symbolic Execution
fact Run of 1 and 2 October 2026: 12 harness contracts, 73 check_ properties. 34 are proved; 1 returned no verdict within the per-assertion solver budget; 38 did not finish inside the per-suite wall-clock cap (10 or 15 minutes). The caps are a budget, not a result: an unfinished property is open, and is covered by the fuzz and invariant suites listed in Testing methodology until a later run with a larger budget closes it.
Proved
| Harness | Property | Statement |
|---|---|---|
OracleAdapterFormal | check_selected_round_in_window | Whenever readAt returns a price it is the answer of the last round stamped at or before the close and within maxPreCloseLag of it; otherwise it reports no price |
OracleAdapterFormal | check_observe_pins_in_window_round | A round stamped after the close is never observed, whenever observe is called; the pinned price is the closing print and later feed history cannot change it |
OracleAdapterFormal | check_observe_rejected_before_grace | observe is rejected at every timestamp up to and including closeTs + closeGrace |
OracleAdapterFormal | check_force_path_delays | A forced observation cannot be proposed before the deferral window has elapsed nor executed before the force delay has elapsed; revoking returns the observation to deferred with no price |
OracleAdapterFormal | check_resolved_is_immutable | Once an observation is pinned, neither a forced price nor a cancellation can alter it |
OracleAdapterFormal | check_setParams_bounded, check_setCloseWindow_bounded, check_setters_cross_constraint | Every parameter setter rejects exactly the values outside its documented bounds, including the cross-constraints between them |
NoteCoreLifecycleFormal | check_no_strike_before_close, check_no_observe_before_close | Neither strike nor observation can be recorded before the official close they refer to |
NoteCoreLifecycleFormal | check_observe_transition, check_observe_idempotent_per_index, check_final_observation_matures | From Live, one resolved observation at any price leads to Live, Autocalled or Matured with nextObs advanced by exactly one; an index is never processed twice; the last observation always matures and breached is exactly the barrier predicate |
NoteCoreLifecycleFormal | check_price_bound_to_selected_round | The settlement price is the last round published at or before the close; a round published after the close, even inside the grace, never reaches the series |
NoteLegsFormal | check_supply_equals_outstanding, check_transfer_conserves, check_batch_transfer_conserves | After any mint, burn and transfer sequence the per-id supply equals the holders' outstanding units and the aggregate supply equals the sum over ids; single and batch transfers conserve balances |
NoteLegsFormal | check_only_core_mints_burns, check_approval_unusable_after_revocation, check_approval_not_transitive | Only the core mints or burns legs; approvals end on revocation and do not chain |
DeskGatesFormal | check_entry_closed_off_session, check_entry_closed_while_core_paused_or_unwinding | No Desk entry off session (so no share is priced on a stale mark), from the guardian pause onwards, or while an unwind proposal is pending |
AuctionRoundFormal | check_no_supply_no_price | Zero circulating supply means no floor and no price |
StakingVestingFormal | check_cooldown_not_shortenable, check_cooldown_setter_bounded | No sequence of requests, cancellations and deposits unlocks a staking exit before t0 + cooldown, open requests stay within their cap with shares escrowed, and the cooldown setter respects its bounds |
EmissionScheduleFormal | check_emission_bounded, check_emission_matches_closed_form, check_emission_non_increasing | Over the first six decay periods the weekly emission is zero before the start, lies in [floor, initial], equals the closed-form curve exactly, and never rises |
EmissionScheduleFormal | check_setSchedule_rejects_invalid, check_setSchedule_floor_edges, check_only_owner_sets | setSchedule accepts exactly the valid parameter sets and only from the owner |
EmissionScheduleFormal | check_change_applies_next_week, check_same_week_replaces | A schedule change applies from the following week, leaves the current week unchanged, and two changes in one week collapse into one checkpoint |
MarketCalendarFormal | check_civil_round_trip | For every day index from 2026-01-01 to 2099-12-31, the civil date is well formed and converts back to the same day index |
Not Proved Within Budget
| Harness | Properties | Why open | Covered meanwhile by |
|---|---|---|---|
DeskGatesFormal | check_exits_closed_inside_open_grace (no verdict), check_exits_closed_while_market_closed | Path condition includes the calendar's daylight-saving arithmetic | Desk gate unit and fuzz suites |
AuctionRoundFormal | check_round_opens_at_floor, check_param_change_resets_to_floor, check_params_bounded | Price curve multiplication by symbolic elapsed time | Auction fuzz suite, invariant suite |
EscrowConservationFormal | check_conservation_small_domain | Full series lifecycle with symbolic notional | Escrow invariants C1 to C3 (invariant suite), differential vectors |
GuardianFundsFormal | three properties | Symbolic calldata over every guardian entry point | Guardian unit suite, access-control fuzz |
DeskFormal | five ERC-4626 round-trip properties | mulDiv with symbolic numerators | Desk fuzz and invariant suites |
StakingVestingFormal | four share-price and vesting properties | mulDiv share pricing | sNOTE and vesting fuzz suites |
NoteCoreLifecycleFormal | check_subscription_transitions, check_strike_result, three terminal-status properties | Long symbolic paths through strike and settlement | Lifecycle unit suite, invariant C7 |
VeGaugeGovernanceFormal | seven voting-power and governance properties | The governance fixture is rebuilt inside every property (the deployment branches on the block time, which the engine rejects in setUp); no property finished in 15 minutes | Governance unit and fuzz suites |
MarketCalendarFormal | nine session, holiday, early-close and close-walk properties | Daylight-saving arithmetic per day index over a 74-year domain | Calendar fuzz suite and pinned transition dates |
open These properties remain unproved in the reported run. A resource limit is not a proof result, and the absence of a reported counterexample does not establish correctness.
Results: Integer Proofs
fact All 14 arithmetic properties are proved over the integers (longest 20 seconds):
| Library | Properties |
|---|---|
LegWrap | Wrap never lowers the pool per share; unwrap never lowers the pool per share; a wrap followed by an unwrap never profits; buy-in and payout fit in 256 bits for pools and units below 2^128 |
LegOracle | Price is at least the mark, monotone in the pool, scale invariant, with bounded carry, and does not overflow for factors up to 1e18 and pools and supplies below 2^128 |
FixedPointMath | mulDivUp dominates mulDiv by at most one and equals it exactly when divisible; bpsOf never exceeds its base; clamp stays in bounds |
WeekMath | roundWeek is week aligned, at most the input and within one week of it |
Results: Compiler Model Checker
fact The harness contracts/test/formal/smt/MathProperties.smt.sol states 40 assertions over FixedPointMath, WeekMath, ExpMath and DateTimeLib. On the 2 October 2026 run the model checker returned no verdict: with division slack variables disabled every query failed to invoke the solver, and without that option the analysis exhausted the available memory (5 GB cap) even when restricted to the 26 FixedPointMath and WeekMath obligations, while a one-line control contract proves in under a second. The committed output records each attempt. The FixedPointMath and WeekMath statements are therefore carried by the integer proofs above; the ExpMath and DateTimeLib statements by the symbolic round-trip proof, the differential vectors and the fuzz suites.
illustrative The 512-bit intermediate in Math.mulDiv (inline assembly) is the likely cause of the memory growth. A run on a larger machine, or one obligation per compilation, is the planned next step for this route.
Accrue
The Accrue contracts (src/accrue/: the registry, the hook and the shelf, with the QuoteMath library) have their own harnesses under test/formal/ and their own integer proofs. Raw outputs: audit/static-analysis/halmos-accrue-2026-10-09.txt and integer-proofs-accrue-2026-10-09.txt.
Symbolic Execution
fact Run of 9 October 2026, one property per process, 420 s wall clock each: 31 distinct properties over three harnesses (AccrueMathFormal, AccrueShelfFormal, AccrueShelfCashFormal, the last one running the shelf properties with cash on the book). 12 are proved, 19 returned no verdict, none produced a counterexample. Every property has a concrete twin in AccrueShelfFormalReach and AccrueShelfCashFormalReach (16 unit tests, all passing), so a property that only held because every path reverted would be caught.
Proved
| Harness | Property | Statement |
|---|---|---|
AccrueShelfFormal | check_only_hook_fills | fillBuy, fillSell and payOut revert for every caller but the hook, whatever the arguments |
AccrueShelfFormal | check_only_registry_configures | Parameters, pause, posted feed and venue revert for every caller but the registry |
AccrueShelfFormal | check_settle_self_is_self_only | The best-effort settlement entry refuses every caller but the shelf itself |
AccrueShelfFormal | check_registry_owner_only | Registry governance is the owner's alone; the guardian may only pause and unpark; ownership cannot be renounced |
AccrueShelfFormal | check_hook_surface | The hook answers the pool manager only, refuses liquidity and donations, and registers pools for the registry only |
AccrueShelfFormal | check_hook_initialise_registered_only | A pool the registry did not register cannot be initialised through the hook; a registered one cannot be initialised by anyone but the registry |
AccrueShelfFormal | check_params_bounds_exact | setShelfParams accepts a parameter set exactly when every field sits inside its documented bound (363 paths) |
AccrueShelfFormal | check_pause_closes_quotes | A paused registry or shelf closes fills and deposits for every amount; a paused shelf never blocks the in-kind exit of a position already held |
AccrueShelfFormal | check_weekend_closes_entries | Outside the 24/5 window deposits and the stock-only exit are closed; the in-kind exit stays open |
AccrueShelfFormal | check_collect_fees_to_treasury | Fees leave the shelf only through collectFees, go to the registry's treasury in full, and the book is untouched |
AccrueMathFormal | check_bid_refuses_full_spread | A half spread of 10,000 bp or more is refused, so a bid is never zero |
AccrueMathFormal | check_half_spread_floor_and_shift | One side's half spread is the base shifted by the skew, never below the floor, plus the age and size terms |
Not Proved Within Budget
| Harness | Properties | Why open | Covered meanwhile by |
|---|---|---|---|
AccrueMathFormal | ten arithmetic properties (bracket, monotonicity, saturation, skew, cash share, rounding on both sides, round trip, conversion, pool price) | mulDiv with symbolic operands | The integer proofs below, one for one |
AccrueShelfFormal | check_first_deposit_fee_exact, check_round_trip_never_profits, check_in_kind_exit_bounded | Deposit and exit paths through mulDiv; the solver's query files exceeded the disk of the review machine | Integer proofs first_deposit_is_linear, fee_on_total_bounded, deposit_then_redeem_never_profits, in_kind_split_never_exceeds_book; fuzz and invariant suites |
AccrueShelfFormal | check_no_reference_no_quote, check_same_block_exit_refused | Same paths before the gate | Unit suites (ShelfHardening, ShelfValuation), concrete twins, fork end-to-end run |
AccrueShelfCashFormal | check_entry_values_cash_at_bid, check_exit_values_cash_at_ask, check_round_trip_with_cash_never_profits, check_fill_matches_preview, and the two inherited exit properties | Valuation of the cash leg through mulDiv | Integer proofs entry_at_bid_never_mints_more_than_at_reference, exit_at_ask_never_pays_more_than_at_reference, deposit_at_bid_then_redeem_at_ask_never_profits; unit suites; concrete twins |
open These properties remain unproved in the reported run. A resource limit is not a proof result, and the absence of a reported counterexample does not establish correctness.
Integer Proofs
fact test/halmos/smt/accrue_math_proofs.py: 29 of 29 properties proved over the integers (longest 29 s), each checked non-vacuous first. Domains: prices to 1e14 (8 decimals), stock to 1e27 units, USDG to 1e18, half spreads to 900 bp; results_fit_uint256 proves every intermediate fits in 256 bits under these bounds.
| Group | Properties |
|---|---|
| Spread and price | Ask and bid bracket the reference by the half spread rounded against the trader; bid positive from one cent; zero spread is the identity; monotone in the spread; spread width exact; the valuation half spread brackets the tier base |
| Fill rounding and round trips | Rounding never favours the trader on either side; exact-in and exact-out round trips never pay the trader; conversion round trip never creates USDG; a fill never lowers the book; an exact-output sell delivers at least the reference size |
| Spread terms | Cash share is a fraction; the linear term is bounded and monotone; the skew is bounded |
| Fees, shares and valuations | Fee on total bounded; fee on the raw amount covers it; a deposit then an exit never profits (with and without cash, at bid and ask); shares never dilute existing holders; the first deposit is linear; the in-kind split never exceeds the book |
| Pool price | The pool price stays inside the pool's bounds in both token orders |
Static Analysis
Slither and forge lint results for the Accrue contracts are on the static analysis page.
Not Covered by Any Proof
fact No universal proof exists yet for Treasury reserve accounting, BondDepository, RollPolicy and NoteAutomation calendar bounds, PythProFeed payload parsing, Minter, the vault layer (NoteVault, NoteVaultMandate, NoteCoreAdapter, NoteVaultFactory) and the omnichain contracts (LegVault, LegMirror). These are covered by unit, fuzz and invariant suites and by the live testnet rounds described in Testing methodology. The vault layer binds each vault to its mandate and adapter through a predicted deployment address; the symbolic engine allocates addresses differently from the chain, so a symbolic fixture for the vault needs a dedicated construction path and is planned rather than done.
How to Reproduce
cd contracts
# symbolic execution, one harness at a time
FOUNDRY_DYNAMIC_TEST_LINKING=false halmos --contract OracleAdapterFormal --root . \
--solver-threads 1 --solver-timeout-assertion 60000 --solver-timeout-branching 1000
# integer proofs
python3 test/halmos/smt/credit_math_proofs.py
# compiler model checker
scripts/smtcheck.sh /path/to/solc-0.8.28 10000Properties are added as check_ functions next to the contract they describe. A property that only holds on a bounded domain states the domain in its vm.assume preconditions and in its comment; the domain is part of the claim.
Keep exploring, or revisit this topic from the navigation.