Add README comments re Solana hackathon and move 2 SVM demos to public repo

Author: Accelnorm

README.md

@@ -1,6 +1,31 @@
-# Certora AI Composer (Solidity + Solana/SVM Experimental)
+# Spec-driven AI Coder (Solidity + Solana/SVM Experimental)
 
-AI Composer is a tool for generating verified implementations from documentation and CVL specifications.
+Spec-driven AI Coder is an AI agent that codes more securely by generating verified implementations from documentation and specifications, with test-driven development (TDD) and formal verification (FV) support.
+
+# Scope Accomplished for Solana Student Hackathon - Fall 2025
+
+For this hackathon, I extended the original Certora AI Composer (which previously targeted only the EVM) with an experimental Solana/SVM pipeline. The expansions include:
+
+- SVM target selection.
+- Solana‑specific prompts and workflows.
+- Solana/CVLR (Certora Verification Language for Rust) RAG stack.
+- TDD-oriented development flow: the ability to run in a “tests‑first” mode where the Composer generates code guided by passing tests, with an explicit `--no-fv` option to skip formal verification early on and iterate quickly.
+- End‑to‑end SVM example: a trivial Rust project under `examples/svm/materialized_trivial_addition` [demonstrating the full loop](examples/svm/materialized_trivial_addition/terminal_logs_for_trivial_demo_with_formal_verification.txt) from natural language/system doc → Rust code → formal checks. 
+- [Vault program example](examples/svm/materialized_vault) done by TDD.
+
+Compared to the earlier EVM‑only prototype from Certora Labs, this fork now supports a second, Solana‑native verification path (Rust + certoraSolanaProver) with Solana‑specific prompts, RAG, and examples, while staying aligned with the original Composer architecture.
+
+# Next Steps for Solana Development
+My next steps would be to:
+- Test having the AI Composer implement the vault application in Certora/SolanaExamples with formal verification enabled
+- Translate [novel AMM](examples/cccp_fixed/system_doc.txt) spec to CVLR
+- Test having  the AI Composer implement the novel AMM for Solana
+- Test with an Anchor project and make any needed adjustments
+- Enable the agent to use the Solana MCP
+- Explore integration of Kani Rust Verifier before running the more specific Certora Solana Prover
+- Make more developer-friendly
+- Enable using a local LLM
+- Do AI coding workshops/bootcamps advocating for TDD and FV adoption
 
 # Installation
 
@@ -209,5 +234,7 @@ to the updated/refined spec file to use for the next iteration.
 
 # Disclaimer
 
-AI Composer is a research prototype released by Certora Labs. The code generated by AI Composer should **not** be
+AI Composer is a research prototype initially released by Certora Labs. This Solana extension is not affiliated to Certora Labs.
+
+The code generated by AI Composer should **not** be
 placed into production without thorough vetting/testing/auditing.

examples/svm/materialized_trivial_addition/.session-id

@@ -0,0 +1 @@
+crypto_session_2f8508c2-dc70-11f0-a4d3-1c697aaa77f7

examples/svm/trivial/Cargo.toml …materialized_trivial_addition/Cargo.tomlexamples/svm/trivial/Cargo.toml renamed to examples/svm/materialized_trivial_addition/Cargo.toml examples/svm/trivial/Cargo.toml renamed to examples/svm/materialized_trivial_addition/Cargo.toml

@@ -1,5 +1,5 @@
 [package]
-name = "svm_trivial"
+name = "simple-addition"
 version = "0.1.0"
 edition = "2021"
 
@@ -8,9 +8,10 @@ crate-type = ["cdylib"]
 
 [features]
 certora = []
+rt = []
 
 [dependencies]
