finance/options: fully collateralized options venue in Anchor v2, Anchor v1, and Quasar, with Kani proofs

.github/workflows/anchor.yml

@@ -300,6 +300,7 @@ jobs:
             case "$project" in
               ./basics/pyth/anchor \
               |./finance/betting-market/anchor \
+              |./finance/options/anchor \
               |./finance/order-book/anchor \
               |./finance/perpetual-futures/anchor \
               |./finance/prop-amm/anchor \

.github/workflows/kani.yml

@@ -61,6 +61,7 @@ jobs:
           - vault-strategy
           - token-fundraiser
           - prop-amm
+          - options
     steps:
       - uses: actions/checkout@v5
       - uses: dtolnay/rust-toolchain@stable
@@ -105,6 +106,7 @@ jobs:
           - vault-strategy
           - token-fundraiser
           - prop-amm
+          - options
     steps:
       - uses: actions/checkout@v5
       - name: Run Kani

CHANGELOG.md

@@ -4,6 +4,30 @@ All notable changes to this repository are documented here.
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
+## [2026-09-04] - Options venue example
+
+### Added
+
+- `finance/options`: a fully collateralized, physically settled options venue,
+  in Anchor v2, Anchor v1, and Quasar, with a Kani proof crate. A writer posts
+  the whole obligation (the underlying for a call, the strike in the quote token
+  for a put) and lists an option at a premium; a buyer pays the premium and becomes
+  the holder; the holder may exercise before expiry; after expiry the writer
+  reclaims the collateral. Eight instruction handlers (`initialize_market`,
+  `write_option`, `buy_option`, `cancel_option`, `exercise_option`,
+  `collect_proceeds`, `reclaim_collateral`, `collect_fees`). Every settlement
+  amount is a product of two of the option's integers, so there is no division and
+  no rounding in settlement; the venue's fee on each premium is the only floor.
+  The market account keeps a ledger of what each vault owes, asserted against
+  the vault balances after every transfer, and the proof crate walks every path
+  through an option's life and shows the ledger returns to zero. No oracle: physical
+  settlement moves the tokens themselves, so the program never has to know the
+  price. Each option is one account, bought and exercised as a whole.
+- The Anchor v2 copy joins the `--no-idl` list in `.github/workflows/anchor.yml`
+  (anchor#4947: its `OptionKind` and `OptionStatus` enums reach the IDL) and the
+  root Cargo workspace; the proof crate joins both matrices in
+  `.github/workflows/kani.yml`.
+
 ## [2026-08-21] - Anchor v1 kept alongside Anchor v2
 
 Anchor v1 is expected to stay on long-term support, and many deployed programs