List view
* Enhance usability and performance of the formal verification framework based on early adopter feedback. * Provide ongoing maintenance of the symbolic execution and proof construction frameworks for 1 year. * Publish updates and technical reports to highlight new use cases and improvements. * Continue supporting developers with documentation updates and bug fixes. * Investigate deeper verification of memory handling challenges encountered in Solana smart contracts.
Due by June 19, 2026* Publish documentation, technical blogs, and demo videos to support developer onboarding * Work with Solana teams to refine developer tooling and improve integration with the ecosystem * Onboard minimum 2 ecosystem teams to use the tool * Technical talk at Solana Accelerate: Scale or Die
Overdue by 1 month(s)•Due by June 19, 2025* Work with the Anza core developer team and the Solana Foundation to formally verify SPL stake program * Best effort verification of the stake token program by Solana Accelerate: Scale or Die
Overdue by 2 month(s)•Due by May 22, 2025* Collaborate with the Anza team to verify critical security properties of the P-Token contract, including: - Token minting - Burning - Transfer mechanisms * Address technical blockers identified in our analysis: - Update Rust version for compatibility with our serialization code. - Ensure compatibility with stable-mir-json output from their repositories. - Handle unsafe code in state/mod.rs (4 instances) and processor/mod.rs (complex nested loops + unsafe). - Investigate Pinocchio dependency footprint and selectively verify its used portions. * Improve the sol-semantics library and symbolic execution engine based on insights from this verification effort.
Overdue by 3 month(s)•Due by May 1, 2025* Instantiate our symbolic execution engine to the Solana semantics, to enable verification. * Build the `kompass` property-based testing formal verification/proof construction framework for Rust Solana smart contracts. * Conduct best-effort verification of a P-Token Solana program for demonstration at the Solana Developer Conference (May 2025). * Address memory modeling challenges in kmir, ensuring robust handling of program memory and execution traces.
Overdue by 3 month(s)•Due by April 11, 2025