Lean 4 formalization of a uniform zero-free region for Dedekind zeta functions: ζ_K(s) ≠ 0 for Re(s) > 31/32

The is the official implementation of "s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs"

Build an agent harness and control it end-to-end. Open-source SDK for production AI agents in Python & TypeScript - any model, any cloud.

Minimal reproduction of DeepSeek R1-Zero

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

LLM code

A project to map out the relations between different equational theories of Magmas.

Public reference documents for the SMT-LIB standard

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

Command line wrapper to interact with CodeGuru Reviewer

List of bugs found in distributed protocols

(now moved to Codeberg) An equational theorem prover based on Knuth-Bendix completion

MATLAB Independent, Small & Safe, High Integrity Tools - code formatter and more

Materials related to security: docs, checklists, processes, etc...

Management of Benchmark Instances and Instance Attributes

This repository contains code developed by the SRI team for the IARPA/TrojAI program.

NASA PVS Library of Formal Developments

FASTEN: FormAl SpecificaTion ENvironment - a set of DSLs to experiment with rigorous systems and safety engineering.

Create beautiful diagrams just by typing notation in plain text.

The Yices SMT Solver

This is solc-verify, a modular verifier for Solidity.

SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers

CV

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.

JavaSMT - Unified Java API for SMT solvers.

Source code verification service for Ethereum smart contracts