Expand formal coverage and resilience brief

Author: Your Name

README.md

@@ -35,6 +35,7 @@
   <a href="docs/INVESTOR_ONE_PAGER.md">Investor One-Pager</a> •
   <a href="docs/ASSURANCE.md">Assurance Packet</a> •
   <a href="docs/FORMAL_VERIFICATION.md">Formal Verification</a> •
+  <a href="docs/RESILIENCE_BRIEF.md">Resilience Brief</a> •
   <a href="docs/CHAOS_ENGINEERING.md">Chaos Engineering</a> •
   <a href="docs/PANCAKECALL_AUDIT.md">Callback Audit</a> •
   <a href="docs/RELEASE_NOTES.md">Release Notes</a> •
@@ -336,7 +337,7 @@ python scripts/backtest.py --days 90 --tvl 100000 --cycles-per-day 4 --gas-gwei
 
 Latest local validation: `54/54` tests passing.
 
-Formal verification: `9/9` symbolic properties passing via `python scripts/run_formal.py`.
+Formal verification: `10/10` symbolic properties passing via `python scripts/run_formal.py`.
 
 Invariant tests:
 

docs/ASSURANCE.md

@@ -43,7 +43,7 @@ Faster investor diligence
 | Economic framing | formulas and caveats are explicit | `ECONOMICS.md` |
 | Regression tests | main contract behavior stays intact | `forge test` |
 | Invariants | key capital-safety properties hold across randomized sequences | `test/Invariant.t.sol` |
-| Formal verification | nine core internal properties hold under symbolic execution | `test/FormalEngineVault.t.sol` |
+| Formal verification | ten core internal properties hold under symbolic execution | `test/FormalEngineVault.t.sol` |
 | Adversarial tests | bad dependencies end in safe revert or safe degradation | `test/AssuranceAdversarial.t.sol` |
 | Static analysis | flash callback and external-call hotspots stay visible | `docs/SLITHER_NOTES.md` |
 | Manual audit focus | remaining callback hotspot has a written human review | `docs/PANCAKECALL_AUDIT.md` |

docs/FORMAL_VERIFICATION.md

@@ -4,7 +4,7 @@
 
 This repo now includes an actual symbolic-proof layer using `halmos`, not just conventional tests.
 
-Current local result: `9/9` symbolic properties passing via `python scripts/run_formal.py`.
+Current local result: `10/10` symbolic properties passing via `python scripts/run_formal.py`.
 
 The goal is not to claim that the entire strategy and all external markets are mathematically proven.
 
@@ -23,7 +23,8 @@ Formal targets
 ├─ ONLY_UNWIND blocks fresh exposure
 ├─ ONLY_UNWIND recovers after two safe cycles
 ├─ flash borrowed base caps at zero when underwater
