Magma, a project I hope will make provably correct software possible for everyone

• magmide

  22 804 6.9 Coq

  A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

  

The idea with notations isn't to make custom symbology impossible, just clearly signaled, much in the same way Rust macros can do whatever they want but have to be underneath some macro_name!esque indicator. Check out my rough design thoughts for more if you're interested :) https://github.com/blainehansen/magma/blob/main/posts/design-of-magma.md

• Rudra

  11 1,294 5.5 Rust

  Rust Memory Safety & Undefined Behavior Detection

  

• InfluxDB

  www.influxdata.com sponsored

  Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

  

• rust-verification-tools

  2 241 3.1 Rust

  Discontinued RVT is a collection of tools/libraries to support both static and dynamic verification of Rust programs.

  

• prusti-dev

  23 1,460 8.8 Rust

  A static verifier for Rust, based on the Viper verification infrastructure.

  

Prusti too.

• tectonic

  22 3,750 9.2 C

  A modernized, complete, self-contained TeX/LaTeX engine, powered by XeTeX and TeXLive.

  

Taken by https://github.com/tectonic-typesetting/tectonic. Cool project too.

• line-combination-proofs

  1 0 0.0 TeX

I have verified some theory in Coq https://github.com/joonazan/line-combination-proofs/tree/master/proofs and would like to verify a Rust implementation, too.

• electrolysis

  2 322 10.0 Lean

  Simple verification of Rust programs via functional purification in Lean 2(!)

In my opinion the best way of going about it is translating the Rust to Coq that has the same semantics (but different performance) as pioneered in https://github.com/Kha/electrolysis. Unfortunately that project isn't usable today as it requires an ancient version of Rust and Lean.

• WorkOS

  workos.com sponsored

  The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

  

• fiat

  1 145 6.6 Coq

  Mostly Automated Synthesis of Correct-by-Construction Programs

  

Yeah once this project is actually real it could be used for that ha :) Your description kinda reminds me fiat: https://github.com/mit-plv/fiat which generates code from just a correctness specification.

Suggest a related project