The Center for Digital Trust's Showcase

Anyway

Self-hosted AI platform for private, on-premise LLM inference

Anyway orchestrates on-premise hardware into a distributed inference cluster supporting any Hugging Face model. It deploys as a standalone app, Docker image, or Kubernetes pod and provides an OpenAI-compatible REST API endpoint, giving organisations full model control and fixed operational costs with no per-token fees.

PrivacyShield

BLE beacon relay system to prevent unwanted AirTag tracking using ESP32 relays.

System countering unsolicited BLE tracker-based surveillance by relay-confusing AirTag and similar devices. Architecture: Flask server, modified AirGuard Android app, ESP32 BLE relay firmware, and optional Sniffle-based sniffer tools. Fully open-source under GPLv3/MIT.

HalluHard

Hard multi-turn hallucination benchmark for evaluating language models across domains.

Multi-turn hallucination benchmark evaluating LLMs across diverse domains. Installed via Pixi; scripts provided for response generation, claim-based web-scraping judgment (or coding_direct mode), and report creation. Supports multiple models and CLI configuration. Designed to maximize hallucination elicitation difficulty.

Votegral

End-to-end verifiable, coercion-resistant voting system using TRIP for in-person registration.

End-to-end verifiable, coercion-resistant voting system using TRIP for in-person registration. Implements E2E verification and coercion resistance via randomized ballot shuffling and re-encryption. Includes simulation framework, Docker/local build, configurable hardware and shuffle modes, and performance metrics generation.

DebateGPT

Code and data for studying the conversational persuasiveness of GPT-4.

Code and data for studying conversational persuasiveness of GPT-4 vs. human debaters, published in Nature Human Behaviour. Includes scripts for data processing, linguistic feature extraction, and statistical analysis. Reproduces all experiments from the associated arXiv paper.

TiME

Training tiny monolingual language models via knowledge distillation from larger models.

Knowledge distillation pipeline for training tiny monolingual encoders from XLM-R or HPLT teacher models. Supports downstream evaluation for POS tagging, lemmatization, dependency parsing, and NER. Includes checkpoint selection scripts, distillation pipelines, and evaluation tooling.

Truman

Constructs device behavior models from OS drivers for virtual-device fuzzing.

Framework for constructing device behavior models from OS device drivers, capturing inter- and intra-message dependencies. Generates dependency-aware seeds for virtual-device fuzzing via dynamic binary instrumentation (DBI). Docker-based build, fuzzing, and coverage collection pipelines provided.

SPD

Single-pass detection classifier for jailbreaking inputs in large language models.

Single-pass jailbreak detection classifier for LLMs extending JailbreakBench. Trained on 4,000+ samples from GCG, AutoDAN, and PAIR attack methods. TMLR 2025 paper. Provides training and evaluation scripts and a unified detection interface.

Reflecta

Reflection-based, language-agnostic fuzzer for scripting languages.

Language-agnostic fuzzer for scripting language interpreters leveraging reflection APIs to generate valid programs. Supports Ruby, MRuby, CPython, MicroPython, PHP, and V8. Dockerized with scripts for campaign launch, coverage collection, and result visualization. Compatible with reflecta, nautilus, and polyglot fuzzers.

arkworks

Rust ecosystem for zkSNARK programming

Arkworks provides efficient implementations of components required for zkSNARK applications. It includes libraries for finite fields, elliptic curves, R1CS constraints, and SNARK proving systems like Groth16 and Marlin. It defines interfaces for relations like R1CS, and for building SNARK circuits using gadgets and subcircuits.

d-voting

A decentralized, fully anonymous voting system for EPFL-internal elections.

Secure and Privacy-Preserving Credentials for E-ID

Research techniques to improve privacy when using electronic identities

Today's identity security faces challenges like misuse and tracking. Our goal is to enable secure, anonymous, unlinkable E-ID interactions by researching novel cryptographic algorithms. This boosts user trust, creates new business opportunities, and cuts financial losses after data breaches.

Showcase v2.0

Version 2.0 of the C4DT's showcase.

Disco

Decentralized Collaborative Machine Learning

A collection of objects and routines to help you develop your own distributed machine learning algorithm. It has two modes, federated, where a server is keeping track of the model, and decentralized, where each participant has their own local model. You can train your model directly in the browser, allowing it to run on a variety of hardware. Many extensions are in the pipeline, such as adding Byzantine resistance or training without revealing the model. Compared to other solutions, Disco is bridging the gap between people creating machine learning models and people having relevant data. By running without installation nor complex configuration, anyone can help. It's also a breeding ground for new machine learning technologies.

