The efficient SMT-based context-bounded model checker (ESBMC)
Artifact of the paper "Sound Verication of Security Protocols: From Design to Interoperable Implementations"
Tamarin Model & Verified Go Implementation of the WireGuard VPN Key Exchange Protocol
Artifact for "The Secrets Must Not Flow: Scaling Security Verification to Large Codebases" (S&P '26)
FailSafe: An autonomous fact-checking framework leveraging Multi-Agent LLMs and Structured Argumentation Graphs (SAG) to verify claims with deep-web retrieval and reasoning.
Automated formal verification tool for vision classifiers using CLIP embeddings and MILP optimization. Converts OWL ontologies into ConSpec specifications and provides mathematical guarantees about model behavior in safety-critical AI systems.
A different implementation of Decentralized Systems and Blockchain Technologies
An automated, real-time EWS verification platform replacing paper certificate fraud with cross-registry telemetry (Income Tax, UPI volumes, Aadhaar family graphs, and digitized land records). Programmatically enforces PPP urban tiering and structural agricultural land caps. Designed by Srinivasa.
Certus is a finetuned model that generates machine-checkable correctness certificates for Python functions, plus a checker that verifies them with counterexample search. 83% of certificates survive Hypothesis testing on unseen code.
To associate your repository with the automated-verification topic, visit your repo's landing page and select "manage topics."