CompCert Alternatives

Similar projects and alternatives to CompCert

  • coq

    CompCert VS coq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

  • corn

    CompCert VS corn

    Coq Repository at Nijmegen [[email protected],@VincentSe]

  • Scout APM

    Less time debugging, more time building. Scout APM allows you to find and fix performance issues with no hassle. Now with error monitoring and external services monitoring, Scout is a developer's best friend when it comes to application development.

  • unbound

    Replib: generic programming & Unbound: generic treatment of binders

  • silt

    CompCert VS silt

    An in-progress fast, dependently typed, functional programming language implemented in Swift.

  • acsl-by-example

    Public snapshots of "ACSL by Example"

  • cakeml

    CompCert VS cakeml

    CakeML: A Verified Implementation of ML

  • SonarQube

    Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.

  • sol2

    CompCert VS sol2

    Sol3 (sol2 v3.0) - a C++ <-> Lua API wrapper with advanced features and top notch performance - is here, and it's great! Documentation:

  • seL4

    CompCert VS seL4

    The seL4 microkernel

  • koika

    CompCert VS koika

    A core language for rule-based hardware design 🦑

  • Mumble

    CompCert VS Mumble

    Mumble is an open-source, low-latency, high quality voice chat software.

  • wuffs

    CompCert VS wuffs

    Wrangling Untrusted File Formats Safely

  • checkedc

    Checked C is an extension to C that lets programmers write C code that is guaranteed by the compiler to be type-safe. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors. Checked C does not address use-after-free errors. This repo has a wiki for Checked C, sample code, the specification, and test code.

  • winix

    A UNIX-style Operating System for the Waikato RISC Architecture Microprocessor (WRAMP)

  • proofs

    CompCert VS proofs

    My personal repository of formally verified mathematics.

  • why3

    CompCert VS why3

    SPARK 2014 repository for the Why3 verification platform. (by AdaCore)

  • vericert

    A formally verified high-level synthesis tool based on CompCert and written in Coq.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better CompCert alternative or higher similarity.

Suggest an alternative to CompCert

CompCert reviews and mentions