Orchestrated Artifact Evaluation

Automatically evaluating code artifacts from research papers

While there has been a strong push for adding reliable code artifacts to research papers since 2018, the process of evaluating them is still manual and often very tedious. Orchard proposes a standardized framework based on Docker to automatically evaluate those artifacts.

Combattre le phishing: quelles innovations apporter ?

Combating phishing through vulnerability analysis, detection tools, and best practice guidelines.

This project addresses phishing threats through the analysis of existing countermeasures, identification of vulnerabilities, and development of innovative solutions including best practice guidelines and tools for email configuration testing and malicious link detection. The initiative enhances organizational and societal resilience against phishing attacks through knowledge dissemination and fosters collaboration among stakeholders.

Sécurisation de Digiinov Hmi en adéquation avec le Cyber Resilience Act (CRA)

Securing industrial HMI software for EU Cyber-Resilience-Act compliance

This project integrates state-of-the-art software security measures into Digiinov HMI, a platform bridging Operational Technology (OT) and Information Technology (IT) for industrial Human-Machine Interfaces. The collaboration with HEIG-VD and EPFL focuses on achieving compliance with the EU Cyber-Resilience-Act (CRA) requirements before its 2027 enforcement. The security enhancements target the software development lifecycle and maintenance processes for embedded industrial control systems.

Matrix@EPFL

The Matrix server run for the EPFL community by the EPFL Center for Imaging with help from the EPFL Center for Digital Trust.

Lattigo

A lattice-based multiparty homomorphic encryption library in Go

Lattigo is a Go module for Multiparty Homomorphic Encryption, that implements Ring-Learning-With-Errors-based homomorphic encryption primitives. It comprises highly-efficient RNS versions of the BFV and CKKS schemes and their multiparty (N-out-of-N-threshold) counterparts. It also implements a dense-key and sparse-key Bootstrapping procedure for RNS-CKKS. The Lattigo library was originally exclusively developed by the EPFL Laboratory for Data Security until its version 2.4.0. Starting with the release of version 3.0.0, Lattigo is maintained and supported by Tune Insight SA. Lattigo 2.0.0 has been code-reviewed by ELCA in November 2020 and, within the allocated time for the code review, no critical or high-risk issues were found.

MetaWearS

Meta-learning framework for few-shot adaptation in wearable health monitoring.

Meta-learning framework for few-shot adaptation in wearable health monitoring. Pre-trains on large datasets with prototypical network structure; fine-tunes on few shots per user. Lightweight update mechanism conserves battery. Provides code, Jupyter notebooks, and hardware implementation details.

nwsim

Network simulation suite integrating ns-2 with pFabric, SIRD, DCTCP, and Homa.

ns-2 simulation suite extended with pFabric, SIRD, DCTCP, and Homa transport protocols, plus OMNET integration. Provides configuration scripts for incast and random traffic experiments and output processing tools for queue occupancy and application metrics.

Miralis

Virtual firmware monitor for RISC-V with formal verification via Kani.

Virtual firmware monitor for RISC-V running below M-mode firmware, providing isolation and policy enforcement via sandbox and Keystone policies. Includes a Rust RISC-V ISA translator, benchmark scripts, and formal verification via Kani. Supports Docker and manual setup. SOSP'25 artifact.

PEPO

Preference alignment framework for language models using DPO and RLHF techniques.

Preference alignment framework for LLMs implementing DPO, RLHF, and related techniques. Uses Hydra for configuration management; supports SLURM cluster scheduling, CUDA systems, training and evaluation pipelines, and environment variable management. Pre-commit hooks included for code quality.

TiMoE

Modular framework for temporally grounded language models with time-aware expert routing.

Modular Mixture-of-Experts (MoE) framework for temporally grounded LLMs. Trains separate GPT experts on two-year data slices; routes queries to experts up to the query timestamp. Aggregates outputs via equal weighting, learned routing, or joint co-adaptation. Includes repo structure and quickstart instructions.

NEX

Full-stack simulation framework running unmodified software while modelling hardware accelerators.

Full-stack simulation framework running unmodified software stacks on real CPUs while modeling hardware accelerators (VTA, JPEG, Protoacc) via RTL simulation or DSim. Supports multi-accelerator setups, DMA and interconnect latency modeling, and epoch-based scheduling. Integrates with the SimBricks modular simulation platform.

