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

giftpy

GIFT Core: Certified mathematical identities from E8×E8 gauge theory on G2 manifolds. Verified in Lean 4

acacia-boomslang

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

miesc

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

a2a-greenhelix-sdk

Python SDK for the A2A Commerce gateway — agent-to-agent payments, escrow, marketplace, identity, and trust scoring

proof-citations

Fetch URLs and verify that quoted text appears on the page. Extracted from proof-engine.

proof-engine-wiki

Attach verified Proof Engine proofs to LLM-wiki claims.

proof-engine-registry

Proof Registry protocol: client, reference server, and static-JSON emitter.

recordflux

A toolset for the formal specification and generation of verifiable binary parsers, message generators and protocol state machines.

invar-tools

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

goodhart

Catch reward traps before training. Named after Goodhart's Law.

cosa

CoreIR Symbolic Analyzer

csl-core

CSL-Core: Deterministic Safety Layer for Probabilistic AI Systems

watkins-nn

Conservation-law constrained optimization on the golden-ratio simplex

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

monogate-forge

EML language and compiler for verified mathematical computation. 33 backends (software · GPU shaders · FPGA · Lean proofs · safety-critical) from one source, with chain-order analysis and Lean-checkable contracts on every function.

agentassert-abc

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

qwed

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

skillfortify

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

cervellaswarm-lingua-universale

A verification language for AI agent protocols — session types, compiler, code generation, and formal verification