Hi,
We wrote formal property tests for the pyth-solana-receiver program against the Apache-2.0 codebase and wired them into CI: https://github.com/caliperforge/cf-invariants-pyth
invariant_reclaim_rent_conservation: reclaim_rent can only transfer SOL to the write_authority and only up to the exact rent amount. The program's lamport balance must decrease by at most the reclaimed rent; any larger decrease fires the invariant. The planted twin (transferring to an attacker-controlled account) fails; the clean harness passes. We did not find an existing test for this instruction.
We also have invariant_two_step_governance, which verifies the RequestGovernanceAuthorityTransfer/AcceptGovernanceAuthorityTransfer two-step must both complete before authority changes hands. We saw your test_governance.rs already covers this flow; our invariant adds a Crucible-fuzzed layer over the same property if that is useful alongside what you have.
Both run on Crucible (Asymmetric Research) v0.2.0 with anchor-lang 1.0.1; CI-green (run 26986538814).
Happy to open a PR or adjust scope based on what is useful.
Authored with AI assistance. Michael Moffett / CaliperForge — michael@caliperforge.com
Hi,
We wrote formal property tests for the
pyth-solana-receiverprogram against the Apache-2.0 codebase and wired them into CI: https://github.com/caliperforge/cf-invariants-pythinvariant_reclaim_rent_conservation:reclaim_rentcan only transfer SOL to thewrite_authorityand only up to the exact rent amount. The program's lamport balance must decrease by at most the reclaimed rent; any larger decrease fires the invariant. The planted twin (transferring to an attacker-controlled account) fails; the clean harness passes. We did not find an existing test for this instruction.We also have
invariant_two_step_governance, which verifies theRequestGovernanceAuthorityTransfer/AcceptGovernanceAuthorityTransfertwo-step must both complete before authority changes hands. We saw yourtest_governance.rsalready covers this flow; our invariant adds a Crucible-fuzzed layer over the same property if that is useful alongside what you have.Both run on Crucible (Asymmetric Research) v0.2.0 with anchor-lang 1.0.1; CI-green (run 26986538814).
Happy to open a PR or adjust scope based on what is useful.
Authored with AI assistance. Michael Moffett / CaliperForge — michael@caliperforge.com