Timeseries Saliency Maps

Cross-domain saliency maps library for time-series model explanation in PyTorch and TensorFlow.

Library implementing cross-domain saliency maps for time-series model explainability in PyTorch and TensorFlow. Supports time, frequency, and ICA domains via invertible differentiable transforms. Requires no model retraining; extensible to custom transforms. Pip-installable with ready-to-run notebooks.

BoostCD

Information extraction system with training, inference, and evaluation pipeline.

End-to-end information extraction system with training, inference, and evaluation pipelines. Uses a conda environment and Hugging Face datasets; supports training on custom data, batched inference, and prediction postprocessing. Published at an NLP conference.

libErator

Automatically generates fuzzing drivers for libraries by extracting constraints.

Framework for automated fuzzing driver synthesis for C/C++ libraries. Uses static analysis to extract API constraints and pre/post-conditions, then generates conforming drivers for libfuzzer. Includes a customized libfuzzer build and tooling to add new fuzzing targets and run experiments.

GP TA Emulator

GlobalPlatform Trusted Application emulator with GDB and fuzzing support.

Emulator for GlobalPlatform-compliant Trusted Applications (TAs) enabling development, debugging (GDB support), and fuzzing without physical TEE hardware. Provides Docker setup, PoC build instructions, Android NDK cross-compilation, and fuzzing harness with crash handling and replay.

NoiseDiff

Dark Noise Diffusion for synthetic low-light noise generation and image denoising.

Dark Noise Diffusion model for synthetic low-light noise generation and paired image denoising. Trained on SID and ELD datasets; uses diffusion-based noise simulation to augment training data. Provides pretrained models, training/testing scripts, shading resources, and optional synthetic data generation pipeline.

zip2zip

High-performance LZW compression library with Python bindings for adaptive vocabularies.

High-performance C LZW compression library with Python bindings (cffi/ctypes). Supports adaptive vocabularies for LLM tokenization pipelines; includes a novel LZW variant that decompresses LLM- generated sequences without requiring a perfectly encoded input stream. Install via pip or from source.

Tandem Training

Code and data for tandem training of language models.

Code and data for the "Tandem Training for Language Models" paper (arXiv:2510.13551). Implements coordinated joint training of language model pairs. Pre-trained models available on Hugging Face. Authors: West, Anderson, Kamar, Horvitz.

ICCWD

Scripts for the Image-Caption in the Wild Dataset and minor-detection method evaluation.

Scripts for downloading and evaluating the Image-Caption in the Wild Dataset (ICCWD) using three minor-detection pipelines: DeepSeek caption labeling, Amazon Rekognition image analysis, and a combined approach. Outputs TPR/FPR metrics and ROC curves.

WF4NYM

Website fingerprinting and flow-correlation attacks on the Nym mixnet.

Artifact for website fingerprinting and flow-correlation attacks on the Nym mixnet and Tor. Evaluates the WTF4NYM defense, analyzes feature importance, and measures overhead. Implemented in Python 3.9/3.10 on Linux; includes code, datasets, and full reproduction instructions.

Scion Optimizer

Norm-constrained optimizer with multiple norm implementations for neural network training.

Norm-constrained optimizer for neural network training with reference implementations of Scion and ScionLight supporting multiple norms (spectral, Frobenius, etc.). Includes hyperparameter guidance, nanoGPT/MLP/CNN example configurations, and notes on a recent momentum initialization change.

LEAF

Levenshtein Efficient Adversarial Finetuning for creating a robust CLIP text encoder.

Levenshtein Efficient Adversarial Finetuning (LEAF) for a robust CLIP text encoder resilient to character-level perturbations. Combined with FARE (robust image encoder) for dual-domain robustness. Pre-trained models on HuggingFace; provides training and evaluation procedures.

CHAMELEON

Data-mixing framework using Kernel Ridge Leverage Scores for LLM pretraining and finetuning.

Data-mixing framework using Kernel Ridge Leverage Scores (KRLS) for domain weighting in LLM pretraining and finetuning. Computes domain embeddings and weights to optimize universal generalization and transferability. Integrates with existing training pipelines via simple scripting.

NBL

Neural Block Linearization replacing self-attention with LMMSE approximations for faster LLM inference.

