Idealized GCM from the University of Exeter

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

A decoder for various HF data modes

Carbon Language's main repository: documents, design, implementation, and related tools. (NOTE: Carbon Language is experimental; see README)

Qlib is an AI-oriented quantitative investment platform that aims to realize the potential, empower research, and create value using AI technologies in quantitative investment, from exploring ideas…

FinRL: Financial Reinforcement Learning. 🔥

Python implementations of the RL algorithms in examples and figures in Sutton & Barto, Reinforcement Learning: An Introduction

Verification-condition-generation-based verifier for the Viper intermediate verification language.

Crucible is a library for symbolic simulation of imperative programs

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

Symbolic-execution-based verifier for the Viper intermediate verification language.

The Rosette solver-aided host language, sample solver-aided DSLs, and demos

The Vellvm (Verified LLVM) coq development.

Definition of the Viper intermediate verification language.

The VerCors verification toolset for verifying parallel and concurrent software

The opensmt solver

Research prototype tool for modular formal verification of C and Java programs

The SAW scripting language.

UCLID5: formal modeling, verification, and synthesis of computational systems

Persistent, fast mmap'd database for Common Lisp using MOP; includes its own GC systems

Ray tracing engine, from scratch, in C++

simple, C-like compiled programming language

☕ Official Cup Programming Language Development Toolkit

UCalgary version of forallx, an introduction to formal logic

Looking for a guide? You came to the right place. Here you can find documentation for a variety of topics I research to make complex computing easier. For comments go to the IRC channel #nfo at the…

This repository contains coding examples of all sorts written in ATS and possibly other programming languages. These examples are primarily meant as recipes for people interested in learning ATS as…

The Flix Programming Language

A statically typed lisp, without a GC, for real-time applications.

Boogie