-cvlr = { path = "../../../cvlr/cvlr" }
+cvlr = "0.4"
 
 [package.metadata.certora]
 sources = [

examples/svm/materialized_trivial_addition/certora/summaries/cvlr_inlining_core.txt

@@ -0,0 +1,196 @@
+; By default we do not inline core, std, alloc, and solana_program
+; with some exceptions below with #[inline]
+
+#[inline(never)] ^core::.*$
+#[inline(never)] ^std::.*$
+#[inline(never)] ^<?alloc::.*$
+#[inline(never)] ^solana_program::.*$
+
+; CVT functions
+#[inline(never)] ^([^:]+::)*CVT_.*$
+
+; Rust memory allocation functions 
+#[inline(never)] ^__rust_alloc$
+#[inline(never)] ^__rust_dealloc$
+#[inline(never)] ^__rust_alloc_zeroed$
+#[inline(never)] ^__rg_alloc$
+#[inline(never)] ^__rg_dealloc$
+#[inline(never)] ^__rg_oom$
+
+;; We want to inline wrappers that call the global allocator
+#[inline] ^alloc::alloc::exchange_malloc$
+;;;#[inline] ^alloc::fmt::format::format_inner$
+
+; memcpy/memmove/memset/memcmp
+; These functions are wrappers to sol_memcpy_, sol_memmove_,
+; sol_memset_, and sol_memcmp_.  These wrappers ensure that sol_*
+; preconditions are satisfied when these functions are called
+; (alignment conditions, non-nullity, etc). Since, we are not interested in
+; verifying the code of the wrappers, we don't inline calls to
+; memcpy, memmove, memset, and memcmp so that we can replace them
+; directly with sol_memcpy_, sol_memmove_, sol_memset_, and
+; sol_memcmp_, respectively.
+#[inline(never)] ^memcpy$
+#[inline(never)] ^memmove$
+#[inline(never)] ^memset$
+#[inline(never)] ^memcmp$
+
+
+; Compiler-RT: integer arithmetic routines used on platforms that don't provide HW support
+; All the functions are described here
+; https://github.com/llvm/llvm-project/blob/main/compiler-rt/lib/builtins/README.txt
+; 
+; Starting with sbfv2, the code of compiler-rt library is not included in the final ELF file
+; but in ebpf and sbf did so we make sure that we don't inline those functions.
+;
+; Integral bit manipulation
+#[inline(never)] ^__ashldi3$
+#[inline(never)] ^__ashlti3$
+#[inline(never)] ^__ashrdi3$
+#[inline(never)] ^__ashrti3$
+#[inline(never)] ^__lshrdi3$
+#[inline(never)] ^__lshrti3$
+#[inline(never)] ^__clzsi2$
+#[inline(never)] ^__clzdi2$
+#[inline(never)] ^__clzti2$
+#[inline(never)] ^__ctzsi2$
+#[inline(never)] ^__ctzdi2$
+#[inline(never)] ^__ctzti2$
+#[inline(never)] ^__ffssi2$
+#[inline(never)] ^__ffsdi2$
+#[inline(never)] ^__ffsti2$
+#[inline(never)] ^__paritysi2$
+#[inline(never)] ^__paritydi2$
+#[inline(never)] ^__parityti2$
+#[inline(never)] ^__popcountsi2$
+#[inline(never)] ^__popcountdi2$
+#[inline(never)] ^__popcountti2$
+#[inline(never)] ^__bswapsi2$
+#[inline(never)] ^__bswapdi2$
+; integral arithmetic 
+#[inline(never)] ^__negdi2$
+#[inline(never)] ^__negti2$
+#[inline(never)] ^__muldi3$
+#[inline(never)] ^__multi3$
+#[inline(never)] ^__divsi3$
+#[inline(never)] ^__divdi3$
+#[inline(never)] ^__divti3$
+#[inline(never)] ^__udivsi3$
+#[inline(never)] ^__udivdi3$
+#[inline(never)] ^__udivti3$
+#[inline(never)] ^__modsi3$
+#[inline(never)] ^__moddi3$
+#[inline(never)] ^__modti3$
+#[inline(never)] ^__umodsi3$
+#[inline(never)] ^__umoddi3$
+#[inline(never)] ^__umodti3$
+#[inline(never)] ^__udivmoddi4$
+#[inline(never)] ^__udivmodti4$
+#[inline(never)] ^__udivmodsi4$
+#[inline(never)] ^__divmodsi4$
+#[inline(never)] ^__divmoddi4$
+#[inline(never)] ^__divmodti4$
+; floating point arithmetic
+#[inline(never)] ^(compiler_builtins::float::add::)?__adddf3$
+#[inline(never)] ^__muldf3$
+#[inline(never)] ^(compiler_builtins::float::div::)?__divdf3$
+#[inline(never)] ^(compiler_builtins::math::libm::exp::)?exp$
+#[inline(never)] ^__floatundidf$
+#[inline(never)] ^__powidf2$
+#[inline(never)] ^__unorddf2$
+#[inline(never)] ^__truncdfsf2$
+#[inline(never)] ^__ltdf2$
+#[inline(never)] ^__gtdf2$
+#[inline(never)] ^__fixdfdi$
+#[inline(never)] ^__gedf2$
+#[inline(never)] ^__floatsidf$
+#[inline(never)] ^__subdf3$
+#[inline(never)] ^__floattidf$
+
+#[inline(never)] ^.*::fmt$
+
+;; This is a wrapper so we inline it
+#[inline] ^([^:]+::)*CVT_uninterpreted_usize$
+
+#[inline] ^solana_program::account_info::AccountInfo::new$
+#[inline] ^solana_program::account_info::AccountInfo::lamports$
+#[inline] ^solana_program::account_info::AccountInfo::try_borrow_mut_lamports$
+#[inline] ^solana_program::account_info::AccountInfo::data_len$
+#[inline] ^solana_program::account_info::AccountInfo::try_data_len$
+#[inline] ^solana_program::account_info::AccountInfo::try_borrow_data$
+#[inline] ^solana_program::account_info::AccountInfo::try_borrow_mut_data$
+#[inline] ^solana_program::account_info::AccountInfo::data_is_empty$
+#[inline] ^solana_program::program::invoke_signed$
+#[inline] ^solana_program::program::invoke$
+#[inline] ^solana_program::program_pack::Pack::unpack$
+#[inline] ^solana_program::hash::Hash::new_from_array$
+#[inline] ^solana_program::sysvar::clock::<impl solana_program::sysvar::Sysvar for solana_program::clock::Clock>::get$
+#[inline] ^solana_program::poseidon::PoseidonHash::new$
+#[inline] ^solana_program::account_info::AccountInfo::assign$
+#[inline] ^solana_program::incinerator::check_id$
+#[inline] ^solana_program::system_program::check_id$
+#[inline] ^solana_program::system_program::id$
+#[inline] ^solana_program::rent::Rent::minimum_balance$
+#[inline] ^solana_program::sysvar::rent::<impl solana_program::sysvar::Sysvar for solana_program::rent::Rent>::get$
+#[inline] ^solana_program::instruction::get_stack_height$
+#[inline] ^solana_program::program::set_return_data$
+
+#[inline(never)] ^<solana_program::program_error::ProgramError as core::convert::From<u64>>::from$
+
+#[inline] ^core::result::unwrap_failed$
+#[inline] ^core::cell::RefCell<T>::borrow(_\d+)?$
+#[inline] ^core::cell::RefCell<T>::borrow_mut(_\d+)?$
+
+
+;; Borsh and common functions used by Borsh
+#[inline(never)] ^std::io::error::Error::new(_\d+)?$
+#[inline(never)] ^borsh::de::unexpected_eof_to_unexpected_length_of_input$
+
+
+;; We need to inline this function to avoid unsoundness results in
+;; NcnOperatorTicket::seeds and others.
+#[inline] ^<alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter(_\d+)?$
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Anchor-specific inlining
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; By default we don't inline anything from anchor.
+#[inline(never)] ^.*anchor_lang.*$
+
+;; except these functions
+
+#[inline] ^anchor_lang::accounts::account_loader::AccountLoader<T>::load(_[0-9][0-9]*)*$
+#[inline] ^anchor_lang::accounts::account_loader::AccountLoader<T>::load_mut(_[0-9][0-9]*)*$
+
+#[inline] ^<anchor_lang::accounts::account::Account<T> as core::clone::Clone>::clone(_[0-9][0-9]*)*$
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; try_from and try_from_unchecked might call to deserialize so we need to check case by case
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+#[inline] ^anchor_lang::accounts::account_loader::AccountLoader<T>::try_from(_[0-9][0-9]*)*$
+#[inline] ^anchor_lang::accounts::account_loader::AccountLoader<T>::try_from_unchecked(_[0-9][0-9]*)*$
+#[inline] ^anchor_lang::accounts::account::Account<T>::try_from_unchecked(_[0-9][0-9]*)*$
+#[inline] ^anchor_lang::accounts::account::Account<T>::try_from(_[0-9][0-9]*)*$
+#[inline] ^anchor_lang::accounts::signer::Signer::try_from$
+#[inline] ^<anchor_lang::accounts::program::Program<T> as core::convert::TryFrom<&solana_program::account_info::AccountInfo>>::try_from$
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+#[inline] ^<anchor_lang::accounts::unchecked_account::UncheckedAccount as core::convert::AsRef<solana_program::account_info::AccountInfo>>::as_ref$
+#[inline] ^<anchor_lang::accounts::unchecked_account::UncheckedAccount as anchor_lang::ToAccountInfos>::to_account_infos$
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; These are needed to include the code for key()
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+#[inline] ^<anchor_lang::accounts::unchecked_account::UncheckedAccount as anchor_lang::Key>::key$
+#[inline] ^<solana_program::pubkey::Pubkey as anchor_lang::Key>::key$
+#[inline] ^.*::ZeroCopyAccessor<solana_program::pubkey::Pubkey>>::get$
+#[inline] ^anchor_lang::accounts::account_info::<impl anchor_lang::Key for solana_program::account_info::AccountInfo>::key$
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;; These do conversion between error codes 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+#[inline] ^<anchor_lang::error::Error as core::convert::From<anchor_lang::error::AnchorError>>::from$
+#[inline] ^<anchor_lang::error::Error as core::convert::From<anchor_lang::error::ErrorCode>>::from$
+#[inline] ^<anchor_lang::error::Error as core::convert::From<solana_program::program_error::ProgramError>>::from$           
+#[inline] ^anchor_lang::error::<impl core::convert::From<anchor_lang::error::ErrorCode> for u32>::from$
+#[inline] ^squads_multisig_program::errors::<impl core::convert::From<squads_multisig_program::errors::MultisigError> for anchor_lang::error::Error>::from$

examples/svm/materialized_trivial_addition/certora/summaries/cvlr_summaries_core.txt

@@ -0,0 +1,96 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;;                    POINTS-TO SUMMARIES
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;;; if the call returns then (*i64)(r1+0) is always a valid pointer.
+;;; 1st call:
+;;; - precondition: (*i64)(r1+0) is a Rust dangling pointer
+;;; - post-condition: (*i64)(r1+0) points to new allocated memory (malloc)
+;;; 2nd call:
+;;; - precondition: (*i64)(r1+0) is a valid pointer
+;;; - post-condition: (*i64)(r1+0) points to a new allocated memory after resizing the memory object
+;;;                   to which r1 pointed to before the call (realloc).
+#[type((*i64)(r1+0):ptr_heap)]
+^alloc::raw_vec::RawVec<T,A>::reserve_for_push(_[0-9][0-9]*)*$
+#[type((*i64)(r1+0):ptr_heap)]
+^alloc::raw_vec::RawVec<T,A>::reserve::do_reserve_and_handle(_[0-9][0-9]*)*$
+
+#[type((*i64)(r1+0):num)]
+#[type((*i64)(r1+8):num)]
+^__multi3$
+
+#[type((*i64)(r1+0):num)]
+#[type((*i64)(r1+8):num)]
+^__udivti3$
+
+#[type((*i64)(r1+0):num)]
+#[type((*i64)(r1+8):num)]
+^__divti3$
+
+#[type(r0:num)]
+^__muldf3$
+
+#[type(r0:num)]
+^__divdf3$
+
+#[type((*i64)(r1+0):num)]
+#[type((*i64)(r1+8):num)]
+#[type((*i64)(r1+16):num)]
+#[type((*i64)(r1+24):num)]
+#[type((*i64)(r1+32):num)]
+^sol_get_clock_sysvar$
+
+;; %"AccountInfo" = type { %"Pubkey"*, i64*, i64*, %"Pubkey"*, i64, i8, i8, i8, [5 x i8] }
+#[type((*i64)(r1+0):ptr_external)]
+#[type((*i64)(r1+8):ptr_external)]
+#[type((*i64)(r1+16):ptr_external)]
+#[type((*i64)(r1+24):ptr_external)]
+#[type((*i64)(r1+32):num)]
+#[type((*i8)(r1+40):num)]
+#[type((*i8)(r1+41):num)]
+#[type((*i8)(r1+42):num)]
+^([^:]+::)*CVT_nondet_account_info$
+
+#[type((*i64)(r1+0):num)]
+#[type((*i64)(r1+8):num)]
+#[type((*i64)(r1+16):num)]
+#[type((*i64)(r1+24):num)]
+^([^:]+::)*CVT_nondet_pubkey$
+
+#[type((*i64)(r1+0):num)]
+#[type((*i64)(r1+8):num)]
+^([^:]+::)*CVT_nondet_layout_unchecked$
+
+#[type(r0:ptr_external)]
+^([^:]+::)*CVT_nondet_pointer_usize$
+
+#[type((*i32)(r1+0):num)]
+^solana_program::account_info::AccountInfo::realloc$
+
+;; Result<Pubkey, PubkeyError>
+#[type((*i8)(r1+0):num)]
+#[type((*i64)(r1+1):num)]
+#[type((*i64)(r1+9):num)]
+#[type((*i64)(r1+17):num)]
+#[type((*i64)(r1+25):num)]
+^solana_program::pubkey::Pubkey::create_program_address$
+
+;; (Pubkey, u8)
+#[type((*i64)(r1+0):num)]
+#[type((*i64)(r1+8):num)]
+#[type((*i64)(r1+16):num)]
+#[type((*i64)(r1+24):num)]
+#[type((*i8)(r1+32):num)]
+^solana_program::pubkey::Pubkey::find_program_address$
+
+
+#[type((*i32)(r1+0):num)]
+^solana_program::program::invoke_signed_unchecked$
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Anchor-specific summaries
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+;; Empty for now

…s/svm/trivial/src/certora/spec/checks.rs …/materialized_trivial_addition/checks.rsexamples/svm/trivial/src/certora/spec/checks.rs renamed to examples/svm/materialized_trivial_addition/checks.rs examples/svm/trivial/src/certora/spec/checks.rs renamed to examples/svm/materialized_trivial_addition/checks.rs

@@ -0,0 +1,12 @@
+use crate::add;
+
+use cvlr::prelude::*;
+
+/// Verifies that `add` correctly computes the sum of two numbers.
+#[rule]
+pub fn rule_add_is_correct() {
+    let x: u64 = nondet();
+    let y: u64 = nondet();
+    let result = add(x, y);
+    cvlr_assert_eq!(result, x + y);
+}