LLM inference acceleration via selective replacement of self-attention with linear LMMSE approximations. CCA-based error bounding identifies low-error layers without fine-tuning. Achieves ~32% speed-up on Llama-8B with <1% accuracy loss. Supports quantization, LoRA fine-tuning, and speculative decoding.

ClippedScion

Reference implementation of ClippedScion optimizers supporting multiple norms.

Reference implementation of ClippedScion and UnconstrainedClippedScion optimizers extending Scion with gradient clipping. Supports multiple norms and hyperparameter configurations for nanoGPT, CNN, and DeiT training with example setups and citation information.

Gradient-Normalized Smoothness

Algorithms for optimization with approximate Hessians using gradient-normalized smoothness.

Implementation of the gradient-normalized smoothness (GNS) analysis framework for optimization with approximate Hessians. Provides algorithms, oracle functions, Hessian approximation routines, and utilities for convex and non-convex settings. Includes quick-start instructions and examples reproducing paper results.

LLM Optimizer Benchmark

Benchmark for comparing optimizers for LLM pretraining on Llama and MoE models.

Benchmarking suite for comparing optimizers (Adam, SGD, Muon, Scion, etc.) on LLM pretraining using Llama and MoE architectures. Supports configurable training parameters, WandB logging, multi-GPU and CPU setups, and guidelines for extending to new models or datasets.

MTBBench

Benchmark for evaluating multimodal LLM reasoning in complex oncology clinical decision-making scenarios

MTBBench is a benchmark for evaluating multimodal LLM reasoning in oncology, covering two core challenges: multimodal integration (pathology, genomics, radiology) and longitudinal reasoning across patient timelines. It includes agentic tasks requiring interaction with external foundation-model-based tools such as TRIDENT for pathology and DrugBank for pharmacology.

NASS

Dynamic binary instrumentation tool for fuzzing Android native system services.

Dynamic binary instrumentation (DBI) framework for discovering and fuzzing Android native system services. Requires a rooted device with ADB and NDK r26. Provides scripts for interface extraction, seed generation, fuzzing campaigns, crash triage, and evaluation against COTS and FANS baselines. Docker setup available.

PHEE

Posit-enabled X-HEEP RISC-V platform integrating the Coprosit arithmetic coprocessor.

X-HEEP RISC-V SoC extended with the Coprosit posit coprocessor via CV-X-IF, targeting the cv32e40px CPU. Supports configurable posit sizes and quire operations. Provides QuestaSim simulation, PYNQ-Z2 FPGA synthesis, vendor update management, and test commands.

Compigra

MLIR-based compilation tool transforming C/C++ code into CGRA assembly.

MLIR-based compilation tool transforming C/C++ to CGRA assembly via custom IR dialects, front-end optimizations, and a back-end ILP mapper requiring Gurobi. Build with CMake; run via compigra-opt; results verifiable with CGRA-simulator or RTL tools.

AquaCast

Transformer-based time-series forecasting framework for urban water dynamics.

Research framework for multi-variate, multi-horizon time-series forecasting of urban water dynamics using transformer architectures. Includes synthetic datasets, Docker setup, and experiment scripts. Real operational data unavailable due to NDAs. References an arXiv preprint.

Mage

Remote memory system for scalable memory-intensive applications with asynchronous decoupling.

Remote memory system for memory-intensive workloads using asynchronous decoupling, pipelined execution, and contention avoidance at the LibOS layer, implemented on top of RDMA. Artifact includes kernel module, LibOS, baseline comparisons (kernel swap, Fastswap), and full evaluation scripts.

Fold

Rust framework for building dynamic linkers with syscall filtering and function hooks.

Rust framework for constructing custom dynamic linkers with syscall filtering, inter-module communication, and invisible function-hook injection. Includes quick-start guide, required toolchain, VSCode configuration, and example projects demonstrating core capabilities.

Lorikeet

Scalafix-based code quality feedback tool with custom rule definitions via query patterns.

Scalafix-based linting and automated grading framework with custom rule definitions via semantic query patterns and rewrite templates. Supports batch student submission checking, formatting feedback, and developer assistance. Scripts included for testing, publishing, and evaluation.

LPN/DSim for SimBricks

LPN/DSim integration with SimBricks for modular network and accelerator simulation.

Integration of LPN/DSim with the SimBricks modular simulation platform. Supports building and connecting gem5, QEMU, VTA, and Protoacc simulators with configurable disk images and experiment scripts. Docker support and all required dependencies are included.

Kernel TLA+ Specifications

