Discover an index of datasets, SDKs, APIs and open-source tools developed by Microsoft researchers and shared with the global academic community below. These experimental technologies—available through Azure AI Foundry Labs (opens in new tab)—offer a glimpse into the future of AI innovation.
Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license. Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages including…
KreMLin is a tool that extracts an F* program to readable C code. If the F* program verifies against a low-level memory model that talks about the stack and the heap; if it is first-order;…
Lean is a functional programming language that makes it easy to write correct and maintainable code. You can also use Lean as an interactive theorem prover. Lean programming primarily involves defining types and functions. This…
Boogie is an intermediate verification language (IVL), intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers…
A Python package that implements a variety of algorithms that mitigate unfairness in supervised machine learning.
This is a Microsoft Visual Studio solution that contains reference implementation of the TPM 2.0 Specification by TCG available at https://trustedcomputinggroup.org/tpm-library-specification. See the TPMCmd/tpm/include/TpmTypes.h header for the exact revision/date of the TPM 2.0 specification issue, which…
The source code for the simulations in the paper, 007: Democratically Finding The Cause of Packet Drops (NSDI 2018). To run: use MultiFailureDriver or SingleLinkFailureDriver (these are the starting points/drivers of the code).
This is a small library for implementing several standard “test collection” or “offline” evaluation measures for search systems. See: https://github.com/Microsoft/irmetrics-r
This C library implements FrodoKEM, an IND-CCA secure key encapsulation (KEM) protocol based on the well-studied Learning with Errors (LWE) problem [1], which in turn has close connections to conjectured-hard problems on generic, “algebraically unstructured” lattices. FrodoKEM is…
