fiat
by mit-plv
Mostly Automated Synthesis of Correct-by-Construction Programs
AI summary
Data type synthesizer
A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications
- stars
- 149
- forks
- 32
- watching
- 9
- awesome list
- 1
Similar projects
Found by comparing what the projects do, not just their names.
Code generator
Automated generation of cryptographic primitive code using a constructive design approach
Coq utility library
A collection of reusable tools and utilities for working with the Coq proof assistant
RISC-V spec
An implementation of the RISC-V instruction set specification in Coq
Program verifier
Automated verification of higher-order programs using separation logic
Bit Vector Library
A repository unifying bit vector definitions and lemmas across multiple Coq projects.
Hardware specification platform
A platform for high-level parametric hardware specification and modular verification
Compiler toolkit
A toolkit for compiling functional programs into imperative code for performance-critical applications
Hardware design language
A formal language for designing and verifying rule-based hardware systems
Type synthesizer
A package providing runtime type representations and a syntax extension to synthesize them from OCaml types
Formalism library
A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination.
Type inference tool verifier
A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools.
Relational programming semantics
A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages
Hypothesis manager
A Coq library providing tactics to manipulate hypotheses in formal proofs.
Coq generator
Tool for generating Coq definitions and proofs for locally nameless representations
RISC-V semantics
A formal specification of the RISC-V instruction set architecture in Haskell
Featured in 1 awesome list
Each link jumps to the spot where the list mentions fiat.
