Downloads
MicroCode
June 2024
Microsoft MicroCode is an icon-based programming language and editor for young learners to code with the BBC micro:bit V2. MicroCode allows you to program the micro:bit V2 with only an Arcade shield accessory – no other computer is required! If…
REST API Fuzz Testing
November 2020
This self-hosted service developed for Azure, including its orchestration engine and security tools (including MSR’s RESTler), enables developers to embed security tooling into their CI/CD workflows.
VCC
April 2016
VCC is a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program…
Koka
June 2021
Koka: a Functional Language with Effects Koka is a strongly typed functional-style language with effect types and handlers.
Lean interactive theorem prover
May 2018
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 allows your focus to remain…
Z3 automated theorem prover
May 2018
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 .NET, C, C++, Java, OCaml,…
Boogie intermediate verification language
May 2018
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 for C and the verifiers…
Microsoft Touch Develop
February 2015
Touch Develop is a touch-friendly, cross-platform, mobile-first app creation environment.