Formal TLA+ specifications of Linux kernel synchronization algorithms.

Formal TLA+ specifications of Linux kernel synchronization primitives: ASID allocator, queued RW locks, ticket spinlock, context switching, queued spinlock, arm64 KPTI, and FPSIMD/SVE state saving. Includes TLC model checker scripts for both simulation and exhaustive verification.

Grounded Arithmetic

Prototype of Grounded Arithmetic logic formalized in Isabelle/Pure.

Isabelle/Pure prototype of the Grounded Arithmetic (GA) logic system. Features a complete axiomatization, arithmetic functions, Cantor tuple constructions, a manually encoded List datatype, and the accompanying B.Sc. thesis PDF and source files.

Droidot

Framework to fuzz Android app native libraries on arm64.

Fuzzing framework for Android app native libraries (arm64) using static analysis to extract function signatures and generate fuzzing harnesses. Workflow: Docker setup → APK loading → emulator setup → static analysis → harness generation → fuzzing → crash triage. Includes emulator, fuzzing, harness, and static analysis tooling.

SYSYPHUZZ

Syzkaller-based kernel fuzzer targeting low-frequency code regions with coverage-guided scheduling.

Kernel fuzzer extending Syzkaller with selective task scheduling to prioritize low-frequency basic blocks and context-preserving mutations. Introduces warm-up mode with basic-block hit-count tracking via kcov instrumentation. Achieves better coverage of rare but bug-prone kernel code paths.

Beanpod TEE Pwn

Proof-of-concept exploit for the keyinstall Trusted Application on Xiaomi Redmi Note 11s 5G.

PoC exploit targeting the keyinstall Trusted Application in the Beanpod TEE on Xiaomi Redmi Note 11s 5G. Demonstrates mapping of secure monitor memory via a vulnerability in the TA's key installation flow. Requires rooted device; provides kernel module and verification steps.

HEEPidermis

X-HEEP-based SoC for GSR and impedance recording with DMA and level-crossing support.

X-HEEP-based SoC for galvanic skin response (GSR) and impedance recording using an iDAC and 14-bit VCO-ADC. Supports DMA, digital Level-Crossing detection, and JTAG/SPI/UART interfaces. Board preparation, programming modes, and RTL simulation steps documented in the README.

HEEPidermis Breakout Board

Hardware breakout board for HEEPidermis with connector pinout documentation.

Hardware breakout board for the HEEPidermis SoC providing accessible connector pinouts for integration and testing. Includes a connector pinout spreadsheet and diagram link for hardware engineers.

CHEEP Boards

Modular PCB suite with configurable power supplies and current measurement modules.

Modular PCB suite with a main board (FTDI, power, peripherals) and 150-pin connector for custom breakout boards. Chewing-gum modules add configurable voltage supplies or current measurement. I²C multiplexers manage address conflicts. Open-source with extension APIs for custom module development.

Veritas

Syzkaller-based fuzzer with specification-based oracle for detecting eBPF misbehavior.

Syzkaller-based kernel fuzzer augmented with the SpecCheck specification-based oracle, which encodes formal eBPF semantics. Detects eBPF misbehavior by comparing runtime behavior against specifications. Runs on Ubuntu 22.04; includes bug-finding, comparison, and performance evaluation tooling.

Dietary Consistency and Gut Microbiota

Analysis code for a Swiss cohort study on dietary patterns and gut microbiota diversity.

Analysis pipeline for the "Food & You" digital cohort studying associations between dietary consistency, quality metrics, and gut microbiota diversity. Includes alpha/beta diversity correlations, differential abundance analysis via BIRDMan and QIIME2, taxa correlation studies, and machine learning prediction of microbiome composition from longitudinal dietary variables.

Meal Timing Analysis

Analysis of meal timing effects on dietary quality and glucose response.

Analysis notebooks for the "Food & You" digital cohort examining meal timing and dietary quality effects on glycemic response. Implements partial correlations, linear mixed effects models, mediation analysis, weekend effects, and incremental area under the curve (iAUC) determinants using CGM-derived and dietary intake data.

Food Additive Gut Microbiota

Code for analyzing food additive exposure and its impact on gut microbiota diversity.

Analysis pipeline using non-negative matrix factorization (NMF) to identify additive co-consumption patterns from MyFoodRepo barcode logs and OpenFoodFacts ingredient data, followed by z-score normalization, composite contrast metrics, and BIRDMan differential abundance analysis to assess associations between food additive mixtures and gut microbiota diversity in the "Food & You" digital cohort.

