Split a payout
Enter an amount in dollars and three or more recipients, then run the same request on the buggy build and on the verified repair. Both builds are the Lean payout component compiled to the payout-sidecar executable.
Lean component: Payout.step
Status for the repaired build: VERIFIED. Its requirements are proved in Lean for all inputs and checked by Comparator.
Open the Passport 6c87fa0708a1 for formal/evidence/muse-repair-002/Solution.lean (sha256 f815f964e7041187).
TypeScript glue on this page
Status: TESTED_ONLY. Dollar parsing, cent formatting, request building and result summaries are not proved.
16,000 property-test cases across 14 properties with fast-check, all passing. Last run 2026-10-27T06:44:54.562Z.
The JSON wrapper inside the executable (app/Main.lean) is also TESTED_ONLY.
Payout request
Buggy build
Not run yet.
Repaired build
Not run yet.