ZenoFCIS 2.1 · Interactive case
Two-Key Release Desk
Two different approvers. One release intent.
Try the rules, including the actions that should fail. Each answer comes from a table recorded by the real ZenoFCIS Authority. This browser view is a local demonstration; it does not authenticate people or release anything.
One simulated request
Release authorization
- First key
- Waiting
- Second key
- Waiting
- Release intents
- 0
Loading the Authority decision table…
A rejection changes nothing. Cancellation closes the request without a release; the contract calls this a CommittedFailure. A new simulation starts a separate history.
Try an adversarial sequence
Action history · 0 attempts
Latest 40 actions shown.
Inspect the last recorded decision
Choose an action to inspect its recorded decision.
What runs here, and what was checked?
The Rust app was emitted by the pinned ZenoFCIS 2.1 development factory. Its native tests exercise the actual Authority and SQLite shell. This page uses 384 recorded Authority answers; its JavaScript and the export adapter are tested, not formally verified.
The finite model has 14 reachable states and 112 outgoing state/action/caller combinations. A separate Lean model proves preservation and at most one release intent for every finite history. The Lean model’s class, successor state, and release count also match all 384 Authority rows in an executable check; no Rust-to-Lean compiler is proved.
The selector supplies an ID. A deployed service would have to authenticate that ID, protect the database, and implement a durable idempotent destination. A hostile host can alter delivery acknowledgements or restore an old valid database. No real payment or network delivery happens here.