LibRRD

Build and CLI deployment tool with a web GUI component.

Build orchestration tool using SBT for compilation, with a Node.js CLI (v20+) and a statically served browser-based GUI. Deploy with `sbt deploy`; run CLI via `node cli/cli.js`; serve the GUI from the gui/ directory.

dvar-track

Emacs Lisp tool for tracking dynamic variable dependencies with eldoc support.

Emacs Lisp tool for static analysis of dynamic variable (defvar) dependencies in Elisp and C sources. Provides dependency graphs, reporting, eldoc integration for on-the-fly documentation, and docstring annotations. Includes C analysis patches targeting Emacs internals.

Logical Pinning

Coq formalization of logical pinning for container-internal pointers.

Coq formalization of logical pinning for container-internal (interior) pointers. Covers core libraries and case studies for linked lists and binary trees. Provides automated (make) and manual build paths with explicit dependencies. Accompanies a published research paper.

NEX+DSim Artifact Evaluation

Artifact evaluation guide for reproducing accelerated hardware-software stack simulations.

Artifact evaluation guide for reproducing performance simulations of VTA, Protoacc, and JPEG accelerators across NEX+DSim, NEX+RTL, gem5+DSim, and gem5+RTL configurations. Covers Docker setup, SimBricks build, gem5 scripting, and NEX experiment execution.

Kyber

Cryptographic library

DRand

Publicly verifiable randomness

matchertext

Matchertext is a syntactic discipline that allows strings in one compliant language to be embedded verbatim without escaping (e.g., via cut-and-paste) into itself or another compliant language.

EPFL Combinational Benchmark Suite

Benchmarks for logical gates optimizer

Igor

Crash deduplication through root-cause clustering

Fuzzing has emerged as the most effective bug-finding technique. The output of a fuzzer is a set of proof-of-concept (PoC) test cases for all observed “unique” crashes. It costs developers substantial efforts to analyze each crashing test case. This, mostly manual, process has lead to the number of reported crashes out-pacing the number of bug fixes. Igor is a tool for automated crash grouping/deduplication.

3D-ICE

Thermal simulator for stacked integrated circuits

x-heep

Open-source RISC-V system-on-chip for healthcare monitoring

The X-HEEP project is an open-source RISC-V microcontroller designed for continuous healthcare monitoring. It provides a customizable microcontroller unit (MCU) composed of an open-source, industrial-grade RISC-V CPU, common peripherals, and memories, which users can extend with their own accelerators. The project targets both FPGA and ASIC implementations, with support for Xilinx-based FPGAs.

ByzFL

Python library for Byzantine-resilient federated learning, compatible with PyTorch and NumPy.

ByzFL implements state-of-the-art robust aggregators (Trimmed Mean, Geometric Median, Krum, Centered Clipping, etc.) and pre-aggregators (NNM, Bucketing, ARC) as well as Byzantine attack strategies (IPM, ALIE, Sign Flipping, Mimic, …) fully compatible with PyTorch tensors and NumPy arrays. It also ships a complete federated learning simulation pipeline for systematic benchmarking under adversarial conditions.

Choix

Library that provides inference algorithms for models based on Luce's choice axiom

kickscore

Dynamic skill rating system

Kickscore can be used to understand & visualize the skill of players (or teams) competing in pairwise matches, and to predict outcomes of future matches. It extends the Elo rating system and TrueSkill.

Stainless

Verification framework for a subset of the Scala programming language

Stainless is a tool for verifying Scala programs developed by the LARA. It can verify that your program is correct for all inputs, it can report inputs for which your program fails when they exist, and it can prove that functions do not loop.

Inox

Constraint solver for Stainless

Inox can be used to prove constraints on methods in a program, to attest the correctness of these parts.

LISA

A Proof Assistant based on first order logic, sequent calculus and set theory.

Scallion

A library for writing parsers and pretty printers for LL(1) languages in Scala.

Refiner

Reasoning framework with feedback on intermediate steps

REFINER is an interaction-based framework for natural language reasoning tasks. It has a CRITIC model that provides structured feedback on intermediate reasoning steps, and a GENERATOR model that solves the reasoning task by first generating intermediate steps. The core idea is the interaction between the generator and critic, where the generator's steps are improved via feedback from the critic.

AIcrowd

Open platform for data science challenges