{"words":"each C kernel's verdict from Aristotle's own CI, failing on any property left without a verdict; the sha256 of every file the run read, and that file served verbatim at its url, so it can be hashed and compared; and Aristotle's own report. a verdict stands only while every file still hashes the same.","kernels":[{"backend":"aristotle","tool":"aristotle-ci","toolVersion":"3.0.0","desk":"poiesis","kernel":"agent/instruments/instruments.c","properties":[{"id":"muldiv_no_ub","status":"verified","words":"the multiply-divide is memory safe on every input: no out-of-range shift, no division by zero, no overflow, and nothing written but its output"},{"id":"quote_no_ub","status":"verified","words":"the quote is memory safe on every input and writes nothing but its output"},{"id":"payoff_no_ub","status":"verified","words":"the payoff is memory safe on every input and writes nothing but its output"},{"id":"muldiv_exact","status":"verified","words":"the multiply-divide is exact, floor(a·b/d) with no intermediate overflow"},{"id":"quote_fee_conservation","status":"verified","words":"the operations fee plus the writer's premium equals the premium paid, exactly"},{"id":"spread_payoff_conservation","status":"verified","words":"the buyer's payout plus the writer's residual equals the collateral, exactly, and the payout never exceeds it"},{"id":"invalid_terms_no_write","status":"verified","words":"invalid terms are refused and nothing is written"}],"verified":7,"total":7,"files":{"agent/instruments/instruments.c":{"sha256":"47779578d3b6f6d88db622664061cfd218c3c2d0c34a8b2febbff5c5ca1ccf66","url":"/api/code-proofs/file/agent/instruments/instruments.c"},"agent/instruments/instruments.h":{"sha256":"2fbb1710ee0aadd27edaebe53514169054f2c39addfc21bd95eada8f6236556c","url":"/api/code-proofs/file/agent/instruments/instruments.h"},"agent/instruments/aristotle.toml":{"sha256":"535deeaf24f5a4067dfac92abfe22b4cfb4a4bdf375e45f7a26fd5ee1a83dc66","url":"/api/code-proofs/file/agent/instruments/aristotle.toml"},"agent/bank/proofs/Poiesis.lean":{"sha256":"33fbd5250086156f087fd843f5cc5e17dae6345df6e31620ed371891a4d9991c","url":"/api/code-proofs/file/agent/bank/proofs/Poiesis.lean"}},"checkedAt":"2026-10-28T05:01:37.302Z","projectUrl":"https://aristotle.harmonic.fun/projects/e9dfa7e8-4a4f-4ba9-8fd6-2262a08a1e55","report":"/api/code-proofs/poiesis/report.xml","current":true,"why":null},{"backend":"aristotle","tool":"aristotle-project","toolVersion":"3.0.0","desk":"stocks","kernel":"agent/kernels/stocks/stocks.c","properties":[{"id":"rail_admit_no_ub","status":"verified","words":"the audited rail's check is memory safe on every input and writes nothing"},{"id":"rail_admit_exact","status":"verified","words":"the audited rail forwards an order exactly when the stock is not halted, the symbol is allowed, the order is priced, it is within the order cap, the day's orders plus this one are within the day cap counted in whole cents, and the gap since the last order has passed; otherwise it names the first rule that failed"},{"id":"rail_admit_limits_hold","status":"verified","words":"an unpriced order is never forwarded and a halted holder forwards nothing; loosening a limit never refuses an order that passed; and two orders admitted in turn never together exceed the day cap"},{"id":"oracle_needs_write_no_ub","status":"verified","words":"the equity oracle writer's rewrite check is memory safe on every input and writes nothing"},{"id":"oracle_moved_exact","status":"verified","words":"whether a price moved is decided exactly, in whole numbers, with no overflow"},{"id":"oracle_rewrite_only_when_moved","status":"verified","words":"an oracle row is rewritten only when it moved or its heartbeat is due: a free row only when its verdict changes, a paid row when its verdict, basis, time, pool or price moved past its threshold"},{"id":"oracle_cycle_bounded","status":"verified","words":"one cycle sends at most four transactions of at most twenty five rows each, in order and without overlap, and nothing after a failed send"},{"id":"print_allowance_no_ub","status":"verified","words":"the print allowance is memory safe on every input and writes nothing but its output"},{"id":"print_allowance_bounds","status":"verified","words":"a stock print may stand between fifteen and thirty minutes: fifteen until twenty four gaps between its prints are on record, then the ninetieth percentile of its last forty eight, held inside those bounds"},{"id":"quote_verdict_stale","status":"verified","words":"a quote in an open session reads stale exactly when it is older than its allowance, and never reads open without a price, with a halt flag that is not down, while paused, undated, or in the weekend hold"},{"id":"halt_due_exact","status":"verified","words":"the risk feed lands a halt exactly when the issuer's feed says halted on a written token that is not already halted, dated no later than now"},{"id":"halt_apply_no_ub","status":"verified","words":"the risk feed's update of a halt record is memory safe on every input"},{"id":"halt_start_never_moves","status":"verified","words":"the start of a halt never moves while it lasts, and a halt lifts only on a whole write made on a dated quote whose halt flag reads down"},{"id":"mark_never_pool_price","status":"verified","words":"the risk feed's mark is the issuer's print while the market is open, the weekend mark or the last open print while it is shut, or none, and never the pool's price whatever the pool says; the contract's own check always takes it"}],"verified":14,"total":14,"files":{"agent/kernels/stocks/stocks.c":{"sha256":"4b8e20db8bf44673bba60bddfac4f7f55258c132a80ab26de9a3db0888b78cf7","url":"/api/code-proofs/file/agent/kernels/stocks/stocks.c"},"agent/kernels/stocks/stocks.h":{"sha256":"ffb357aa0a674970223d454995ed4f3a07bf64f4d04e5476c9e024ed23858c33","url":"/api/code-proofs/file/agent/kernels/stocks/stocks.h"},"agent/kernels/stocks/aristotle.toml":{"sha256":"81cdb80cd7093d112560a42369b45184379611be2a72322f4bff203a48005049","url":"/api/code-proofs/file/agent/kernels/stocks/aristotle.toml"}},"checkedAt":"2026-11-01T05:36:29.242Z","projectUrl":"https://aristotle.harmonic.fun/projects/aa6d37f2-558c-42cf-adc5-e48a4b698b7d","report":"/api/code-proofs/stocks/report.json","current":true,"why":null}],"deciding":{"stocks":{"running":true,"sourceHash":"0033b325261d462e77c42aa8c95a7bca6017865fb5c9d50b2584259efe089378","decisions":{"kernel":144779,"javascript":0,"disagreements":0,"lastDisagreement":null}}}}