fpoli
Follow
Stars
The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
arXiv LaTeX Cleaner: Easily clean the LaTeX code of your paper to submit to arXiv
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs!
Research prototype tool for modular formal verification of C and Java programs
Capability-based verifier for safe Rust clients of interior mutability
LaTeXML: a TeX and LaTeX to XML/HTML/ePub/MathML translator.
fault-tolerant Python3 package for searching, navigating, and modifying LaTeX documents
Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for RISC-V with focus on a formally verified and auditable security monitor.
Lean 4 programming language and theorem prover
ShellCheck, a static analysis tool for shell scripts
A guide to how rustc works and how to contribute to it.
Scan your Rust crate for semver violations.
Carbon Language's main repository: documents, design, implementation, and related tools. (NOTE: Carbon Language is experimental; see README)
SPARK 2014 is the new version of SPARK, a software development technology specifically designed for engineering high-reliability applications.
Flowistry is an IDE plugin for Rust that helps you focus on relevant code.
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
An interpreter for Rust's mid-level intermediate representation
Rust mid-level IR Abstract Interpreter
Creusot helps you prove your code is correct in an automated fashion.