s2n-tls is a C99 implementation of the TLS/SSL protocols designed by AWS for simplicity, small size, and security. It supports TLS 1.2 and 1.3, including features like 0-RTT early data, session tickets, post-quantum KEMs (ML-KEM, ML-DSA), and QUIC transport integration. The library provides a public C API (api/s2n.h) and multiple libcrypto backends (OpenSSL, AWS-LC, BoringSSL, LibreSSL). Extensive formal verification (CBMC, SAW, SideTrail) and fuzz testing ensure memory safety and constant-time execution. The architecture is highly modular with a stuffer buffer abstraction, blob/array utilities, a table-driven TLS extension framework, and a robust error-handling macro system. Rust bindings are first-class, offering safe wrappers (s2n-tls), async Tokio integration (s2n-tls-tokio), an HTTP client connector for Hyper (s2n-tls-hyper), and a metrics subscriber for handshake analysis. The library is used by AWS services like S3 and KMS, and includes interoperability tests against OpenSSL, GnuTLS, Java, and rustls. It is actively maintained with a sophisticated CI pipeline covering unit, integration, fuzz, formal proof, and performance regression tests across multiple platforms and libcrypto versions.
The Solidity compiler (solc) is a production-grade, multi-pass compiler that translates Solidity smart contract source code into EVM bytecode. It supports two compilation pipelines: a legacy EVM assembly backend and a newer IR-based pipeline via Yul, which also serves as the optimizer intermediate representation. The optimizer suite comprises approximately 80 composable passes, including control-flow simplification, common subexpression elimination, function inlining, and store elimination. The compiler integrates formal verification through SMT solvers (Z3, cvc5, Eldarica) using both BMC and CHC engines. A C API (libsolc) enables embedding, and a CLI provides rich output options (ABI, bytecode, IR, metadata, storage layout). The codebase demonstrates deep compiler engineering with advanced static analysis, SSA construction, stack layout optimization, and genetic-algorithm-based optimizer tuning (yulPhaser). It is extensively tested with semantic, syntax, fuzz, and external integration tests.
Ibex is a production-quality open-source 32-bit RISC-V CPU core designed for embedded control applications. It provides a highly configurable, synthesizable core written in SystemVerilog with support for RISC-V ISA extensions (I, E, M, C, B) and security features like PMP, lockstep, and data-independent timing. The core features a modular architecture with separate functional units, a sophisticated configuration system via YAML/Python, and extensive verification infrastructure including UVM testbenches, formal proofs, and co-simulation with Spike ISS. It is actively maintained and used in real silicon designs including OpenTitan.
Chisel is a hardware construction language (DSL) embedded in Scala. It provides a rich set of abstractions (Module, Bundle, Reg, Mem, UInt, SInt, Bool, Vec, Clock, When) for describing synchronous digital circuits at the register-transfer level. The system compiles these circuit descriptions into an intermediate representation (FIRRTL/CIRRTL) and then uses the CIRCT compiler framework to generate synthesizable SystemVerilog. It also includes a comprehensive simulation framework (svsim, ChiselSim) for verification on Verilator or VCS, formal verification capabilities (LTL properties), and a standard library of reusable hardware components (counters, queues, FIFOs, arbiters, decoders, PRNGs). The architecture is a multi-stage compiler pipeline: user code elaboration, FIRRTL IR conversion, and CIRCT-based code generation. It relies on external tools like firtool, Verilator, Espresso, and Slang. The codebase is actively maintained with a clear versioning history (7.x), but carries significant technical debt from a deprecated FIRRTL package, an ongoing Scala 2 to Scala 3 migration, and a large surface of experimental features.
ESBMC (Efficient SMT-based Bounded Model Checker) is a mature, open-source formal verification tool that automatically detects or proves the absence of runtime errors in C, C++, Python, Java/Kotlin (via Jimple), CHERI, and Solidity programs. It parses source code using language-specific frontends (Clang for C/C++, CPython parser for Python, Soot for Java), converts programs into a common GOTO intermediate representation, and performs bounded symbolic execution with SMT solving (Z3, Bitwuzla, CVC5, Yices, etc.). The tool checks for assertions, memory safety (buffer overflows, null pointers, use-after-free), arithmetic overflows, concurrency races, and user-defined contracts (requires/ensures/assigns). It supports advanced verification techniques including k-induction, loop invariant synthesis, incremental BMC, and quantifier reasoning. The architecture is modular: frontends produce GOTO programs, which are then processed by a series of analysis passes (pointer analysis, value-set analysis, loop unrolling, contract enforcement) before being encoded into SMT formulas. The solver backend is pluggable, with support for interactive solvers and experimental one-shot solvers (Mallob, NeuroSym). The repository includes an extensive regression test suite with thousands of small, self-contained test cases organized by language and feature, many with paired passing/failing variants to ensure soundness. Operational models for C standard library functions, C++ STL, Python standard library (including numpy), and SystemC are bundled as source code for SMT translation. Key entry points include the main ESBMC binary (built from `src/esbmc/`), the Clang C/C++ frontend (`src/clang-c-frontend/`), the Python frontend (`src/python-frontend/`), and the solver interfaces (`src/solvers/`). The tool is actively used in research and industry, has won 43 awards at SV-COMP and Test-Comp, and is supported by multiple funding agencies. External dependencies include Boost (program_options, filesystem), Clang/LLVM, and several SMT solvers.
Chiasmus is a neurosymbolic verification engine packaged as a TypeScript library and Model Context Protocol (MCP) server. It bridges LLMs with formal solvers — Z3 (SMT) and SWI-Prolog (WASM) — by translating natural-language problems into template-based formal specifications that are verified with mathematical certainty. It also performs static code analysis: tree-sitter-based extraction of call graphs for TypeScript/JavaScript, Python, Go, Rust, Clojure, Scheme, Racket, and Common Lisp, followed by 16 analyses (reachability, dead code, impact, cycles, layer violations, community detection, hubs, bridges, diffs). Architecturally, the repo is a modular ESM library with an MCP server entry point (src/mcp-server.ts) exposing 11 tools over stdio (chiasmus_graph, chiasmus_map, chiasmus_formalize, chiasmus_verify, chiasmus_search, chiasmus_review, chiasmus_learn, etc.). Core subsystems: graph extraction with per-file content-hash caching and snapshot diffing; a formalization engine that selects from 8 built-in skill templates via BM25/embedding retrieval and runs an LLM-driven correction loop against the solvers; a SQLite-backed skill library that learns new templates from verified solutions; and pluggable LLM adapters (Anthropic, OpenAI-compatible, Azure, local via node-llama-cpp). Data flows: source files are parsed by tree-sitter into a CodeGraph, which can be emitted as Prolog facts for symbolic queries or analyzed natively with O(V+E) algorithms (Tarjan SCC, BFS). For verification, a problem statement is embedded, matched to a template, slot-filled by an LLM, linted, and iteratively corrected until the Z3/Prolog solver confirms the property or finds a counterexample. The benchmark suite compares Chiasmus against traditional implementations across RBAC, dependency resolution, taint analysis, workflow validation, and validation consistency. Maintenance is active (v0.1.28, CI on Node 22/24, 70+ test files covering graph extraction, solvers, MCP tools, search, and skills). The codebase is well-engineered with several genuinely reusable components — native graph algorithms, an LRU extraction cache, a BM25 index, and a tsconfig alias resolver — though some coupling exists between the extractor and the TypeScript type environment, and the vendored WASM grammars require periodic upstream syncs.
This repository implements a compiler-based optimization framework for zero-knowledge virtual machines (zkVMs), specifically targeting OpenVM and SP1. Its core innovation is Automatic Precompile Synthesis (APC), which analyzes execution traces of RISC-V guest programs and synthesizes optimized constraint systems (symbolic machines) that drastically reduce proof cost—achieving up to 9x column reduction and 88x constraint reduction on complex operations. The system combines profile-guided optimization (PGO), a sophisticated constraint solver with range reasoning and rule-based rewriting, and an optional Lean4 verified optimizer via FFI. The architecture is a multi-crate Rust workspace with a CLI (`powdr_openvm_riscv`) orchestrating a staged pipeline: generate APCs from execution profiles, select the best candidates using PGO metrics, setup the prover with the selected APCs, execute the program, and generate proofs. It supports CPU and GPU (CUDA) backends, and includes extensive benchmarking infrastructure with nightly regression analysis and a web-based APC effectiveness viewer. Bus interaction handling is abstracted via a `BusMap` and adapter pattern, making the optimization logic VM-agnostic. While primarily an application, the repository has strong research character: it includes domain-specific formal methods (Lean4, Datalog rules), empirical constraint detection, and a large corpus of snapshot tests documenting optimizer outputs. It is actively maintained with CI pipelines, but depends on several tightly coupled forks (OpenVM, SP1) and pinned nightly Rust toolchains, posing moderate technical drift risk.
This repository is a formal verification suite for Clawdbot, a Discord bot, using TLA+ and the TLC model checker. It provides machine-checkable security models that act as a regression suite: 'green' models should pass (no invariant violation) and 'red' models are deliberately buggy variants that should fail with a counterexample trace. The repo includes over 100 TLA+ specifications covering gateway exposure, node command policy, pairing store invariants, routing isolation, Discord-specific conformance (role gating, PluralKit, thread binding), and liveness properties. It also contains scripts to extract tool group definitions from the main Clawdbot codebase and generate TLA+ configuration constants, ensuring conformance between the formal models and the implementation. The architecture is a collection of TLA+ specs and model configs orchestrated by a Makefile, with a vendored TLC jar and a CI pipeline that runs selected models on each PR. While the models are domain-specific to Clawdbot, the patterns (e.g., policy precedence, pairing store with expiry and cap, tokenized approvals) are reusable templates for formal verification of similar systems.
This repository is the content generation and build system for the interactive textbook *Mathematics in Lean*. It is a hybrid project: primarily a set of Python scripts and a Lean 4 project that together produce the textbook in multiple formats (Sphinx RST/HTML/PDF), as well as a separate user repository with exercise stubs and solutions. The core pipeline parses Lean source files annotated with custom directives (`TEXT`, `EXAMPLES`, `SOLUTIONS`) via `scripts/mkdoc.py` to generate textbook prose and Lean exercise files. A Sphinx build then produces the final HTML/PDF documentation. The Lean source files themselves cover mathematics from basic arithmetic to measure theory, heavily leveraging the Mathlib library. The repository includes CI/CD workflows (GitHub Actions), developer environments (Devcontainers, Gitpod), and testing scripts that verify the generated Lean files compile. While not a traditional application, it functions as a specialized toolchain for creating and deploying formal mathematics educational content.
BosqueCore is a compiler and toolchain for the Bosque programming language, a research-oriented language emphasizing mechanized reasoning, deterministic execution, and safe-by-design programming. The repository implements a full compilation pipeline in TypeScript: a recursive-descent parser and lexer, a semantic type checker with advanced features (invariants, pre/post conditions, validated strings, numeric range types), an IR with monomorphization, and a C++ backend that generates garbage-collected, allocation-aware code. The CLI (`src/cmd/bosque.ts`) compiles `.bsq` files to C++ and produces executables via a Makefile build system. Extensive tests cover parser, typechecker, C++ emission, and runtime execution of sample programs (raytracer, nbody, binary tree). The architecture is cleanly split between frontend (AST, parsing, checking) and backend (IR, monomorphization, C++ emission), with a hand-written recursion-descent parser and a highly detailed type system. However, the codebase is a work in progress: many language features are explicitly unimplemented (tasks, switch, dispatch, multi-return, resource/env handling) with `assert(false, "Not implemented")` stubs, and large monolithic files (e.g., `parser.ts`, `checker.ts`, `flatten.ts`) concentrate complexity. The repository also includes a C++ runtime with a custom GC and allocators, plus a lexer/serializer for the BAPI IR format. As a research project transitioning toward practical use, it offers a unique, safety-focused language design but is not yet production-ready.