Formal Verification Python Packages

pyvcg

Verification Condition Generator

certora-cli

The Certora Prover is the state-of-the-art security tool for automated formal verification of smart contracts running on EVM-based chains, Solana and Stellar

certora-cli-alpha-master

The Certora Prover is the state-of-the-art security tool for automated formal verification of smart contracts running on EVM-based chains, Solana and Stellar

certora-cli-beta

The Certora Prover is the state-of-the-art security tool for automated formal verification of smart contracts running on EVM-based chains, Solana and Stellar

certora-cli-beta-mirror

The Certora Prover is the state-of-the-art security tool for automated formal verification of smart contracts running on EVM-based chains, Solana and Stellar

a2a-greenhelix-sdk

Agent-to-agent payments, escrow and formal verification services

giftpy

GIFT mathematical core - Formally verified constants (Lean 4)

miesc

Multi-layer Intelligent Evaluation for Smart Contracts — 35 analysis modules, 9 defense layers, one command. Pre-audit triage for Ethereum, Starknet, and beyond.

acacia-boomslang

A minimal implementation of reactive synthesis via universal co-Buchi automata using antichains

invar-tools

AI-native software engineering tools with design-by-contract verification

agentassert-abc

Formal behavioral specification and runtime enforcement for autonomous AI agents. Agent Behavioral Contracts (ABC).

recordflux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines

skillfortify

First formal security scanner for AI agent skills & plugins. Static analysis, supply chain verification, SBOM generation. 22 frameworks supported including MCP, LangChain, CrewAI.

watkins-nn

Conservation-law constrained optimization on the golden-ratio simplex

proof-citations

AI agent skill that creates formal, verifiable proofs of claims — every fact computed or cited, never asserted

proof-frog

A tool for verifying transitions in cryptographic game-hopping proofs

qwed

The Deterministic Verification Protocol for AI - 11 verification engines for math, logic, code, SQL, facts, images, and more. Now with Agentic Security Guards.

cosa

CoreIR Symbolic Analyzer

proof-engine-registry

AI agent skill that creates formal, verifiable proofs of claims — every fact computed or cited, never asserted

proof-engine-wiki

Attach verified Proof Engine proofs to LLM-wiki claims.

csl-core

Deterministic policy language for AI agents. Z3 + TLA+ dual-engine formal verification. Runtime enforcement <1ms.

certora-cli-alpha-oz-publish-test

The Certora Prover is the state-of-the-art security tool for automated formal verification of smart contracts running on EVM-based chains, Solana and Stellar

arbiter-debate

Open-source framework for formally verifying academic paper claims using multi-agent LLM debate + Z3/Knuckledragger proof certificates. Supports OpenAI, Anthropic, Google, Grok.

python-invar

From AI-generated to AI-engineered code. Guides AI agents to write verifiable code through contracts and structured workflows.