-└─ deposits pause when risk mode is `ONLY_UNWIND`
+├─ deposits pause when risk mode is `ONLY_UNWIND`
+└─ zero borrowed-base context preserves totalAssets
 ```
 
 These properties are implemented in `test/FormalEngineVault.t.sol` and run by `scripts/run_formal.py`.

docs/INVESTOR_ONE_PAGER.md

@@ -47,7 +47,7 @@ It is presented as a strategy system with a growing assurance stack:
 
 - `54/54` contract tests passing locally.
 - `5/5` invariant checks passing.
-- `9/9` symbolic formal properties passing via Halmos.
+- `10/10` symbolic formal properties passing via Halmos.
 - adversarial tests covering dependency and unwind edge cases.
 - Slither reduced to `1` remaining finding family focused on flash-callback event ordering.
 

docs/RELEASE_NOTES.md

@@ -16,7 +16,7 @@ Self-Driving Yield Engine now ships with a stronger investor-proof story: a dedi
 ## Highlights
 
 - Added an investor-facing `docs/ASSURANCE.md` that links research, tests, static analysis, and fork checks into one proof index.
-- Added an actual Halmos-based formal layer proving nine core internal properties.
+- Added an actual Halmos-based formal layer proving ten core internal properties.
 - Expanded machine-checked invariants around asset conservation, flash-borrow cleanup, and no-profit/no-bounty behavior.
 - Added adversarial tests for `ONLY_UNWIND`, blocked hedge closes, and ALP cooldown-constrained unwinds.
 - Added minimal GitHub Actions CI for `forge build/test`, invariant runs, research script checks, scenario backtests, and Slither.
@@ -42,7 +42,7 @@ This release makes the project easier to diligence:
 
 - `forge test` → `54/54 PASS`
 - `forge test --match-path test/Invariant.t.sol` → `5/5 PASS`
-- `python scripts/run_formal.py` → `9/9 PASS`
+- `python scripts/run_formal.py` → `10/10 PASS`
 - `python -m py_compile scripts/backtest.py` → `PASS`
 - `python scripts/backtest.py --days 90 --tvl 100000 --cycles-per-day 4 --gas-gwei 50 --compare-scenarios --json-out cache/backtest-report.json` → `PASS`
 - `slither . --exclude-dependencies --exclude incorrect-equality,timestamp,low-level-calls,naming-convention,cyclomatic-complexity` → `1 finding triaged`
@@ -86,7 +86,7 @@ This release makes the project easier to diligence:
 #### 2. Safety Coverage
 
 - Invariants now cover asset conservation, flash state cleanup, and zero bounty without profit.
-- Formal verification now covers nine symbolic properties around accounting, share math, price-guard behavior, `ONLY_UNWIND`, deposit pausing, and no-profit bounty behavior.
+- Formal verification now covers ten symbolic properties around accounting, share math, price-guard behavior, `ONLY_UNWIND`, deposit pausing, no-profit bounty behavior, and zero-borrow flash accounting consistency.
 - Added a dedicated manual review note for the remaining flash-callback hotspot in `docs/PANCAKECALL_AUDIT.md`.
 - Adversarial tests now prove safer behavior under dependency stress.
 
@@ -105,7 +105,7 @@ This release makes the project easier to diligence:
 
 - Solidity regression: `forge test` → `54/54 PASS`
 - Invariants: `forge test --match-path test/Invariant.t.sol` → `5/5 PASS`
-- Formal verification: `python scripts/run_formal.py` → `9/9 PASS`
+- Formal verification: `python scripts/run_formal.py` → `10/10 PASS`
 - Research script: `python -m py_compile scripts/backtest.py` → `PASS`
 - Scenario research run: `python scripts/backtest.py --days 90 --tvl 100000 --cycles-per-day 4 --gas-gwei 50 --compare-scenarios --json-out cache/backtest-report.json` → `PASS`
 - Static analysis: Slither run completed and triaged; only `pancakeCall()` event-order warnings remain

docs/RESILIENCE_BRIEF.md

@@ -0,0 +1,63 @@
+# Operational Resilience Brief
+
+## Main Point
+
+Self-Driving Yield Engine now has a clearer resilience story than a typical hackathon repo.
+
+It is no longer just “contracts + tests”.
+
+It is now:
+
+- CI-gated,
+- partially formally verified,
+- static-analysis triaged,
+- manually reviewed at the main callback hotspot,
+- and backed by nightly DeFi-adapted chaos experiments.
+
+
+## Current Evidence Stack
+
+```text
+Operational resilience
+├─ main CI green
+├─ nightly chaos green
+├─ formal 10/10
+├─ invariants 5/5
+├─ regression 54/54
+├─ one known Slither finding
+└─ callback manual review written down
+```
+
+
+## What This Means For Investors
+
+- The system is not being presented as “perfect” or “finished forever”.
+- The main remaining hotspot is visible and documented.
+- The validation stack now tests both correctness and failure behavior.
+
+
+## Current Status
+
+- Regression tests: `54/54`
+- Invariants: `5/5`
+- Formal properties: `10/10`
+- Slither: `1` known triaged finding
+- Main callback review: `docs/PANCAKECALL_AUDIT.md`
+- Nightly chaos workflow: `.github/workflows/nightly-chaos.yml`
+
+
+## Failure Modes We Now Exercise
+
+- oracle divergence
+- `ONLY_UNWIND` entry and recovery
+- blocked hedge close
+- ALP cooldown unwind limits
+- gas spike / bounded bounty
+- flash liquidity shortfall
+- degraded RPC timeout behavior
+
+
+## Remaining Honest Boundary
+
+- This is still not a claim that the full strategy and external markets are mathematically proven.
+- It is a claim that the repo now has a credible resilience process around the highest-risk internal and dependency-driven behaviors.

test/FormalEngineVault.t.sol

@@ -311,4 +311,13 @@ contract EngineVaultFormalTest is Test {
 
         assert(vault.totalAssetsExcludingBorrowedBase(borrowed) == 0);
     }
+
+    function check_totalAssetsExcludingZeroBorrowMatchesTotalAssets(uint16 baseBalance) public {
+        _assumeReasonableAmount(baseBalance);
+
+        (EngineVaultFormalHarness vault,, MockERC20 base) = _deployFlashAccountingVault();
+        base.mint(address(vault), baseBalance);
+
+        assert(vault.totalAssetsExcludingBorrowedBase(0) == vault.totalAssets());
+    }
 }