Full lesson
excalead
Continuous auditing for Solana smart contracts, with Formal Verification & AI
What it does
From the project README:
We combine the rigor of the **Rocq (Coq)** proof assistant with the speed of **AI automation** to bring formal methods to every Solana developer.
- Original
- Excalead/excalead
- SuperStack fork
- Blockchains/excalead @
71dcf87 - Stars
- 6
- Last push (original)
- 2025-12-05
- Languages
- Rocq Prover, Rust, Shell, Dune
- Detected stack
- Anchor
- Categories
- AI & Agents
- Licence
- MIT
- Homepage
- https://excalead.com/
Architecture
27 source files. By extension: .rs ×27.
| Top-level directory | Source files |
|---|---|
Excalead | 26 |
src | 1 |
Dapp: devnet deploy pending
⏳ Devnet deploy pending — goes live when the devnet wallet is topped up. This fork's own dapp is not deployed yet, so there is no program address or transaction to show. It is queued in dapp-queue.txt; once devnet SOL is available it is deployed, exercised with real devnet transactions, and this section switches to the live dapp at /dapps/excalead/. Until then, the lesson and step-by-step guide below are complete, and you can run it locally with the commands below.
Key code, explained
Excerpts chosen automatically where the code uses the most Solana concepts, pinned to the fork's commit.
Excalead/src/examples/quantu_8004/validation_registry/lib.rs L109–132 @ 71dcf87 · MIT · original validation_request.bump = ctx.bumps.validation_request; // Increment total requests counter config.total_requests = config.total_requests .checked_add(1) .ok_or(ValidationError::Overflow)?; // Emit event with full metadata (URI stored in event, not on-chain) emit!(ValidationRequested { agent_id, validator_address, nonce, request_uri, request_hash, requester: ctx.accounts.requester.key(), created_at: clock.unix_timestamp, }); msg!("Validation requested for agent #{} by validator {}", agent_id, validator_address); Ok(()) } /// Validator responds to a validation request (ERC-8004: validationResponse)- Line 109
validation_request.bump = ctx.bumps.validation_request;: Uses the bump seed, the extra byte that pushes the derived address off the ed25519 curve. - Line 113
.checked_add(1): Uses checked arithmetic so overflow fails instead of wrapping. - Line 117
emit!(ValidationRequested {: Emits an Anchor event that clients can parse from the logs. - Line 124
created_at: clock.unix_timestamp,: Reads on-chain time from the Clock sysvar. - Line 127
msg!("Validation requested for agent #{} by validator {}", agent_id, validator_address);: Logs to the program log, which is visible in explorers and the test output.
Excalead/src/secure/basic4.rs L25–48 @ 71dcf87 · MIT · original ctx.accounts.authority.key(), ctx.accounts.counter.authority, ErrorCode::Unauthorized ); ctx.accounts.counter.count += 1; Ok(()) }} #[derive(Accounts)]pub struct Initialize<'info> { #[account( init, payer = authority, space = Counter::SIZE, seeds = [b"counter"], bump )] counter: Account<'info, Counter>, #[account(mut)] authority: Signer<'info>, system_program: Program<'info, System>,}- Line 38
init,: Creates and pays for a new account. Space and payer must be specified. - Line 41
seeds = [b"counter"],: Declares the PDA seeds. Anchor re-derives the address and rejects the account if it doesn't match. - Line 42
bump: Uses the bump seed, the extra byte that pushes the derived address off the ed25519 curve. - Line 46
authority: Signer<'info>,: Requires this account to have signed the transaction.
Excalead/src/examples/domin8/reference/instructions/initialize.rs L13–36 @ 71dcf87 · MIT · original )] pub config: Account<'info, GameConfig>, #[account( init, payer = authority, space = GameRound::LEN, seeds = [GAME_ROUND_SEED], bump )] pub game_round: Account<'info, GameRound>, /// CHECK: This is the vault PDA that will hold game funds #[account( seeds = [VAULT_SEED], bump )] pub vault: UncheckedAccount<'info>, #[account(mut)] pub authority: Signer<'info>, pub system_program: Program<'info, System>,}- Line 17
init,: Creates and pays for a new account. Space and payer must be specified. - Line 20
seeds = [GAME_ROUND_SEED],: Declares the PDA seeds. Anchor re-derives the address and rejects the account if it doesn't match. - Line 21
bump: Uses the bump seed, the extra byte that pushes the derived address off the ed25519 curve. - Line 33
pub authority: Signer<'info>,: Requires this account to have signed the transaction.
Excalead/src/examples/domin8/reference/instructions/deposit_bet.rs L13–36 @ 71dcf87 · MIT · original )] pub game_round: Account<'info, GameRound>, /// CHECK: This is the vault PDA that holds game funds #[account( mut, seeds = [VAULT_SEED], bump )] pub vault: UncheckedAccount<'info>, #[account(mut)] pub player: Signer<'info>, pub system_program: Program<'info, System>,} pub fn deposit_bet( ctx: Context<DepositBet>, amount: u64,) -> Result<()> { let game_round = &mut ctx.accounts.game_round; let player_key = ctx.accounts.player.key(); let clock = Clock::get()?;- Line 19
seeds = [VAULT_SEED],: Declares the PDA seeds. Anchor re-derives the address and rejects the account if it doesn't match. - Line 20
bump: Uses the bump seed, the extra byte that pushes the derived address off the ed25519 curve. - Line 25
pub player: Signer<'info>,: Requires this account to have signed the transaction. - Line 36
let clock = Clock::get()?;: Reads on-chain time from the Clock sysvar.
How to run
No package.json, Anchor.toml, Cargo.toml, go.mod or Makefile was found near the root. See the project README.
What you could build from it
- Fork the SuperStack copy and extend it within the AI & Agents gaps listed on the idea page.
- Learn the pattern first: AI agents on Solana
- Learn the pattern first: Building and sending transactions from a client
- Learn the pattern first: Blinks and Solana Actions