Posts with mentions or reviews of CompCert. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2022-07-05.
  • New Coq tutorial
    3 projects | reddit.com/r/ProgrammingLanguages | 5 Jul 2022
    Hi all, Coq is a "proof assistant" that allows you to write both code and proofs in the same language (thanks to the Curry–Howard correspondence). Its uses range from pure math (e.g., the Feit–Thompson theorem was proven in Coq!) to reasoning about programming languages (e.g., proving the soundness of a type system) to writing verified code (e.g., this verified C compiler!). You can "extract" your code (without the proofs) to OCaml/Haskell/Scheme for running it in production. Coq is awesome, but it's known for having a steep learning curve (it's based on type theory, which is a foundational system of mathematics). It took me several years to become proficient in it. I wanted to help people pick it up faster than I did, so I wrote this introductory tutorial. Hope you find it useful!
  • Ask HN: Can the same individual accomplish more with programming than proofs?
    1 project | news.ycombinator.com | 14 Apr 2022
  • The Software Foundations: mathematical underpinnings of reliable software
    4 projects | news.ycombinator.com | 5 Mar 2022
    Not an expert but I've heard formal methods are used in Chip Design. Also https://compcert.org/ a c compiler which uses formal verifcation. I tiored some exercises in the series. Its pretty interesting thing to do, but yes I don't think its great for rapid software development.
    4 projects | news.ycombinator.com | 5 Mar 2022
    The seL4 microkernel: https://sel4.systems/

    The CompCert C compiler: https://compcert.org/

    TLS implementation in Firefox: https://blog.mozilla.org/security/2020/07/06/performance-imp...

    Elasticsearch model checks some of their core algorithms with TLA+: https://youtu.be/qYDcbcOVurc.

    Amazon is known to apply formal methods in varying forms to services like S3: https://www.amazon.science/publications/using-lightweight-fo...

    Many components in airplane software is formally verified in some aspect.

  • Lol
    1 project | reddit.com/r/ProgrammerHumor | 15 Feb 2022
    They are useful for theorem proving and formal verification, which does not play well with non-termination. For example, CompCert, a formally verified C compiler, is written in Coq. So yes, I think they qualify as programming languages.
  • Two Mechanisations of WebAssembly 1.0
    2 projects | reddit.com/r/ProgrammingLanguages | 3 Jan 2022
    If this interests you, I'd highly recommend checking out CompCert (docs here) and CakeML.
  • Why the C Language Will Never Stop You from Making Mistakes
    5 projects | news.ycombinator.com | 30 Dec 2021
    With Frama-C you can prove doubly linked lists and all manner of complicated pointer manipulating graph algorithms. It does not impose a Rust-like pointer ownership policy as does SPARK.

    However, for embedded development, SPARK's restrictions are a good trade-off, as the more restrictive rules allow more proofs to be fully automated than with Frama-C and simplify diagnostic messages. A fly-by-wire avionics computer doesn't need to dynamically allocate a billion graph nodes. But SPARK is not "general purpose" like C with Frama-C is.

    AdaCore's SPARK tool stack is not actually written in SPARK as far as I can see, much of it is actually OCaml and Coq/Gallina for the Why3 component also used by Frama-C. See all the .ml OCaml and .v Gallina source code for yourself:

    https://github.com/AdaCore/why3

    And of course the compiler backend for Ada/SPARK is GNU GCC, written in unverified C:

    https://github.com/gcc-mirror/gcc/tree/master/gcc/config

    Compare with CompCert, the formally verified C compiler:

    https://github.com/AbsInt/CompCert

    Frama-C unfortunately requires a user to be mathematician-logician logic programming expert to fully utilize. One can begin training in Coq/Gallina with the large free online Software Foundations course:

    https://softwarefoundations.cis.upenn.edu/

  • Writing a Fuzzer for NES Games
    1 project | news.ycombinator.com | 27 Nov 2021
    I wonder if it will ever be possible for games like Super Mario Bros. to be "solved" in the sense that there is a formal proof of the shortest possible completion time (for a given category / ruleset of speedrun).

    Presumably that would first require a disassembly of the game, with a proven compilation process back to the original ROM (something like what CompCert does[0]) and then, after enumerating all the possible glitches, building some sort of state machine that defines how the character can progress through each level.

    [0] https://compcert.org/

  • Multicore OCaml: September 2021, effect handlers will be in OCaml 5.0
    1 project | news.ycombinator.com | 4 Oct 2021
    OCaml is becoming a must learn language for those who want to take their C programming to the highest levels, because:

    1. Frama-C, which enables writing bug-free C programs, is implemented using a combination of OCaml and the Coq proof assistant (which is itself implemented in OCaml):

    https://frama-c.com/

    2. CompCert, a formally verified C compiler, is implemented using OCaml and Coq:

    https://github.com/AbsInt/CompCert

    Nothing at this level yet exists in the Rust and Zig ecosystems, for example. Rust is a very complicated language with many features which makes formalization much harder than with C and OCaml, which both had mathematical ideas of simplicity, analyzability, and minimalism inspire their designs, even if they continue to grow into more complicated monsters, which, incidentally this OCaml 5.0 release will contribute towards. :-)

  • Coverage Is Not Strongly Correlated with Test Suite Effectiveness
    1 project | news.ycombinator.com | 28 Sep 2021
    Well, by this I mean math (and mathematical logic). Math is the tool for reasoning about possibly infinite concepts, i.e. you can make a statement about infinite sets and still know if it’s true or not. We aren’t limited to what we can see and touch, which is good because any non-trivial software application is so large that it could never be drawn out like a building blueprint. It can only be described and reasoned about abstractly.

    But, you are probably asking about what ‘tools’ can be applied to programming, meaning some kind of library or application. These are also out there. Here’s a few that I think are promising:

    TLA+: This is a specification language for describing and reasoning about computations as state machines, with a particular focus on modeling distributed systems. It has been used at Amazon to check designs for their distributed algorithms. They have used it to check parts of S3 for example: https://lamport.azurewebsites.net/tla/formal-methods-amazon....

    Best reference is the book Specifying Systems: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf.

    Then you have theorem provers / proof assistants based on type theory. These are frankly complex, but getting better.

    F*: This one is the most exciting to me. It’s currently being used to develop a formally verified HTTPS stack: https://project-everest.github.io/. They already have components released to the Linux kernel and Firefox. One of the most exciting things about this tool is that you can verify an efficient, stateful algorithm and extract highly performant C code from it. Their verified implementations have equal or better performance to the current solutions out there. So all of the overhead is for verification, none exists at runtime.

    Of course you can’t talk about proof assistants without mentioning Coq. Its claim to fame is producing a formally verified C compiler, CompCert: https://compcert.org/.

    As you can see, so far, formal verification has been mostly limited to components of systems, not entire systems. But, it’s a start, and the scope of what we can verify is getting larger.

  • What are real world examples of dependent types signficant improving security or productivity?
    1 project | reddit.com/r/agda | 13 Sep 2021
    Check out CompCert C compiler. It's your usual C compiler but with all optimizations verified to be correct (i. e. not changing program semantics). This means that as long as you agree with definition of program semantics given in the compiler (it's reasonable) and believe that Coq - the dependently typed language behind CompCert - is correct, you can be sure that no optimization breaks your code and that's a big deal since program optimization algorithms are very prone to bugs in usual compilers.
  • Proof Assistant Makes Jump to Big-League Math | Quanta Magazine
    1 project | reddit.com/r/math | 29 Jul 2021
    Again, the answer is "it depends"; there's even fragmentation between Lean3 and Lean4. Coq is very good at many things, such as verified compilers whilst Lean3 could never dream of such things. Lean4 is written in Lean4 so there's some hope for that. Meanwhile, a lot of maths has been written in both and they're both still actively used; I personally prefer Lean but that's personal preference. A "good" baseline to see mathematical progress in various proof assistants is Freek's 100 theorem list.
  • Hacker News top posts: Jun 27, 2021
    3 projects | reddit.com/r/hackerdigest | 27 Jun 2021
    A Proven Correct C Compiler\ (76 comments)
  • A Proven Correct C Compiler (Used by Airbus)
    1 project | reddit.com/r/hackernews | 27 Jun 2021
    7 projects | news.ycombinator.com | 26 Jun 2021
    As noted in the License section of the readme,

    > CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. A commercial version of CompCert, without this restriction and with professional support and extra features, can be purchased from AbsInt. See the file LICENSE for more information.

    However, https://github.com/AbsInt/CompCert/blob/master/LICENSE goes onto say that

    > The following files in this distribution are dual-licensed both under

Stats

Basic CompCert repo stats
21
1,431
7.1
24 days ago

AbsInt/CompCert is an open source project licensed under GNU General Public License v3.0 or later which is an OSI approved license.

SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
Find remote jobs at our new job board 99remotejobs.com. There are 3 new remote jobs listed recently.
Are you hiring? Post a new remote job listing for free.