acsl

Public snapshots of "ACSL by Example"

Linux kernel library functions formally verified.

MCP server that gives AI agents Frama-C: EVA, WP, and sandboxed ACSL iteration

Generation of mutant programs

Fully proved small C functions (examples for verification course).

Towards a formally verified, tiny and permissively licensed C standard library, using Frama-C (fork of Baselibc/Klibc)

A number of utilities for writing ACSL specifications for a Linux module.

This repository contains both the server and client software that implement the Language Server Protocol (LSP) for C/ACSL language. The server part is a novel Frama-C plugin called "lsp". The client part is a VsCode extension.

Static & Dynamic Verification of C programs

Tiny programs with ACSL specifications.

Frama-C plugin for inference of ACSL contracts for C helper functions

ACSL grammar built up from official specification, with C grammar behind

Inlining of ACSL predicates and logic functions

A Study in Implementing Functional Programming Languages

Agent Skills for deductive verification of C with Frama-C/WP: writing ACSL specifications, running and triaging proofs, designing provable C, and hand-written Coq when nothing else closes the goal.

Convert your ACSL scripts to equivalent R code.

Alphastar Ada master course CC39-21 - Covers several different CP competitions

SKILL.md-standard proofreading skill — code & document review with real, verified formal-verification backends for C, Python, Rust, Java, and C++

Программы для работы с репозитарием AstraVer

A repository for holding solutions to the ACSL 2017-2018 contest problems.